why3doc index index

Implementation of logarithmic-time ordered associative tables on top of AVL trees

Author: Martin Clochard

module MapBase

Shared base implementation between set and map structures

  use int.Int
  use avl.SelectionTypes
  use option.Option
  use ref.Ref
  use seq.Seq
  use mach.peano.Peano as I

Implementation parameters

  val constant balancing : I.t
    ensures { result > 0 }

The level of balancing is left abstract.

  scope D type t 'a end scope K type t end
  clone export key_type.KeyType with type t = D.t, type key = K.t
  clone preorder.Computable as CO with type t = K.t, axiom .
  scope D
    let function measure 'a : unit = ()
  end

Stored elements are identified by totally ordered keys

  scope M
    type t = unit
    constant zero : unit = ()
    function op (_x _y:unit) : unit = ()
    let lemma neutral_ (x:unit) : unit
      ensures { op zero x = x = op x zero }
    = match x with _ -> () end
    clone export monoid.Monoid with type t = t,
      constant zero = zero,function op = op,lemma assoc,lemma neutral
    clone export monoid.MonoidSumDef with type M.t = t,
      constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
    let zero () : unit ensures { result = () } = ()
    let op (_x _y:unit) : unit ensures { result = () } = ()
  end

As we do not need any extra information in order to perform search for this particular instance, we instantiate the monoid by unit.

  type selector = K.t

In associative tables, elements are selected with respect to their keys.

  predicate selection_possible (_:'b) (s:seq (D.t 'a)) =
    forall i j. 0 <= i < j < length s -> CO.lt s[i].key s[j].key

Efficient search for ordered keys can be carried out efficiently only in strictly increasing sequences.

  predicate upper_bound_s (k:K.t) (s:seq (D.t 'a)) =
    forall i. 0 <= i < length s -> CO.lt s[i].key k
  predicate lower_bound_s (k:K.t) (s:seq (D.t 'a)) =
    forall i. 0 <= i < length s -> CO.lt k s[i].key

  predicate selected (k:K.t) (e:split (D.t 'a)) =
    let _s = rebuild e in
    upper_bound_s k e.left /\ lower_bound_s k e.right /\
    match e.middle with None -> true | Some d -> CO.eq k d.key end

Selected splits correspond to sorted sequence, in which:

1) the left part precede the selector key

2) the selector key precede the right part

3) If it exists, the middle element has key equivalent to the selector

  let selected_part (ghost lseq rseq:seq (D.t 'a))
    (k:K.t) (_l:'e) (d:D.t 'a) (_r:'f) : part_base K.t
    requires { selection_possible k (lseq ++ cons d rseq) }
    returns { Here -> let e2 = { left = lseq;
        middle = Some d;
        right = rseq } in selected k e2
      | Left sl -> selection_possible sl lseq /\
        forall e. selected sl e /\ rebuild e = lseq ->
          selected k (right_extend e d rseq)
      | Right sr -> selection_possible sr rseq /\
        forall e. selected sr e /\ rebuild e = rseq ->
          selected k (left_extend lseq d e) }
  = let kd = d.key in
    let ghost s = (lseq ++ cons d rseq) in
    assert { forall i. 0 <= i < length rseq -> rseq[i] = s[i+length lseq+1] };
    assert { d = s[length lseq] };
    let cmp = CO.compare k kd in
    if cmp < 0
    then Left k
    else if cmp > 0
    then Right k
    else Here

Comparison-based binary search

  clone avl.AVL as Sel with type selector = selector,
    predicate selection_possible = selection_possible,
    predicate selected = selected,
    val selected_part = selected_part,
    goal selection_empty,
    val balancing = balancing,
    type D.t = D.t,
    val D.measure = D.measure,
    type M.t = M.t,
    constant M.zero = M.zero,
    function M.op = M.op,
    goal M.assoc,
    goal M.neutral,
    function M.agg = M.agg,
    goal M.agg_empty,
    goal M.agg_sing,
    goal M.agg_cat,
    val M.zero = M.zero,
    val M.op = M.op

Full instantiation of the avl module.

Adaptation of the specification to associative tables

  type t 'a = { field : Sel.t 'a } invariant { selection_possible () field }
  by { field = Sel.empty () }

Extra invariant: sequence sorted

  type m 'a = {
    domn : K.t -> bool;
    func : K.t -> D.t 'a;
    card : int;
  }

  predicate domain (s:seq (D.t 'a)) (k:K.t) =
    exists i. 0 <= i < length s /\ CO.eq s[i].key k

  let ghost function make_func (s:seq (D.t 'a)) (k:K.t) : D.t 'a
    requires { selection_possible () s /\ domain s k }
    ensures { forall i. 0 <= i < length s /\ CO.eq s[i].key k -> result = s[i] }
  = let j = ref 0 in
    while not CO.eq s[!j].key k do
      invariant { 0 <= !j < length s }
      invariant { CO.le s[!j].key k }
      variant { length s - !j }
      j := !j + 1
    done;
    s[!j]

  function m (t:t 'a) : m 'a =
    { domn = fun y -> domain t.field y;
      func = fun y -> make_func t.field y;
      card = length t.field }
  meta coercion function m

  let lemma correction (t:t 'a)
    ensures { forall k1 k2. CO.eq k1 k2 -> t.domn k1 <-> t.domn k2 }
    ensures { forall k1 k2. CO.eq k1 k2 /\ t.domn k1 -> t.func k1 = t.func k2 }
    ensures { forall k. t.domn k -> CO.eq k (t.func k).key }
    ensures { t.card >= 0 }
  = ()

  (* Link model and selection. *)
  let lemma selected_model (k0:K.t) (e:split (D.t 'a))
    requires { selection_possible k0 (rebuild e) }
    requires { selected k0 e }
    ensures {
      let s = rebuild e in
      match e.middle with
      | None -> forall k. CO.eq k k0 -> not domain s k
      | Some d -> forall k. CO.eq k k0 -> domain s k /\ make_func s k = d
        by s[length e.left] = d so CO.eq d.key k
      end
      /\ (forall k. CO.le k k0 -> not domain e.right k)
      /\ (forall k. CO.le k0 k -> not domain e.left k)
      /\ (forall k. CO.lt k0 k -> domain e.right k <-> domain s k)
      /\ (forall k. CO.lt k k0 -> domain e.left k <-> domain s k)
      /\ (forall k. CO.lt k0 k /\ domain e.right k ->
        make_func e.right k = make_func s k)
      /\ (forall k. CO.lt k k0 /\ domain e.left k ->
        make_func e.left k = make_func s k)
    }
  = ()

  (* Link selection and sortedness. *)
  let lemma selected_sorted (k0:K.t) (e:split (D.t 'a))
    requires { selected k0 e }
    ensures { selection_possible k0 (rebuild e) <->
      selection_possible k0 e.left /\ selection_possible k0 e.right }
  = ()

  let empty () : t 'a
    ensures { result.card = 0 /\ forall k. not result.domn k }
  = { field = Sel.empty () }

Create an empty associative table.

  let singleton (d:D.t 'a) : t 'a
    ensures { forall k. result.domn k <-> CO.eq k d.key }
    ensures { forall k. CO.eq k d.key -> result.func k = d }
    ensures { result.card = 1 }
  = { field = Sel.singleton d }

Create an associative table with a single element.

  let is_empty (ghost rk:ref K.t) (t:t 'a) : bool
    ensures { result -> forall k. not t.domn k }
    ensures { not result -> t.domn !rk }
    ensures { result <-> t.card = 0 }
  = let res = Sel.is_empty t.field in
    ghost if not res then rk := t.field.Sel.m.Sel.seq[0].key;
    res

Check emptyness of an associative table.

  let min (t:t 'a) : D.t 'a
    requires { t.card > 0 }
    ensures  { t.domn result.key /\ t.func result.key = result }
    ensures  { forall k. t.domn k -> CO.le result.key k }
  = Sel.front t.field

  let max (t:t 'a) : D.t 'a
    requires { t.card > 0 }
    ensures  { t.domn result.key /\ t.func result.key = result }
    ensures  { forall k. t.domn k -> CO.le k result.key }
  = Sel.back t.field

  let decompose_min (t:t 'a) : option (D.t 'a,t 'a)
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (d,r:t 'a) -> t.card = r.card + 1 /\
        t.domn d.key /\ t.func d.key = d /\ not r.domn d.key /\
        (forall k. CO.lt k d.key -> not t.domn k) /\
        (forall k. CO.eq k d.key -> t.func k = d) /\
        (forall k. CO.le k d.key -> not r.domn k) /\
        (forall k. CO.lt d.key k -> r.domn k <-> t.domn k) /\
        (forall k. CO.lt d.key k /\ r.domn k -> r.func k = t.func k) }
  = match Sel.decompose_front t.field with
    | None -> None
    | Some (d,r) -> Some (d,{ field = r })
    end

Get and extract the element with minimum key from the table.

  let decompose_max (t:t 'a) : option (t 'a,D.t 'a)
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (l:t 'a,d) -> t.card = l.card + 1 /\
        t.domn d.key /\ t.func d.key = d /\ not l.domn d.key /\
        (forall k. CO.lt d.key k -> not t.domn k) /\
        (forall k. CO.eq k d.key -> t.func k = d) /\
        (forall k. CO.le d.key k -> not l.domn k) /\
        (forall k. CO.lt k d.key -> l.domn k <-> t.domn k) /\
        (forall k. CO.lt k d.key /\ l.domn k -> l.func k = t.func k) }
  = match Sel.decompose_back t.field with
    | None -> None
    | Some (l,d) -> Some ({ field = l },d)
    end

Get and extract the element with maximum key from the table.

  let add_min (d:D.t 'a) (t:t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt d.key k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k d.key -> not result.domn k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { forall k. CO.lt d.key k -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt d.key k /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.cons d t.field }

Optimized insertion of an element with minimum key.

  let add_max (t:t 'a) (d:D.t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt k d.key }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt d.key k -> not result.domn k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { forall k. CO.lt k d.key -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k d.key /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.snoc t.field d }

Optimized insertion of an element with maximal key.

  let ordered_union (l r:t 'a) : t 'a
    requires { forall k1 k2. l.domn k1 /\ r.domn k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.domn k <-> l.domn k \/ r.domn k }
    ensures  { forall k. result.domn k /\ l.domn k -> result.func k = l.func k }
    ensures  { forall k. result.domn k /\ r.domn k -> result.func k = r.func k }
    ensures  { result.card = l.card + r.card }
  = { field = Sel.concat l.field r.field }

Ordered union of two associative tables.

  let get (k:K.t) (t:t 'a) : option (D.t 'a)
    returns { None -> not t.domn k
      | Some d -> t.card > 0 /\ CO.eq d.key k /\ t.domn k /\ t.func k = d }
  = Sel.get (Sel.default_split ()) k t.field

Get the value associated to a key in the table, if it exists.

  let insert (d:D.t 'a) (t:t 'a) : t 'a
    ensures { result.card = if t.domn d.key then t.card else t.card + 1 }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { result.domn d.key /\ result.func d.key = d }
    ensures { forall k. not CO.eq k d.key -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k d.key /\ result.domn k ->
      result.func k = t.func k }
  = let r0 = Sel.default_split () in
    let t2 = Sel.insert r0 d.key d t.field in
    selected_model d.key !r0;
    let r1 = { !r0 with middle = Some d } in
    assert { rebuild r1 = t2 };
    selected_model d.key r1;
    { field = t2 }

Insert a value in the table. Erase binding if the key was already present.

  let remove (k0:K.t) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.domn k }
    ensures { not result.domn k0 }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.remove (Sel.default_split ()) k0 t.field }

Erase any binding associated to the given key.

  let split (k0:K.t) (t:t 'a) : (t 'a,option (D.t 'a),t 'a)
    returns { (lf:t 'a,o,rg:t 'a) ->
      (forall k. CO.lt k k0 -> lf.domn k <-> t.domn k) /\
      (forall k. CO.lt k k0 /\ lf.domn k -> lf.func k = t.func k) /\
      (forall k. CO.le k0 k -> not lf.domn k) /\
      (forall k. CO.lt k0 k -> rg.domn k <-> t.domn k) /\
      (forall k. CO.lt k0 k /\ rg.domn k -> rg.func k = t.func k) /\
      (forall k. CO.le k k0 -> not rg.domn k) /\
      match o with
      | None -> t.card = lf.card + rg.card /\
        (forall k. CO.eq k k0 -> not t.domn k) /\
        not t.domn k0
      | Some d -> t.card = lf.card + rg.card + 1 /\
        CO.eq d.key k0 /\
        (forall k. CO.eq k k0 -> t.domn k /\ t.func k = d)
        /\ t.domn k0 /\ t.func k0 = d
      end }
  = let lf,o,rg = Sel.split (Sel.default_split ()) k0 t.field in
    ({ field = lf }, o, { field = rg })

Split the table in three: elements before the key, element associated to the key (if exists), elements after the key.

Extension with set-theoretic routines

Those routines go beyond single-call to the AVL trees function. Also, unlike previous routines they are not logarithmic-time but linear-time instead.

  type view 'a =
    | AEmpty
    | ANode (t 'a) (D.t 'a) (t 'a) I.t

Internal specification wrappers over the AVL view and join routines.

  let view (t:t 'a) : view 'a
    returns { AEmpty -> t.card = 0 /\ forall k:K.t. not t.domn k
      | ANode l d r h ->
        t.card = 1 + l.card + r.card
        /\ h = t.field.Sel.hgt
        /\ let k0 = d.key in
           (forall k. CO.lt k k0 -> l.domn k <-> t.domn k)
        /\ (forall k. CO.lt k k0 /\ l.domn k -> l.func k = t.func k)
        /\ (forall k. CO.le k0 k -> not l.domn k)
        /\ (forall k. CO.lt k0 k -> r.domn k <-> t.domn k)
        /\ (forall k. CO.lt k0 k /\ r.domn k -> r.func k = t.func k)
        /\ (forall k. CO.le k k0 -> not r.domn k)
        /\ (forall k. CO.eq k k0 -> t.domn k /\ t.func k = d)
        /\ t.domn k0 /\ t.func k0 = d }
  = match Sel.view t.field with
    | Sel.AEmpty -> AEmpty
    | Sel.ANode l d r h _ -> ANode { field = l } d { field = r } h
    end

  let join (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a
    requires { forall k. l.domn k -> CO.lt k d.key }
    requires { forall k. r.domn k -> CO.lt d.key k }
    ensures { forall k. CO.lt k d.key -> result.domn k <-> l.domn k }
    ensures { forall k. CO.lt k d.key /\ result.domn k ->
      result.func k = l.func k }
    ensures { forall k. CO.lt d.key k -> result.domn k <-> r.domn k }
    ensures { forall k. CO.lt d.key k /\ result.domn k ->
      result.func k = r.func k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { result.card = 1 + l.card + r.card }
  = let ghost s = { left = l.field.Sel.m.Sel.seq;
                    middle = Some d;
                    right = r.field.Sel.m.Sel.seq }
    in
    assert { selected d.key s };
    { field = Sel.join l.field d r.field }

  let rec add_all (a:t 'a) (t:t 'a) : t 'a
    ensures { forall k. result.domn k <-> a.domn k \/ t.domn k }
    ensures { forall k. a.domn k -> result.func k = a.func k }
    ensures { forall k. t.domn k /\ not a.domn k -> result.func k = t.func k }
    ensures { result.card >= a.card /\ result.card >= t.card }
    ensures { result.card <= a.card + t.card }
    variant { a.m.card + t.m.card }
  = match view a with
    | AEmpty -> t
    | ANode al ad ar ah -> match view t with
      | AEmpty -> a
      | ANode tl td tr th -> if I.le ah th
        then let (al,ad,ar) = split td.key a in
          let ul = add_all al tl in
          let ur = add_all ar tr in
          let ud = match ad with
            | None -> td
            | Some ad -> ad
            end in
          join ul ud ur
        else let (tl,_,tr) = split ad.key t in
          let ul = add_all al tl in
          let ur = add_all ar tr in
          join ul ad ur
      end
    end

Add every element from a into t.

  let rec filter (p:t 'b) (a:t 'a) : t 'a
    ensures { forall k. result.domn k <-> a.domn k /\ p.domn k }
    ensures { forall k. result.domn k -> result.func k = a.func k }
    ensures { result.m.card <= a.m.card /\ result.m.card <= p.m.card }
    variant { a.m.card + p.m.card }
  = match view a with
    | AEmpty -> a
    | ANode al ad ar ah -> match view p with
      | AEmpty -> empty ()
      | ANode pl pd pr ph -> if I.le ah ph
        then let (al,ad,ar) = split pd.key a in
          let fl = filter pl al in
          let fr = filter pr ar in
          match ad with
          | None -> ordered_union fl fr
          | Some ad -> join fl ad fr
          end
        else let (pl,pd,pr) = split ad.key p in
          let fl = filter pl al in
          let fr = filter pr ar in
          match pd with
          | None -> ordered_union fl fr
          | _ -> join fl ad fr
          end
      end
    end

Create the table with the elements of a whose key appear in p.

  let rec remove_all (p:t 'b) (a:t 'a) : t 'a
    ensures { forall k. result.domn k <-> a.domn k /\ not p.domn k }
    ensures { forall k. result.domn k -> result.func k = a.func k }
    ensures { result.m.card <= a.m.card }
    variant { a.m.card + p.m.card }
  = match view a with
    | AEmpty -> a
    | ANode al ad ar ah -> match view p with
      | AEmpty -> a
      | ANode pl pd pr ph -> if I.le ah ph
        then let (al,_,ar) = split pd.key a in
          let fl = remove_all pl al in
          let fr = remove_all pr ar in
          ordered_union fl fr
        else let (pl,pd,pr) = split ad.key p in
          let fl = remove_all pl al in
          let fr = remove_all pr ar in
          match pd with
          | None -> join fl ad fr
          | _ -> ordered_union fl fr
          end
      end
    end

Complement of filter: remove from a every element whose key appear in p.

  let rec symdiff (a b:t 'a) : t 'a
    ensures { forall k. result.domn k <-> not (a.domn k <-> b.domn k) }
    ensures { forall k. result.domn k /\ a.domn k -> result.func k = a.func k }
    ensures { forall k. result.domn k /\ b.domn k -> result.func k = b.func k }
    ensures { result.m.card <= a.m.card + b.m.card }
    variant { a.m.card + b.m.card }
  = match view a with
    | AEmpty -> b
    | ANode al ad ar ah -> match view b with
      | AEmpty -> a
      | ANode bl bd br bh -> if I.le ah bh
        then let (al,ad,ar) = split bd.key a in
          let sl = symdiff al bl in
          let sr = symdiff ar br in
          match ad with
          | None -> join sl bd sr
          | _ -> ordered_union sl sr
          end
        else let (bl,bd,br) = split ad.key b in
          let sl = symdiff al bl in
          let sr = symdiff ar br in
          match bd with
          | None -> join sl ad sr
          | _ -> ordered_union sl sr
          end
      end
    end

Create a table with the elements that appear exactly in one of a and b, but not both.

end

module Map

Instantiation of the base to key-value ordered associative tables

  use int.Int
  use option.Option
  use ref.Ref
  use mach.peano.Peano as I

  val constant balancing : I.t
    ensures { result > 0 }

  scope K type t end
  clone preorder.Computable as CO with type t = K.t, axiom .

Parameter: key type with computable total preorder.

  scope D
    type t 'a = (K.t,'a)
    let function key (t:t 'a) : K.t = let (a,_) = t in a
  end

Elements are key-value pairs

  clone MapBase as MB with val balancing = balancing,
    type K.t = K.t,
    type D.t = D.t,
    val key = D.key,
    predicate CO.le = CO.le,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    predicate CO.lt = CO.lt,
    goal CO.lt_def,
    predicate CO.eq = CO.eq,
    goal CO.eq_def,
    val CO.compare = CO.compare

Direct instantiation.

  type t 'a = MB.t 'a
  type m 'a = {
    domn : K.t -> bool;
    func : K.t -> 'a;
    card : int;
  }
  function m (t:t 'a) : m 'a =
    { domn = t.MB.domn;
      func = fun k -> let (_,v) = t.MB.func k in v;
      card = t.MB.m.MB.card }
  meta coercion function m

Slight adaptation of the logical model (get rid of keys in the output)

  let lemma correction (t:t 'a)
    ensures { forall k1 k2. CO.eq k1 k2 -> t.domn k1 <-> t.domn k2 }
    ensures { forall k1 k2. CO.eq k1 k2 /\ t.domn k1 -> t.func k1 = t.func k2 }
  = ()

  let empty () : t 'a
    ensures { forall k. not result.domn k }
    ensures { result.card = 0 }
  = MB.empty ()

  let singleton (k0:K.t) (v:'a) : t 'a
    ensures { forall k. result.domn k <-> CO.eq k k0 }
    ensures { forall k. CO.eq k k0 -> result.func k = v }
    ensures { result.domn k0 /\ result.func k0 = v }
    ensures { result.card = 1 }
  = MB.singleton (k0,v)

Create a table with a single key->value binding.

  let is_empty (ghost rk:ref K.t) (t:t 'a) : bool
    ensures { result -> forall k. not t.domn k }
    ensures { not result -> t.domn !rk }
    ensures { result <-> t.m.card = 0 }
  = MB.is_empty rk t

Check emptyness of a table.

  let min_binding (t:t 'a) : (K.t,'a)
    requires { t.card > 0 }
    returns  { (k,v) -> t.domn k /\ t.func k = v
      /\ forall k2. t.domn k2 -> CO.le k k2 }
  = MB.min t

  let max_binding (t:t 'a) : (K.t,'a)
    requires { t.card > 0 }
    returns  { (k,v) -> t.domn k /\ t.func k = v
      /\ forall k2. t.domn k2 -> CO.le k2 k }
  = MB.max t

  let decompose_min (t:t 'a) : option ((K.t,'a),t 'a)
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some ((k0,v),r:t 'a) -> t.card = r.card + 1 /\
        t.domn k0 /\ t.func k0 = v /\ not r.domn k0 /\
        (forall k. CO.lt k k0 -> not t.domn k) /\
        (forall k. CO.eq k k0 -> t.func k = v) /\
        (forall k. CO.le k k0 -> not r.domn k) /\
        (forall k. CO.lt k0 k -> r.domn k <-> t.domn k) /\
        (forall k. CO.lt k0 k /\ r.domn k -> r.func k = t.func k) }
  = MB.decompose_min t

Get and extract the (key->value) binding with minimum key.

  let decompose_max (t:t 'a) : option (t 'a,(K.t,'a))
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (l:t 'a,(k0,v)) -> t.card = l.card + 1 /\
        t.domn k0 /\ t.func k0 = v /\ not l.domn k0 /\
        (forall k. CO.lt k0 k -> not t.domn k) /\
        (forall k. CO.eq k k0 -> t.func k = v) /\
        (forall k. CO.le k0 k -> not l.domn k) /\
        (forall k. CO.lt k k0 -> l.domn k <-> t.domn k) /\
        (forall k. CO.lt k k0 /\ l.domn k -> l.func k = t.func k) }
  = MB.decompose_max t

Get and extract the (key->value) binding with maximum key.

  let add_min_binding (k0:K.t) (v:'a) (t:t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt k0 k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k k0 -> not result.domn k }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { forall k. CO.lt k0 k -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k0 k /\ result.domn k ->
      result.func k = t.func k }
    ensures { result.domn k0 /\ result.func k0 = v }
  = MB.add_min (k0,v) t

Add a key->value binding with minimal key.

  let add_max_binding (k0:K.t) (v:'a) (t:t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt k k0 }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k0 k -> not result.domn k }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { forall k. CO.lt k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k k0 /\ result.domn k ->
      result.func k = t.func k }
    ensures { result.domn k0 /\ result.func k0 = v }
  = MB.add_max t (k0,v)

Add a key->value binding with maximal key.

  let ordered_join (l r:t 'a) : t 'a
    requires { forall k1 k2. l.domn k1 /\ r.domn k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.domn k <-> l.domn k \/ r.domn k }
    ensures  { forall k. result.domn k /\ l.domn k -> result.func k = l.func k }
    ensures  { forall k. result.domn k /\ r.domn k -> result.func k = r.func k }
    ensures  { result.card = l.card + r.card }
  = MB.ordered_union l r

Ordered fusion of two associative tables.

  let get (k:K.t) (t:t 'a) : option 'a
    returns { None -> not t.domn k
      | Some v -> t.card > 0 /\ t.domn k /\ t.func k = v }
  = match MB.get k t with
    | None -> None
    | Some (_,v) -> Some v
    end

Extract the value associated to some key.

  let insert (k0:K.t) (v:'a) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card else t.card + 1 }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { result.domn k0 /\ result.func k0 = v }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = MB.insert (k0,v) t

Set the binding for key k, erasing any such previous binding.

  let remove (k0:K.t) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.domn k }
    ensures { not result.domn k0 }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = MB.remove k0 t

Erase any potential binding for key k.

  let split (k0:K.t) (t:t 'a) : (t 'a,option 'a,t 'a)
    returns { (lf:t 'a,o,rg:t 'a) ->
      (forall k. CO.lt k k0 -> lf.domn k <-> t.domn k) /\
      (forall k. CO.lt k k0 /\ lf.domn k -> lf.func k = t.func k) /\
      (forall k. CO.le k0 k -> not lf.domn k) /\
      (forall k. CO.lt k0 k -> rg.domn k <-> t.domn k) /\
      (forall k. CO.lt k0 k /\ rg.domn k -> rg.func k = t.func k) /\
      (forall k. CO.le k k0 -> not rg.domn k) /\
      match o with
      | None -> t.card = lf.card + rg.card /\
        (forall k. CO.eq k k0 -> not t.domn k) /\
        not t.domn k0
      | Some v -> t.card = lf.card + rg.card + 1 /\
        (forall k. CO.eq k k0 -> t.domn k /\ t.func k = v)
        /\ t.domn k0 /\ t.func k0 = v
      end }
  = let (lf,o,rg) = MB.split k0 t in
    let o = match o with None -> None | Some (_,v) -> Some v end in
    (lf,o,rg)

Split the table in three parts: Bindings with key lower than k, value associated to k, and bindings with key greater than k.

end

module Set

Instantiation of the base to ordered sets

  use int.Int
  use option.Option
  use ref.Ref
  use import mach.peano.Peano as I

  val constant balancing : I.t
    ensures { result > 0 }

The balancing level is left abstract.

  scope K type t end
  clone preorder.Computable as CO with type t = K.t, axiom .

Parameter: comparable elements.

  scope D
    type t 'a = K.t
    let function key (x:'a) : 'a = x
  end

Elements are themselves the keys.

  clone MapBase as MB with val balancing = balancing,
    type K.t = K.t,
    type D.t = D.t,
    val key = D.key,
    predicate CO.le = CO.le,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    predicate CO.lt = CO.lt,
    goal CO.lt_def,
    predicate CO.eq = CO.eq,
    goal CO.eq_def,
    val CO.compare = CO.compare

Actual instantiation.

  type t = MB.t unit
  function set (m:MB.m unit) : K.t -> bool = m.MB.domn
  function card (m:MB.m unit) : int = m.MB.card

Minor adaptation of the logical model: only keep the set of elements. In fact, the functions from MapBase can been used as-is (but may be over-specifications) The following specifications wrappers are only given for demonstration.

  let lemma correction (t:t) : unit
    ensures { forall k1 k2:K.t. CO.eq k1 k2 -> t.set k1 <-> t.set k2 }
    ensures { t.card >= 0 }
  = ()

Invariant on the logical model.

  let empty () : t
    ensures { forall k. not result.set k }
    ensures { result.card = 0 }
  = MB.empty ()

Create an empty set.

  let singleton (k0:K.t) : t
    ensures { forall k. result.set k <-> CO.eq k k0 }
    ensures { result.set k0 }
    ensures { result.card = 1 }
  = MB.singleton k0

Create a singleton set.

  let is_empty (ghost rk:ref K.t) (t:t) : bool
    ensures { result -> forall k. not t.set k }
    ensures { not result -> t.set !rk }
    ensures { result <-> t.card = 0 }
  = MB.is_empty rk t

Test emptyness of a set.

  let min_elt (t:t) : K.t
    requires { t.card > 0 }
    ensures  { t.set result }
    ensures  { forall k. t.set k -> CO.le result k }
  = MB.min t

Minimum element of a set.

  let max_elt (t:t) : K.t
    requires { t.card > 0 }
    ensures  { t.set result }
    ensures  { forall k. t.set k -> CO.le k result }
  = MB.max t

Maximum element of a set.

  let decompose_min (t:t) : option (K.t,t)
    returns { None -> t.card = 0 /\ forall k. not t.set k
      | Some (k0,r:t) -> t.card = r.card + 1 /\
        t.set k0 /\ not r.set k0 /\
        (forall k. CO.lt k k0 -> not t.set k) /\
        (forall k. CO.le k k0 -> not r.set k) /\
        (forall k. CO.lt k0 k -> r.set k <-> t.set k) }
  = MB.decompose_min t

Get and remove minimum element from a set.

  let decompose_max (t:t) : option (t,K.t)
    returns { None -> t.card = 0 /\ forall k. not t.set k
      | Some (l:t,k0) -> t.card = l.card + 1 /\
        t.set k0 /\ not l.set k0 /\
        (forall k. CO.lt k0 k -> not t.set k) /\
        (forall k. CO.le k0 k -> not l.set k) /\
        (forall k. CO.lt k0 k -> l.set k <-> t.set k) }
  = MB.decompose_max t

Get and remove maximum element from a set.

  let add_min_elt (k0:K.t) (t:t) : t
    requires { forall k. t.set k -> CO.lt k0 k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k k0 -> not result.set k }
    ensures { forall k. CO.lt k0 k -> result.set k <-> t.set k }
  = MB.add_min k0 t

Add minimal element to a set.

  let add_max_elt (t:t) (k0:K.t) : t
    requires { forall k. t.set k -> CO.lt k k0 }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k0 k -> not result.set k }
    ensures { forall k. CO.lt k k0 -> result.set k <-> t.set k }
  = MB.add_max t k0

Add maximal element to a set.

  let ordered_union (l r:t) : t
    requires { forall k1 k2. l.set k1 /\ r.set k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.set k <-> l.set k \/ r.set k }
    ensures  { result.card = l.card + r.card }
  = MB.ordered_union l r

Ordered union of two sets.

  let mem (k0:K.t) (t:t) : bool
    ensures { result <-> t.set k0 }
    ensures { result -> forall k. CO.eq k k0 -> t.set k }
    ensures { forall k. CO.eq k k0 /\ t.set k -> result }
    ensures { result -> t.card > 0 }
  = match MB.get k0 t with None -> false | _ -> true end

Test membership of an element.

  let add (k0:K.t) (t:t) : t
    ensures { result.card = if t.set k0 then t.card else t.card + 1 }
    ensures { forall k. CO.eq k k0 -> result.set k }
    ensures { result.set k0 }
    ensures { forall k. not CO.eq k k0 -> result.set k <-> t.set k }
  = MB.insert k0 t

Add an element to a set.

  let remove (k0:K.t) (t:t) : t
    ensures { result.card = if t.set k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.set k }
    ensures { not result.set k0 }
    ensures { forall k. not CO.eq k k0 -> result.set k <-> t.set k }
  = MB.remove k0 t

Remove an element from a set.

  let split (k0:K.t) (t:t) : (t,bool,t)
    returns { (lf:t,b,rg:t) ->
      (forall k. CO.lt k k0 -> lf.set k <-> t.set k) /\
      (forall k. CO.le k0 k -> not lf.set k) /\
      (forall k. CO.lt k0 k -> rg.set k <-> t.set k) /\
      (forall k. CO.le k k0 -> not rg.set k) /\
      t.card = lf.card + rg.card + (if b then 1 else 0) /\
      (b <-> t.set k0) /\
      (b -> forall k. CO.eq k k0 -> t.set k) /\
      (forall k. CO.eq k k0 /\ t.set k -> b)
    }
  = let (lf,o,rg) = MB.split k0 t in
    let b = match o with None -> false | _ -> true end in
    (lf,b,rg)

Split the set into three parts: elements lower than k, elements equal to k, and elements bigger than k

Extension: set-theoretic routines.

  let union (a b:t) : t
    ensures { forall k. result.set k <-> a.set k \/ b.set k }
    ensures { result.card >= a.card /\ result.card >= b.card }
    ensures { result.card <= a.card + b.card }
  = MB.add_all a b

Compute the union of two sets.

  let inter (a b:t) : t
    ensures { forall k. result.set k <-> a.set k /\ b.set k }
    ensures { result.card <= a.card /\ result.card <= b.card }
  = MB.filter a b

Compute the intersection of two sets.

  let diff (a b:t) : t
    ensures { forall k. result.set k <-> a.set k /\ not b.set k }
    ensures { result.card <= a.card }
  = MB.remove_all b a

Compute the difference of two sets.

  let symdiff (a b:t) : t
    ensures { forall k. result.set k <-> not (a.set k <-> b.set k) }
    ensures { result.card <= a.card + b.card }
  = MB.symdiff a b

Compute the symmetrical difference of two sets.

end

module IMapAndSet

Example instances: integer keys/elements

  use int.Int
  use mach.peano.Peano as I

  scope K type t = int end

  let constant balancing : I.t = I.succ I.zero

  predicate le (x y:int) = x <= y
  predicate eq (x y:int) = x = y
  predicate lt (x y:int) = x < y

  let compare (x y:int) : int ensures { result = x - y } = x - y

  clone Map as M with val balancing = balancing,
    type K.t = K.t,
    predicate CO.le = le,
    predicate CO.lt = lt,
    predicate CO.eq = eq,
    goal CO.lt_def,
    goal CO.eq_def,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    val CO.compare = compare

  clone Set as S with val balancing = balancing,
    type K.t = K.t,
    predicate CO.le = le,
    predicate CO.lt = lt,
    predicate CO.eq = eq,
    goal CO.lt_def,
    goal CO.eq_def,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    val CO.compare = compare

end

Generated by why3doc 1.7.0