why3doc index index
Author: Martin Clochard
module MapBase use import int.Int use import avl.SelectionTypes use import option.Option use import ref.Ref use import list.List use import list.Append use import list.Mem use import list.Length
The level of balancing is left abstract.
constant balancing : int axiom balancing_positive : balancing > 0
Stored elements are identified by totally ordered keys
namespace D type t 'a end namespace K type t end clone export key_type.ProgramKeyType with type t = D.t, type key = K.t clone preorder.Computable as CO with type t = K.t namespace D function measure 'a : unit = () let measure (x:'c) : unit ensures { result = () } = () end
Import the definition/facts about association list. Required to link together the sequence and functional views.
clone association_list.AssocSorted as A with type K.t = D.t, type K.key = K.t, function K.key = key, predicate O.le = CO.le, goal O.Refl, goal O.Trans, predicate O.eq = CO.eq, goal O.eq_def, predicate O.lt = CO.lt, goal O.lt_def
As we do not need any extra information in order to perform search for this particular instance, we instantiate the monoid by unit.
namespace 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
In associative tables, elements are selected with respect to their keys.
type selector = K.t
Efficient search for ordered keys can be carried out efficiently only in sorted sequences.
predicate selection_possible (s:K.t) (l:list (D.t 'a)) = A.S.increasing l
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
predicate selected (s:K.t) (e:split (D.t 'a)) = let l = rebuild e in (A.S.upper_bound s e.left /\ A.S.lower_bound s e.right /\ match e.middle with | None -> true | Some d2 -> CO.eq s d2.key end) (* Strictly speaking, not necessary because derivable from the context, but makes easier to write some lemmas. *) /\ A.S.increasing e.left /\ A.S.increasing e.right /\ selection_possible s l
Alternative definition of selected based on the functional view of an association list.
predicate selected_sem (s:K.t) (e:split (D.t 'a)) (l:list (D.t 'a)) = forall k:K.t. (CO.lt k s -> A.model l k = A.model e.left k) /\ (CO.lt s k -> A.model l k = A.model e.right k) /\ (CO.eq k s -> A.model l k = e.middle) /\ (CO.le s k -> A.model e.left k = None) /\ (CO.le k s -> A.model e.right k = None) let lemma selected_sem (s:K.t) (e:split (D.t 'a)) : unit requires { selected s e } ensures { selected_sem s e (rebuild e) } = match e.middle with | None -> A.model_cut s e.left e.right | Some d -> A.model_split d e.left e.right end
Comparison-based binary search
let selected_part (ghost llis:list (D.t 'a)) (ghost rlis:list (D.t 'a)) (s:K.t) (l:'e) (d:D.t 'a) (r:'f) : part_base K.t requires { selection_possible s (llis ++ Cons d rlis) } returns { Here -> let e2 = { left = llis; middle = Some d; right = rlis } in selected s e2 | Left sl -> selection_possible sl llis /\ forall e. selected sl e /\ rebuild e = llis -> selected s (right_extend e d rlis) | Right sr -> selection_possible sr rlis /\ forall e. selected sr e /\ rebuild e = rlis -> selected s (left_extend llis d e) } = let kd = get_key d in let cmp = CO.compare s kd in if cmp < 0 then Left s else if cmp > 0 then Right s else Here
Full instantiation of the avl module.
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, constant balancing = balancing, goal balancing_positive, type D.t = D.t, function D.measure = D.measure, 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.sum = M.sum, goal M.sum_def_nil, goal M.sum_def_cons, val M.zero = M.zero, val M.op = M.op (*{3 Adaptation to the specification to associative tables}*) type t 'a = Sel.t 'a
Logical model: a finite association from keys to elements.
type m 'a = { func : K.t -> option (D.t 'a); card : int; } function m (t:t 'a) : m 'a = { func = A.model t.Sel.m.Sel.lis; card = length t.Sel.m.Sel.lis } let ghost m (t:t 'a) : m 'a ensures { result = t.m } = { func = A.model t.Sel.m.Sel.lis; card = length t.Sel.m.Sel.lis } let lemma m_def (t:t 'a) : unit ensures { t.m.func = A.model t.Sel.m.Sel.lis } ensures { t.m.card = length t.Sel.m.Sel.lis } = ()
Invariant: add sortedness to the AVL trees invariant.
predicate c (t:t 'a) = Sel.c t /\ A.S.increasing t.Sel.m.Sel.lis
Logical invariant on the model.
let lemma correction (t:t 'a) : unit requires { c t } ensures { forall k1 k2:K.t. CO.eq k1 k2 -> t.m.func k1 = t.m.func k2 } ensures { forall k:K.t. match t.m.func k with | None -> true | Some d -> CO.eq k d.key end } ensures { t.m.card >= 0 } = ()
Create an empty associative table.
let empty () : t 'a ensures { forall k:K.t. result.m.func k = None } ensures { result.m.card = 0 /\ c result } = Sel.empty ()
Create an associative table with a single element.
let singleton (d:D.t 'a) : t 'a ensures { (forall k:K.t. if CO.eq k d.key then result.m.func k = Some d else result.m.func k = None) && result.m.func d.key = Some d } ensures { result.m.card = 1 /\ c result } = Sel.singleton d
Check emptyness of an associative table.
let is_empty (ghost rd:ref (D.t 'a)) (t:t 'a) : bool requires { c t } ensures { result -> forall k:K.t. t.m.func k = None } ensures { not result -> t.m.func (key !rd) = Some !rd } ensures { result <-> t.m.card = 0 } = let res = Sel.is_empty t in ghost if not res then match t.Sel.m.Sel.lis with | Nil -> absurd | Cons d _ -> rd := d end; res
Get and extract the element with minimum key from the table.
let decompose_min (t:t 'a) : option (D.t 'a,t 'a) requires { c t } returns { None -> (forall k:K.t. t.m.func k = None) /\ t.m.card = 0 | Some (d,r) -> t.m.card = r.m.card + 1 /\ (forall k:K.t. (CO.lt k d.key -> t.m.func k = None) /\ (CO.eq k d.key -> t.m.func k = Some d) /\ (CO.le k d.key -> r.m.func k = None) /\ (not CO.eq d.key k -> r.m.func k = t.m.func k)) && t.m.func d.key = Some d && r.m.func d.key = None /\ c r } = Sel.decompose_front t
Get and extract the element with maximum key from the table.
let decompose_max (t:t 'a) : option (t 'a,D.t 'a) requires { c t } returns { None -> (forall k:K.t. t.m.func k = None) /\ t.m.card = 0 | Some (l,d) -> t.m.card = l.m.card + 1 /\ (forall k:K.t. (CO.lt d.key k -> t.m.func k = None) /\ (CO.eq d.key k -> t.m.func k = Some d) /\ (CO.le d.key k -> l.m.func k = None) /\ (not CO.eq k d.key -> l.m.func k = t.m.func k)) && t.m.func d.key = Some d && l.m.func d.key = None /\ c l } = Sel.decompose_back t
Optimized insertion of an element with minimum key.
let add_min (d:D.t 'a) (t:t 'a) : t 'a requires { c t /\ forall k:K.t. CO.le k d.key -> t.m.func k = None } ensures { (forall k:K.t. (CO.lt k d.key -> result.m.func k = None) /\ (CO.eq k d.key -> result.m.func k = Some d) /\ (not CO.eq d.key k -> result.m.func k = t.m.func k)) && t.m.func d.key = None && result.m.func d.key = Some d } ensures { result.m.card = t.m.card + 1 /\ c result } = Sel.cons d t
Optimized insertion of an element with maximal key.
let add_max (t:t 'a) (d:D.t 'a) : t 'a requires { c t /\ forall k:K.t. CO.le d.key k -> t.m.func k = None } ensures { (forall k:K.t. (CO.lt d.key k -> result.m.func k = None) /\ (CO.eq k d.key -> result.m.func k = Some d) /\ (not CO.eq d.key k -> result.m.func k = t.m.func k)) && t.m.func d.key = None && result.m.func d.key = Some d } ensures { result.m.card = t.m.card + 1 /\ c result } = Sel.snoc t d
Ordered union of two associative table.
let concat (l r:t 'a) : t 'a requires { c l /\ c r } requires { forall k1 k2. l.m.func k1 <> None /\ r.m.func k2 <> None -> CO.lt k1 k2 } ensures { forall k. match l.m.func k with | None -> result.m.func k = r.m.func k | s -> result.m.func k = s end } ensures { forall k. match r.m.func k with | None -> result.m.func k = l.m.func k | s -> result.m.func k = s end } ensures { forall k. (result.m.func k = None <-> l.m.func k = None /\ r.m.func k = None) } ensures { result.m.card = l.m.card + r.m.card /\ c result } = Sel.concat l r
Get the value associated to a key in the table, if it exists.
let get (k:K.t) (t:t 'a) : option (D.t 'a) requires { c t } returns { None -> (forall k2. CO.eq k k2 -> t.m.func k2 = None) && t.m.func k = None | Some d -> t.m.card > 0 /\ CO.eq d.key k /\ (forall k2. CO.eq k k2 -> t.m.func k2 = Some d) && t.m.func k = Some d = t.m.func d.key } = Sel.get (Sel.default_split ()) k t
Insert a value in the table. Erase binding if the key was already present.
let insert (d:D.t 'a) (t:t 'a) : t 'a requires { c t } ensures { (if t.m.func d.key = None then result.m.card = t.m.card + 1 else result.m.card = t.m.card) /\ (forall k:K.t. (CO.eq k d.key -> result.m.func k = Some d) /\ (not CO.eq k d.key -> result.m.func k = t.m.func k)) && result.m.func d.key = Some d /\ t.m.card <= result.m.card /\ c result } = Sel.insert (Sel.default_split ()) (get_key d) d t
Erase any binding associated to the given key.
let remove (k:K.t) (t:t 'a) : t 'a requires { c t } ensures { (if t.m.func k = None then t.m.card = result.m.card else t.m.card = result.m.card + 1) /\ (forall k2:K.t. (CO.eq k2 k -> result.m.func k2 = None) /\ (not CO.eq k2 k -> result.m.func k2 = t.m.func k2)) && result.m.func k = None /\ result.m.card <= t.m.card /\ c result } = Sel.remove (Sel.default_split ()) k t
Split the table in three: elements before the key, element associated to the key (if exists), elements after the key.
let split (k:K.t) (t:t 'a) : (t 'a,option (D.t 'a),t 'a) requires { c t } returns { (lf,o,rg) -> match o with | None -> (forall k2:K.t. CO.eq k k2 -> t.m.func k2 = None) && t.m.func k = None | Some d -> CO.eq k d.key /\ (forall k2:K.t. CO.eq k k2 -> t.m.func k2 = Some d) && t.m.func k = Some d = t.m.func d.key end /\ ((if o = None then t.m.card = lf.m.card + rg.m.card else t.m.card = 1 + (lf.m.card + rg.m.card)) && t.m.card >= lf.m.card + rg.m.card) /\ c lf /\ c rg /\ (forall k2:K.t. CO.lt k2 k -> lf.m.func k2 = t.m.func k2) /\ (forall k2:K.t. CO.le k k2 -> lf.m.func k2 = None) /\ (forall k2:K.t. CO.lt k k2 -> rg.m.func k2 = t.m.func k2) /\ (forall k2:K.t. CO.le k2 k -> rg.m.func k2 = None) } = Sel.split (Sel.default_split ()) k t
Those routines go beyond single-call to the AVL trees function. Also, unlike previous routines they are not logarithmic-time but linear-time instead.
Internal specification wrappers over the AVL view and join routines.
let view (t:t 'a) : Sel.view 'a requires { c t } returns { Sel.AEmpty -> t.m.card = 0 /\ forall k:K.t. t.m.func k = None | Sel.ANode l d r _ _ -> t.m.card = 1 + l.m.card + r.m.card /\ c l /\ c r /\ forall k:K.t. (CO.lt k d.key -> t.m.func k = l.m.func k) /\ (CO.lt d.key k -> t.m.func k = r.m.func k) /\ (CO.eq k d.key -> t.m.func k = Some d) /\ (CO.le d.key k -> l.m.func k = None) /\ (CO.le k d.key -> r.m.func k = None) } = Sel.view t let join (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a requires { c l /\ c r } requires { forall k:K.t. (l.m.func k <> None -> CO.lt k d.key) /\ (r.m.func k <> None -> CO.lt d.key k) } ensures { forall k:K.t. (CO.lt k d.key -> result.m.func k = l.m.func k) /\ (CO.lt d.key k -> result.m.func k = r.m.func k) /\ (CO.eq k d.key -> result.m.func k = Some d) } ensures { result.m.card = 1 + l.m.card + r.m.card /\ c result } = Sel.join l d r
Add every element from a
into t
.
let rec add_all (a:t 'a) (t:t 'a) : t 'a requires { c a /\ c t } ensures { forall k. if a.m.func k = None then result.m.func k = t.m.func k else result.m.func k = a.m.func k } ensures { result.m.card >= a.m.card /\ result.m.card >= t.m.card } ensures { c result } variant { a.m.card + t.m.card } = match view a with | Sel.AEmpty -> t | Sel.ANode al ad ar ah _ -> match view t with | Sel.AEmpty -> a | Sel.ANode tl td tr th _ -> if ah <= th then let (al,ad,ar) = split (get_key td) 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 (get_key ad) t in let ul = add_all al tl in let ur = add_all ar tr in join ul ad ur end end
Create the table with the elements of a
whose key appear in p
.
let rec filter (p:t 'b) (a:t 'a) : t 'a requires { c a /\ c p } ensures { forall k. if p.m.func k = None then result.m.func k = None else result.m.func k = a.m.func k } ensures { result.m.card <= a.m.card /\ result.m.card <= p.m.card } ensures { c result } variant { a.m.card + p.m.card } = match view a with | Sel.AEmpty -> a | Sel.ANode al ad ar ah _ -> match view p with | Sel.AEmpty -> empty () | Sel.ANode pl pd pr ph _ -> if ah <= ph then let (al,ad,ar) = split (get_key pd) a in let fl = filter pl al in let fr = filter pr ar in match ad with | None -> concat fl fr | Some ad -> join fl ad fr end else let (pl,pd,pr) = split (get_key ad) p in let fl = filter pl al in let fr = filter pr ar in match pd with | None -> concat fl fr | _ -> join fl ad fr end end end
Complement of filter
: remove from a
every element whose
key appear in p
.
let rec remove_all (p:t 'b) (a:t 'a) : t 'a requires { c a /\ c p } ensures { forall k. if p.m.func k = None then result.m.func k = a.m.func k else result.m.func k = None } ensures { result.m.card <= a.m.card /\ c result } variant { a.m.card + p.m.card } = match view a with | Sel.AEmpty -> a | Sel.ANode al ad ar ah _ -> match view p with | Sel.AEmpty -> a | Sel.ANode pl pd pr ph _ -> if ah <= ph then let (al,_,ar) = split (get_key pd) a in let fl = remove_all pl al in let fr = remove_all pr ar in concat fl fr else let (pl,pd,pr) = split (get_key ad) p in let fl = remove_all pl al in let fr = remove_all pr ar in match pd with | None -> join fl ad fr | _ -> concat fl fr end end end
Create a table with the elements that appear
exactly in one of a
and b
, but not both.
let rec symdiff (a b:t 'a) : t 'a requires { c a /\ c b } ensures { forall k. (a.m.func k = None -> result.m.func k = b.m.func k) /\ (b.m.func k = None -> result.m.func k = a.m.func k) /\ (a.m.func k <> None /\ b.m.func k <> None -> result.m.func k = None) } ensures { result.m.card <= a.m.card + b.m.card /\ c result } variant { a.m.card + b.m.card } = match view a with | Sel.AEmpty -> b | Sel.ANode al ad ar ah _ -> match view b with | Sel.AEmpty -> a | Sel.ANode bl bd br bh _ -> if ah <= bh then let (al,ad,ar) = split (get_key bd) a in let sl = symdiff al bl in let sr = symdiff ar br in match ad with | None -> join sl bd sr | _ -> concat sl sr end else let (bl,bd,br) = split (get_key ad) b in let sl = symdiff al bl in let sr = symdiff ar br in match bd with | None -> join sl ad sr | _ -> concat sl sr end end end end
module Map use import int.Int use import option.Option use import ref.Ref
Balancing level left abstract.
constant balancing : int axiom balancing_positive : balancing > 0
Parameter: key type with computable total preorder.
namespace K type t end clone preorder.Computable as CO with type t = K.t
Elements are key-value pairs.
namespace D type t 'a = (K.t,'a) function key (t:t 'a) : K.t = let (a,_) = t in a let get_key (t:t 'a) : K.t ensures { key t = result } = let (a,_) = t in a end
Direct instantiation.
clone MapBase as MB with constant balancing = balancing, goal balancing_positive, type K.t = K.t, type D.t = D.t, function key = D.key, val get_key = D.get_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
Slight adaptation of the logical model.
type t 'a = MB.t 'a type m 'a = { func : K.t -> option 'a; card : int; } predicate c (t:t 'a) = MB.c t function oproj (o:option ('a,'b)) : option 'b = match o with | None -> None | Some (_,v) -> Some v end function m (t:t 'a) : m 'a = { func = \k. oproj (t.MB.m.MB.func k); card = t.MB.m.MB.card } let lemma m_def (t:t 'a) : unit ensures { forall k. t.m.func k = None <-> t.MB.m.MB.func k = None } ensures { forall k k2 v. t.MB.m.MB.func k = Some (k2,v) -> t.m.func k = Some v } ensures { forall k v. t.m.func k = Some v -> exists k2. t.MB.m.MB.func k = Some (k2,v) /\ CO.eq k k2 } ensures { t.m.card = t.MB.m.MB.card } = assert { forall k v. t.m.func k = Some v -> (not exists k2. t.MB.m.MB.func k = Some (k2,v) /\ CO.eq k k2) -> match t.MB.m.MB.func k with | None -> false | Some ((k2,_) as x) -> k2 = x.D.key && false end }
Invariant over logical model.
let lemma correction (t:t 'a) : unit requires { c t } ensures { forall k1 k2:K.t. CO.eq k1 k2 -> t.m.func k1 = t.m.func k2 } ensures { t.m.card >= 0 } = ()
Create an empty table.
let empty () : t 'a ensures { forall k:K.t. result.m.func k = None } ensures { result.m.card = 0 /\ c result } = MB.empty ()
Create a table with a single key->value binding.
let singleton (k:K.t) (v:'a) : t 'a ensures { (forall k2:K.t. if CO.eq k2 k then result.m.func k2 = Some v else result.m.func k2 = None) && result.m.func k = Some v } ensures { result.m.card = 1 /\ c result } = MB.singleton (k,v)
Check emptyness of a table.
let is_empty (ghost rk:ref K.t) (ghost rv:ref 'a) (t:t 'a) : bool requires { c t } ensures { result -> forall k:K.t. t.m.func k = None } ensures { not result -> t.m.func !rk = Some !rv } ensures { result <-> t.m.card = 0 } = let r = ref (!rk,!rv) in let res = MB.is_empty r t in let (a,b) = !r in rk := a;rv := b;res
Get and extract the (key->value) binding with minimum key.
let decompose_min (t:t 'a) : option ((K.t,'a),t 'a) requires { c t } returns { None -> (forall k:K.t. t.m.func k = None) /\ t.m.card = 0 | Some ((k,v),r) -> (forall k2:K.t. (CO.lt k2 k -> t.m.func k2 = None) /\ (CO.eq k2 k -> t.m.func k2 = Some v) /\ (CO.le k2 k -> r.m.func k2 = None) /\ (not CO.eq k k2 -> r.m.func k2 = t.m.func k2)) && t.m.func k = Some v && r.m.func k = None /\ t.m.card = 1 + r.m.card /\ c r } = MB.decompose_min t
Get and extract the (key->value) binding with maximum key.
let decompose_max (t:t 'a) : option (t 'a,(K.t,'a)) requires { c t } returns { None -> (forall k:K.t. t.m.func k = None) /\ t.m.card = 0 | Some (l,(k,v)) -> (forall k2:K.t. (CO.lt k k2 -> t.m.func k2 = None) /\ (CO.eq k k2 -> t.m.func k2 = Some v) /\ (CO.le k k2 -> l.m.func k2 = None) /\ (not CO.eq k2 k -> l.m.func k2 = t.m.func k2)) && t.m.func k = Some v && l.m.func k = None /\ t.m.card = 1 + l.m.card /\ c l } = MB.decompose_max t
Add a key->value binding with minimal key.
let add_min (k:K.t) (v:'a) (t:t 'a) : t 'a requires { c t /\ forall k2:K.t. CO.le k2 k -> t.m.func k2 = None } ensures { (forall k2:K.t. (CO.lt k2 k -> result.m.func k2 = None) /\ (CO.eq k2 k -> result.m.func k2 = Some v) /\ (not CO.eq k k2 -> result.m.func k2 = t.m.func k2)) && t.m.func k = None && result.m.func k = Some v } ensures { result.m.card = 1 + t.m.card /\ c result } = MB.add_min (k,v) t
Add a key->value binding with maximal key.
let add_max (t:t 'a) (k:K.t) (v:'a) : t 'a requires { c t /\ forall k2:K.t. CO.le k k2 -> t.m.func k2 = None } ensures { (forall k2:K.t. (CO.lt k k2 -> result.m.func k2 = None) /\ (CO.eq k k2 -> result.m.func k2 = Some v) /\ (not CO.eq k2 k -> result.m.func k2 = t.m.func k2)) && t.m.func k = None && result.m.func k = Some v } ensures { result.m.card = 1 + t.m.card /\ c result } = MB.add_max t (k,v)
Ordered fusion of two associative tables.
let concat (l r:t 'a) : t 'a requires { c l /\ c r } requires { forall k1 k2. l.m.func k1 <> None /\ r.m.func k2 <> None -> CO.lt k1 k2 } ensures { forall k. match l.m.func k with | None -> result.m.func k = r.m.func k | s -> result.m.func k = s end } ensures { forall k. match r.m.func k with | None -> result.m.func k = l.m.func k | s -> result.m.func k = s end } ensures { forall k. (result.m.func k = None <-> l.m.func k = None /\ r.m.func k = None) } ensures { result.m.card = l.m.card + r.m.card /\ c result } = MB.concat l r
Extract the value associated to some key.
let get (k:K.t) (t:t 'a) : option 'a requires { c t } returns { None -> (forall k2. CO.eq k k2 -> t.m.func k2 = None) && t.m.func k = None | Some v -> (forall k2. CO.eq k k2 -> t.m.func k2 = Some v) && t.m.func k = Some v /\ t.m.card > 0 } = match MB.get k t with | None -> None | Some (_,v) -> Some v end
Set the binding for key k
, erasing any such previous binding.
let insert (k:K.t) (v:'a) (t:t 'a) : t 'a requires { c t } ensures { (if t.m.func k = None then result.m.card = t.m.card + 1 else result.m.card = t.m.card) /\ (forall k2:K.t. (CO.eq k2 k -> result.m.func k2 = Some v) /\ (not CO.eq k2 k -> result.m.func k2 = t.m.func k2)) && result.m.func k = Some v /\ result.m.card >= t.m.card /\ c result } = let res = MB.insert (k,v) t in res
Erase any potential binding for key k
.
let remove (k:K.t) (t:t 'a) : t 'a requires { c t } ensures { (if t.m.func k = None then result.m.card = t.m.card else 1 + result.m.card = t.m.card) /\ (forall k2:K.t. (CO.eq k2 k -> result.m.func k2 = None) /\ (not CO.eq k2 k -> result.m.func k2 = t.m.func k2)) && result.m.func k = None /\ result.m.card <= t.m.card /\ c result } = MB.remove k t
Split the table in three parts:
Bindings with key lower than k
, value associated to k
,
and bindings with key greater than k
.
let split (k:K.t) (t:t 'a) : (t 'a,option 'a,t 'a) requires { c t } returns { (lf,o,rg) -> match o with | None -> (forall k2:K.t. CO.eq k k2 -> t.m.func k2 = None) && t.m.func k = None | Some v -> (forall k2:K.t. CO.eq k k2 -> t.m.func k2 = Some v) && t.m.func k = Some v end /\ t.m.card >= lf.m.card + rg.m.card /\ c lf /\ c rg /\ (if o = None then t.m.card = lf.m.card + rg.m.card else t.m.card = 1 + (lf.m.card + rg.m.card)) /\ (forall k2:K.t. CO.lt k2 k -> lf.m.func k2 = t.m.func k2) /\ (forall k2:K.t. CO.le k k2 -> lf.m.func k2 = None) /\ (forall k2:K.t. CO.lt k k2 -> rg.m.func k2 = t.m.func k2) /\ (forall k2:K.t. CO.le k2 k -> rg.m.func k2 = None) } = let (lf,o,rg) = MB.split k t in let o = abstract ensures { match o with None -> result = None | Some (_,v) -> result = Some v end } match o with None -> None | Some (_,v) -> Some v end end in (lf,o,rg) end
module Set use import int.Int use import option.Option use import ref.Ref
The balancing level is left abstract.
constant balancing : int axiom balancing_positive : balancing > 0
Parameter: comparable elements.
namespace K type t end clone preorder.Computable as CO with type t = K.t
Elements are themselves the keys.
namespace D type t 'a = K.t function key (t:'a) : 'a = t let get_key (t:'a) : 'a ensures { result = t } = t end
Actual instantiation.
clone MapBase as MB with constant balancing = balancing, goal balancing_positive, type K.t = K.t, type D.t = D.t, function key = D.key, val get_key = D.get_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
Slight adaptation of the logical model: use a set of elements.
type t = MB.t unit type m = { set : K.t -> bool; card : int; } predicate c (t:t) = MB.c t function oproj (o:option 'a) : bool = match o with | None -> false | Some _ -> true end function m (t:t) : m = { set = \k. oproj (t.MB.m.MB.func k); card = t.MB.m.MB.card } let lemma m_def (t:t) : unit ensures { forall k. not t.m.set k <-> t.MB.m.MB.func k = None } ensures { forall k v. t.MB.m.MB.func k = Some v -> t.m.set k } ensures { forall k. t.m.set k -> exists v. t.MB.m.MB.func k = Some v } ensures { t.m.card = t.MB.m.MB.card } = ()
Invariant on the logical model.
let lemma correction (t:t) : unit requires { c t } ensures { forall k1 k2:K.t. CO.eq k1 k2 -> (t.m.set k1 <-> t.m.set k2) } ensures { t.m.card >= 0 } = ()
Create an empty set.
let empty () : t ensures { forall k:K.t. not result.m.set k } ensures { result.m.card = 0 /\ c result } = MB.empty ()
Create a singleton set.
let singleton (k:K.t) : t ensures { forall k2:K.t. result.m.set k2 <-> CO.eq k2 k } ensures { result.m.card = 1 /\ c result } = MB.singleton k
Test emptyness of a set.
let is_empty (ghost rk:ref (K.t)) (t:t) : bool requires { c t } ensures { result -> forall k:K.t. not t.m.set k } ensures { not result -> t.m.set !rk } ensures { result <-> t.m.card = 0 } = MB.is_empty rk t
Get and remove minimum element from a set.
let decompose_min (t:t) : option (K.t,t) requires { c t } returns { None -> t.m.card = 0 /\ forall k:K.t. not t.m.set k | Some (k,r) -> (forall k2:K.t. (CO.lt k2 k -> not t.m.set k2) /\ (CO.eq k2 k -> t.m.set k2) /\ (CO.le k2 k -> not r.m.set k2) /\ (not CO.eq k k2 -> r.m.set k2 <-> t.m.set k2)) && t.m.set k && not r.m.set k /\ t.m.card = 1 + r.m.card /\ c r } = MB.decompose_min t
Get and remove maximum element from a set.
let decompose_max (t:t) : option (t,K.t) requires { c t } returns { None -> t.m.card = 0 /\ forall k:K.t. not t.m.set k | Some (l,k) -> (forall k2:K.t. (CO.lt k k2 -> not t.m.set k2) /\ (CO.eq k k2 -> t.m.set k2) /\ (CO.le k k2 -> not l.m.set k2) /\ (not CO.eq k2 k -> l.m.set k2 <-> t.m.set k2)) && t.m.set k && not l.m.set k /\ t.m.card = 1 + l.m.card /\ c l } = MB.decompose_max t
Add minimal element to a set.
let add_min (k:K.t) (t:t) : t requires { c t /\ forall k2:K.t. CO.le k2 k -> not t.m.set k2 } ensures { forall k2:K.t. (CO.lt k2 k -> not result.m.set k2) /\ (CO.eq k2 k -> result.m.set k2) /\ (not CO.eq k k2 -> result.m.set k2 <-> t.m.set k2) } ensures { result.m.card = 1 + t.m.card /\ c result } = MB.add_min k t
Add maximal element to a set.
let add_max (t:t) (k:K.t) : t requires { c t /\ forall k2:K.t. CO.le k k2 -> not t.m.set k2 } ensures { forall k2:K.t. (CO.lt k k2 -> not result.m.set k2) /\ (CO.eq k k2 -> result.m.set k2) /\ (not CO.eq k2 k -> result.m.set k2 <-> t.m.set k2) } ensures { result.m.card = 1 + t.m.card /\ c result } = MB.add_max t k
Ordered union of two sets.
let concat (l r:t) : t requires { c l /\ c r } requires { forall k1 k2. l.m.set k1 /\ r.m.set k2 -> CO.lt k1 k2 } ensures { forall k. result.m.set k <-> (r.m.set k \/ l.m.set k) } ensures { result.m.card = l.m.card + r.m.card /\ c result } = MB.concat l r
Test membership of an element.
let mem (k:K.t) (t:t) : bool requires { c t } ensures { result <-> t.m.set k } ensures { result <-> (forall k2. CO.eq k2 k -> t.m.set k2) } ensures { result -> t.m.card > 0 } = match MB.get k t with None -> false | _ -> true end
Add an element to a set.
let add (k:K.t) (t:t) : t requires { c t } ensures { (forall k2:K.t. (CO.eq k2 k -> result.m.set k2) /\ (t.m.set k2 -> result.m.set k2) /\ (not CO.eq k2 k -> result.m.set k2 -> t.m.set k2)) && result.m.set k /\ c result /\ (if t.m.set k then result.m.card = t.m.card else result.m.card = t.m.card + 1) && result.m.card >= t.m.card } = MB.insert k t
Remove an element from a set.
let remove (k:K.t) (t:t) : t requires { c t } ensures { (forall k2:K.t. (CO.eq k2 k -> not result.m.set k2) /\ (result.m.set k2 -> t.m.set k2) /\ (not CO.eq k2 k -> t.m.set k2 -> result.m.set k2)) && not result.m.set k /\ c result /\ (if t.m.set k then 1 + result.m.card = t.m.card else result.m.card = t.m.card) && result.m.card <= t.m.card } = MB.remove k t
Split the set into three parts: elements lower than k
,
elements equal to k
,
and elements bigger than k
let split (k:K.t) (t:t) : (t,bool,t) requires { c t } returns { (lf,b,rg) -> (b <-> t.m.set k) /\ (b <-> (forall k2. CO.eq k2 k -> t.m.set k2)) /\ (if b then t.m.card = 1 + (lf.m.card + rg.m.card) else t.m.card = lf.m.card + rg.m.card) && t.m.card >= lf.m.card + rg.m.card /\ c lf /\ c rg /\ (forall k. lf.m.set k -> t.m.set k) /\ (forall k. rg.m.set k -> t.m.set k) /\ (forall k2. CO.lt k2 k -> t.m.set k2 -> lf.m.set k2) /\ (forall k2. CO.lt k k2 -> t.m.set k2 -> rg.m.set k2) /\ (forall k2. CO.le k k2 -> not lf.m.set k2) /\ (forall k2. CO.le k2 k -> not rg.m.set k2) } = let (lf,o,rg) = MB.split k t in let o = abstract ensures { result <-> o <> None } match o with None -> false | _ -> true end end in (lf,o,rg)
Extension: set-theoretic routines.
Compute the union of two sets.
let union (a b:t) : t requires { c a /\ c b } ensures { forall k. result.m.set k <-> a.m.set k \/ b.m.set k } ensures { result.m.card >= a.m.card /\ result.m.card >= b.m.card } ensures { c result } = MB.add_all a b
Compute the intersection of two sets.
let inter (a b:t) : t requires { c a /\ c b } ensures { c result } ensures { forall k. result.m.set k <-> a.m.set k /\ b.m.set k } ensures { result.m.card <= a.m.card /\ result.m.card <= b.m.card } = MB.filter a b
Compute the difference of two sets.
let diff (a b:t) : t requires { c a /\ c b } ensures { forall k. result.m.set k <-> a.m.set k /\ not b.m.set k } ensures { result.m.card <= a.m.card /\ c result } = MB.remove_all b a
Compute the symmetrical difference of two sets.
let symdiff (a b:t) : t requires { c a /\ c b } ensures { forall k. result.m.set k <-> not (a.m.set k <-> b.m.set k) } ensures { result.m.card <= a.m.card + b.m.card /\ c result } = MB.symdiff a b end
Example instances: integer keys/elements
module IMapAndSet use import int.Int namespace K type t = int end constant balancing : int = 1 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 constant balancing = balancing, goal balancing_positive, 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 constant balancing = balancing, goal balancing_positive, 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 0.84