Commit 32b418b9 authored by Martin Clochard's avatar Martin Clochard

AVL example: cleanup

parent 29086d27
......@@ -447,8 +447,7 @@ module AVL
end
(* Node constructor, any (correct) input. *)
let rec join (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) :
t 'a 'b
let rec join (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : t 'a 'b
requires { c l /\ l.dprm.inv d /\ c r /\ l.prm = r.prm }
ensures { result.m.lis = node_model l.m.lis (l.dprm.mdl d) r.m.lis }
ensures { c result /\ result.prm = l.prm }
......@@ -502,51 +501,49 @@ module AVL
use export SelectionTypes
(* Parameter: selector type. *)
type selector 'a 'b
type selector
(* Parameter: correctness predicate for a selector with respect to the list
e.g the selector can select something in the list +
representation invariants. *)
predicate selector_correct (type_params 'a 'b) (selector 'a 'b)
(list (D.m 'b))
predicate selector_correct selector (list (D.m 'b))
(* Parameter: a position is selected by a selector in the
list corresponding to the avl. *)
predicate selected (type_params 'a 'b) (selector 'a 'b)
(position (D.m 'b)) (list (D.m 'b))
predicate selected selector (position (D.m 'b)) (list (D.m 'b))
axiom selected_rebuild : forall p,s:selector 'a 'b,e,l.
selected p s e l -> rebuild e = l
(*axiom selected_rebuild : forall p,s:selector 'a 'b,e,l.
selected p s e l -> rebuild e = l*)
(* way to the position. *)
type way 'a 'b = way_base (selector 'a 'b)
type way = way_base selector
(* Parameter: a correct selector for the empty list
always select its only possible position. *)
axiom selector_correct_empty : forall p,s:selector 'a 'b.
selector_correct p s Nil ->
selected p s { left = Nil ; middle = None ; right = Nil } Nil
axiom selector_correct_empty : forall s. let nil = (Nil:list (D.m 'b)) in
selector_correct s nil ->
selected s { left = Nil ; middle = None ; right = Nil } nil
(* Parameter: branch on a node. *)
val selected_way (ghost p:type_params 'a 'b)
(ghost base:list (D.m 'b))
(ghost llis:list (D.m 'b))
(ghost rlis:list (D.m 'b))
(s:selector 'a 'b) (l:M.t) (d:D.t 'a 'b) (r:M.t) : way 'a 'b
(s:selector) (l:M.t) (d:D.t 'a 'b) (r:M.t) : way
requires { M.c l /\ p.D.mp.inv d /\ M.c r }
requires { base = node_model llis (p.D.mp.mdl d) rlis }
requires { selector_correct p s base }
requires { selector_correct s base }
requires { l.M.m = M.sum D.measure llis /\ r.M.m = M.sum D.measure rlis }
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis;
middle = Some (p.D.mp.mdl d);
right = rlis } in selected p s e2 base
| Left sl -> selector_correct p sl llis /\
forall e. selected p sl e llis ->
selected p s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct p sr rlis /\
forall e. selected p sr e rlis ->
selected p s (left_extend llis (p.D.mp.mdl d) e) base }
right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\
forall e. selected sl e llis /\ rebuild e = llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\
forall e. selected sr e rlis /\ rebuild e = rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
use import ref.Ref
......@@ -559,11 +556,11 @@ module AVL
and rebuild it with d in the middle (potentially erasing whatever
was there before): build l ++ [d] ++ r.
The reference is assigned to the selected position. *)
let rec add (ghost r:ref (position (D.m 'b))) (s:selector 'a 'b)
let rec add (ghost r:ref (position (D.m 'b))) (s:selector)
(d:D.t 'a 'b) (t:t 'a 'b) : t 'a 'b
requires { selector_correct t.prm s t.m.lis /\ c t /\ t.dprm.inv d }
requires { selector_correct s t.m.lis /\ c t /\ t.dprm.inv d }
ensures { result.m.lis = node_model !r.left (t.dprm.mdl d) !r.right }
ensures { selected t.prm s !r t.m.lis }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { c result /\ result.prm = t.prm }
writes { r }
(* not intended for export. *)
......@@ -588,11 +585,11 @@ module AVL
(* Split the avl using the given selector into l ++ (maybe) ++ r,
and rebuild it without whatever was in the middle:
build l ++ r. *)
let rec remove (ghost r:ref (position (D.m 'b))) (s:selector 'a 'b)
let rec remove (ghost r:ref (position (D.m 'b))) (s:selector)
(t:t 'a 'b) : t 'a 'b
requires { selector_correct t.prm s t.m.lis /\ c t }
requires { selector_correct s t.m.lis /\ c t }
ensures { result.m.lis = !r.left ++ !r.right }
ensures { selected t.prm s !r t.m.lis }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { c result /\ result.prm = t.prm }
writes { r }
(* not intended for export. *)
......@@ -613,10 +610,10 @@ module AVL
end
end
let rec extract (ghost r:ref (position (D.m 'b))) (s:selector 'a 'b)
let rec extract (ghost r:ref (position (D.m 'b))) (s:selector)
(t:t 'a 'b) : (option (D.t 'a 'b),t 'a 'b)
requires { selector_correct t.prm s t.m.lis /\ c t }
ensures { selected t.prm s !r t.m.lis }
requires { selector_correct s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { let (d,t2) = result in
c t2 /\ t2.prm = t.prm /\ t2.m.lis = !r.left ++ !r.right /\
1 >= t.m.hgt - t2.m.hgt >= 0 /\
......@@ -642,10 +639,10 @@ module AVL
(* Split the avl according to the selector. *)
let rec split (ghost r:ref (position (D.m 'b))) (s:selector 'a 'b)
let rec split (ghost r:ref (position (D.m 'b))) (s:selector)
(t:t 'a 'b) : (t 'a 'b,option (D.t 'a 'b),t 'a 'b)
requires { selector_correct t.prm s t.m.lis /\ c t }
ensures { selected t.prm s !r t.m.lis }
requires { selector_correct s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
returns { (lf,o,rg) -> lf.m.lis = !r.left /\ rg.m.lis = !r.right /\
(match o with
| None -> !r.middle = None
......@@ -673,10 +670,10 @@ module AVL
(* Return the middle value obtained by splitting the avl with respect
to the selector. *)
let rec get (ghost r:ref (position (D.m 'b))) (s:selector 'a 'b)
let rec get (ghost r:ref (position (D.m 'b))) (s:selector)
(t:t 'a 'b) : option (D.t 'a 'b)
requires { selector_correct t.prm s t.m.lis /\ c t }
ensures { selected t.prm s !r t.m.lis }
requires { selector_correct s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
returns { None -> !r.middle = None
| Some d -> !r.middle = Some (t.dprm.mdl d) /\ t.dprm.inv d }
writes { r }
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -62,34 +62,32 @@ module MapBase
end
(* Selector: key. *)
type selector 'a 'b = K.t
type selector = K.t
(* Correction of a selector with respect to a list:
The list is sorted. *)
predicate selector_correct (p:type_params 'a 'b) (s:K.t) (l:list (D.m 'b)) =
predicate selector_correct (s:K.t) (l:list (D.m 'b)) =
A.S.increasing l /\ K.c s
predicate selected (p:type_params 'a 'b) (s:K.t)
(e:position (D.m 'b)) (l:list (D.m 'b)) =
predicate selected (s:K.t) (e:position (D.m 'b)) (l:list (D.m 'b)) =
(A.S.majorate s.K.m e.left /\ A.S.minorate s.K.m e.right /\
A.S.increasing e.left /\ A.S.increasing e.right /\
match e.middle with
| None -> true
| Some d2 -> CO.eq s.K.m d2.key
end) /\
rebuild e = l /\ selector_correct p s l
end) /\ rebuild e = l /\ selector_correct s l
predicate selected_sem (s:K.t) (e:position (D.m 'b)) (l:list (D.m 'b)) =
forall k:K.m. (CO.lt k s.K.m -> A.model l k = A.model e.left k) /\
(CO.lt s.K.m k -> A.model l k = A.model e.right k) /\
(CO.eq k s.K.m -> A.model l k = e.middle) /\
(CO.le s.K.m k -> A.model e.left k = None) /\
(CO.le k s.K.m -> A.model e.right k = None)
forall k:K.m. (CO.lt k s.K.m -> A.model l k = A.model e.left k) /\
(CO.lt s.K.m k -> A.model l k = A.model e.right k) /\
(CO.eq k s.K.m -> A.model l k = e.middle) /\
(CO.le s.K.m k -> A.model e.left k = None) /\
(CO.le k s.K.m -> A.model e.right k = None)
let lemma selected_sem (p:type_params 'a 'b) (s:K.t)
let lemma selected_sem (s:K.t)
(e:position (D.m 'b)) (l:list (D.m 'b)) : unit
requires { selected p s e l }
requires { selected s e l }
ensures { selected_sem s e l }
= match e.middle with
| None -> A.model_cut s.K.m e.left e.right
......@@ -103,17 +101,17 @@ module MapBase
(s:K.t) (l:'e) (d:D.t 'a 'b) (r:'f) : way_base K.t
requires { p.D.mp.inv d }
requires { base = llis ++ Cons (p.D.mp.mdl d) rlis }
requires { selector_correct p s base }
requires { selector_correct s base }
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis;
middle = Some (p.D.mp.mdl d);
right = rlis } in selected p s e2 base
| Left sl -> selector_correct p sl llis /\
forall e. selected p sl e llis ->
selected p s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct p sr rlis /\
forall e. selected p sr e rlis ->
selected p s (left_extend llis (p.D.mp.mdl d) e) base }
right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
= let kd = get_key p d in
let cmp = CO.compare s kd in
if cmp < 0
......
......@@ -86,20 +86,18 @@ module Heap
end
(* Selector: nothing. *)
type selector 'a 'b = unit
type selector = unit
(* Correction of a selector with respect to an avl:
the avl list is non-empty. *)
predicate selector_correct 'd 'e (l:list 'g) =
l <> Nil
predicate selector_correct 'e (l:list 'g) = l <> Nil
predicate selected 'd 'e (e:position (D.m 'b)) (l:list (D.m 'b)) =
predicate selected 'e (e:position (D.m 'b)) (l:list (D.m 'b)) =
match e.middle with
| None -> false
| Some d -> S.minorate d.key e.left /\ S.minorate d.key e.right
end /\
rebuild e = l
end /\ rebuild e = l
let rec lemma monoid_sum_is_min (l:list (D.m 'b)) : unit
ensures { let x = M.sum D.measure l in
......@@ -110,9 +108,9 @@ module Heap
variant { l }
= match l with Cons _ q -> monoid_sum_is_min q | _ -> () end
let lemma selected_is_min (p:'c) (s:'d) (e:position (D.m 'b))
let lemma selected_is_min (s:'d) (e:position (D.m 'b))
(l:list (D.m 'b)) : unit
requires { selected p s e l }
requires { selected s e l }
ensures { match e.middle with
| None -> false
| Some d -> S.minorate d.key l && match M.sum D.measure l with
......@@ -134,13 +132,13 @@ module Heap
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis;
middle = Some (p.D.mp.mdl d);
right = rlis } in selected p s e2 base
| Left sl -> selector_correct p sl llis /\
forall e. selected p sl e llis ->
selected p s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct p sr rlis /\
forall e. selected p sr e rlis ->
selected p s (left_extend llis (p.D.mp.mdl d) e) base }
right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
= let kd = get_key p d in
match sl , sr with
| None , None -> Here
......@@ -150,7 +148,7 @@ module Heap
then if CO.compare kd b <= 0
then Here
else begin
assert { forall e. selected p () e rlis ->
assert { forall e. selected () e rlis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key b.K.m && S.minorate d.key llis
......@@ -159,7 +157,7 @@ module Heap
end
else if CO.compare a b <= 0
then begin
assert { forall e. selected p () e llis ->
assert { forall e. selected () e llis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key a.K.m && S.minorate d.key rlis
......@@ -167,7 +165,7 @@ module Heap
Left ()
end
else begin
assert { forall e. selected p () e rlis ->
assert { forall e. selected () e rlis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key b.K.m && S.minorate d.key llis
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -54,39 +54,38 @@ module RAL
= match l with Cons _ q -> sum_measure_is_length q | _ -> () end
(* Select an element or the hole before him (e.g holes starts at 0) *)
type sel = { index : int; hole : bool }
type selector 'a 'b = sel
type selector = { index : int; hole : bool }
(* Correctness predicate for selector with respect to a list:
between bounds. *)
predicate selector_correct (p:type_params 'a 'b) (s:sel) (l:list 'b) =
predicate selector_correct (s:selector) (l:list 'b) =
0 <= s.index && (if s.hole then s.index <= length l else s.index < length l)
(* Selection predicate: We are exactly at the index-th position of the
rebuild list, and there is an element in the middle iff we are
not trying to select a hole. *)
predicate selected 'e (s:sel) (e:position 'b) (l:list 'b) =
s.index = length e.left /\ (s.hole <-> e.middle = None) /\ rebuild e = l
predicate selected (s:selector) (e:position 'b) (l:list 'b) =
s.index = length e.left /\ (s.hole <-> e.middle = None)
let selected_way (ghost p:type_params 'a 'b)
(ghost base:list 'b)
(ghost llis:list 'b)
(ghost rlis:list 'b)
(s:sel) (sl:int) (d:'a) (sr:int) : way_base sel
(s:selector) (sl:int) (d:'a) (sr:int) : way_base selector
requires { p.inv d }
requires { base = llis ++ Cons (p.mdl d) rlis }
requires { selector_correct p s base }
requires { selector_correct s base }
requires { sl = length llis /\ sr = length rlis }
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis;
middle = Some (p.mdl d);
right = rlis } in selected p s e2 base
| Left sl -> selector_correct p sl llis /\
forall e. selected p sl e llis ->
selected p s (right_extend e (p.mdl d) rlis) base
| Right sr -> selector_correct p sr rlis /\
forall e. selected p sr e rlis ->
selected p s (left_extend llis (p.mdl d) e) base }
right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.mdl d) e) base }
= (* Use the size information to decide
where the index-th position is. *)
let ind = s.index in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment