Commit b551e9d8 authored by Martin Clochard's avatar Martin Clochard

AVL example: Removed some useless arguments.

parent 5432d834
......@@ -509,12 +509,8 @@ module AVL
representation invariants. *)
predicate selection_possible selector (list (D.m 'b))
(* Parameter: a position is selected by a selector in the
list corresponding to the avl. *)
predicate selected selector (split (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*)
(* Parameter: a position is selected by a selector in the. *)
predicate selected selector (split (D.m 'b))
(* Selected part. *)
type part = part_base selector
......@@ -523,28 +519,26 @@ module AVL
always select its only possible position. *)
axiom selection_empty : forall s. let nil = (Nil:list (D.m 'b)) in
selection_possible s nil ->
selected s { left = Nil ; middle = None ; right = Nil } nil
selected s { left = nil ; middle = None ; right = nil }
(* Parameter: branch on a node. *)
val selected_part (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) (l:M.t) (d:D.t 'a 'b) (r:M.t) : part
requires { M.c l /\ p.D.mp.inv d /\ M.c r }
requires { base = node_model llis (p.D.mp.mdl d) rlis }
requires { selection_possible s base }
requires { selection_possible s (node_model llis (p.D.mp.mdl d) rlis) }
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 s e2 base
right = rlis } in selected s e2
| Left sl -> selection_possible sl llis /\
forall e. selected sl e llis /\ rebuild e = llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
forall e. selected sl e /\ rebuild e = llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis)
| Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis /\ rebuild e = rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
forall e. selected sr e /\ rebuild e = rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) }
use import ref.Ref
......@@ -561,7 +555,7 @@ module AVL
(d:D.t 'a 'b) (t:t 'a 'b) : t 'a 'b
requires { selection_possible 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 s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { selected s !r /\ rebuild !r = t.m.lis }
ensures { c result /\ result.prm = t.prm }
writes { r }
(* not intended for export. *)
......@@ -570,7 +564,7 @@ module AVL
= match view t with
| AEmpty -> r := { left = Nil; middle = None; right = Nil };
singleton t.prm d
| ANode tl td tr _ _ -> match selected_part t.prm t.m.lis tl.m.lis tr.m.lis
| ANode tl td tr _ _ -> match selected_part t.prm tl.m.lis tr.m.lis
s (total tl) td (total tr) with
| Left sl -> let nl = insert r sl d tl in
r := right_extend !r (t.dprm.mdl td) tr.m.lis; balance nl td tr
......@@ -590,7 +584,7 @@ module AVL
(t:t 'a 'b) : t 'a 'b
requires { selection_possible s t.m.lis /\ c t }
ensures { result.m.lis = !r.left ++ !r.right }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { selected s !r /\ rebuild !r = t.m.lis }
ensures { c result /\ result.prm = t.prm }
writes { r }
(* not intended for export. *)
......@@ -598,7 +592,7 @@ module AVL
variant { t.m.hgt }
= match view t with
| AEmpty -> r := { left = Nil; middle = None; right = Nil}; t
| ANode tl td tr _ _ -> match selected_part t.prm t.m.lis tl.m.lis tr.m.lis
| ANode tl td tr _ _ -> match selected_part t.prm tl.m.lis tr.m.lis
s (total tl) td (total tr) with
| Left sl -> let nl = remove r sl tl in
r := right_extend !r (t.dprm.mdl td) tr.m.lis; balance nl td tr
......@@ -614,7 +608,7 @@ module AVL
let rec extract (ghost r:ref (split (D.m 'b))) (s:selector)
(t:t 'a 'b) : (option (D.t 'a 'b),t 'a 'b)
requires { selection_possible s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { selected s !r /\ 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 /\
......@@ -625,7 +619,7 @@ module AVL
variant { t.m.hgt }
= match view t with
| AEmpty -> r := { left = Nil; middle = None; right = Nil }; (None,t)
| ANode tl td tr _ _ -> match selected_part t.prm t.m.lis tl.m.lis tr.m.lis
| ANode tl td tr _ _ -> match selected_part t.prm tl.m.lis tr.m.lis
s (total tl) td (total tr) with
| Left sl -> let (ol,nl) = extract r sl tl in
r := right_extend !r (t.dprm.mdl td) tr.m.lis; (ol,balance nl td tr)
......@@ -643,7 +637,7 @@ module AVL
let rec split (ghost r:ref (split (D.m 'b))) (s:selector)
(t:t 'a 'b) : (t 'a 'b,option (D.t 'a 'b),t 'a 'b)
requires { selection_possible s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { selected s !r /\ 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
......@@ -654,7 +648,7 @@ module AVL
= match view t with
| AEmpty -> r := { left = Nil; middle = None; right = Nil };
(t,None,t)
| ANode tl td tr _ _ -> match selected_part t.prm t.m.lis tl.m.lis tr.m.lis
| ANode tl td tr _ _ -> match selected_part t.prm tl.m.lis tr.m.lis
s (total tl) td (total tr) with
| Left sl -> let (tll,tlo,tlr) = split r sl tl in
r := right_extend !r (t.dprm.mdl td) tr.m.lis;
......@@ -674,14 +668,14 @@ module AVL
let rec get (ghost r:ref (split (D.m 'b))) (s:selector)
(t:t 'a 'b) : option (D.t 'a 'b)
requires { selection_possible s t.m.lis /\ c t }
ensures { selected s !r t.m.lis /\ rebuild !r = t.m.lis }
ensures { selected s !r /\ 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 }
variant { t.m.hgt }
= match view t with
| AEmpty -> r := { left = Nil; middle = None; right = Nil }; None
| ANode tl td tr _ _ -> match selected_part t.prm t.m.lis tl.m.lis tr.m.lis
| ANode tl td tr _ _ -> match selected_part t.prm tl.m.lis tr.m.lis
s (total tl) td (total tr) with
| Left sl -> let res = get r sl tl in
r := right_extend !r (t.dprm.mdl td) tr.m.lis; res
......
......@@ -70,16 +70,17 @@ module MapBase
predicate selection_possible (s:K.t) (l:list (D.m 'b)) =
A.S.increasing l /\ K.c s
predicate selected (s:K.t) (e:split (D.m 'b)) (l:list (D.m 'b)) =
(A.S.upper_bound s.K.m e.left /\ A.S.lower_bound s.K.m e.right /\
match e.middle with
| None -> true
| Some d2 -> CO.eq s.K.m 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 /\
rebuild e = l /\ selection_possible s l
predicate selected (s:K.t) (e:split (D.m 'b)) =
let l = rebuild e in
(A.S.upper_bound s.K.m e.left /\ A.S.lower_bound s.K.m e.right /\
match e.middle with
| None -> true
| Some d2 -> CO.eq s.K.m 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
predicate selected_sem (s:K.t) (e:split (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) /\
......@@ -88,32 +89,29 @@ module MapBase
(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 (s:K.t)
(e:split (D.m 'b)) (l:list (D.m 'b)) : unit
requires { selected s e l }
ensures { selected_sem s e l }
let lemma selected_sem (s:K.t) (e:split (D.m 'b)) : unit
requires { selected s e }
ensures { selected_sem s e (rebuild e) }
= match e.middle with
| None -> A.model_cut s.K.m e.left e.right
| Some dm -> A.model_split dm e.left e.right
end
let selected_part (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:K.t) (l:'e) (d:D.t 'a 'b) (r:'f) : part_base K.t
requires { p.D.mp.inv d }
requires { base = llis ++ Cons (p.D.mp.mdl d) rlis }
requires { selection_possible s base }
requires { selection_possible s (llis ++ Cons (p.D.mp.mdl d) rlis) }
returns { Here -> let e2 = { left = llis;
middle = Some (p.D.mp.mdl d);
right = rlis } in selected s e2 base
right = rlis } in selected s e2
| Left sl -> selection_possible sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
forall e. selected sl e /\ rebuild e = llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis)
| Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
forall e. selected sr e /\ rebuild e = rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) }
= let kd = get_key p d in
let cmp = CO.compare s kd in
if cmp < 0
......
......@@ -27,10 +27,10 @@
locfile="../monoid.mlw"
loclnum="26" loccnumb="16" loccnume="26"
expl="VC for sum_append"
sum="93f3fef7f24026ff7ffc85f1eeab1ce1"
sum="ae30fca9a3b56ad657714f22093400f4"
proved="true"
expanded="true"
shape="Cainfix =asumV0ainfix ++V1V2aaddasumV0V1asumV0V2Iainfix =asumV0ainfix ++V3V2aaddasumV0V3asumV0V2ACfaNilainfix =V4V3aConswVV1aConswVainfix =asumV0ainfix ++V1V2aaddasumV0V1asumV0V2wV1F">
shape="Cainfix =asumV0ainfix ++V1V2aopasumV0V1asumV0V2Iainfix =asumV0ainfix ++V3V2aopasumV0V3asumV0V2ACfaNilainfix =V4V3aConswVV1aConswVainfix =asumV0ainfix ++V1V2aopasumV0V1asumV0V2wV1F">
<label
name="why3:lemma"/>
<label
......@@ -55,7 +55,7 @@
name="sum_def_nil"
locfile="../monoid.mlw"
loclnum="22" loccnumb="8" loccnume="19"
sum="1fabfcb4f1d5fd8cff9c9422b1af6f6e"
sum="0e664b10c26136c4f145c9d87c130dac"
proved="true"
expanded="true"
shape="ainfix =asumV0aNilazeroF">
......@@ -72,10 +72,10 @@
name="sum_def_cons"
locfile="../monoid.mlw"
loclnum="23" loccnumb="8" loccnume="20"
sum="74a8baa5028da06c811d858ba41c263f"
sum="24fccade2e910321d8504790441b897d"
proved="true"
expanded="true"
shape="ainfix =asumV0aConsV1V2aaddainfix @V0V1asumV0V2F">
shape="ainfix =asumV0aConsV1V2aopainfix @V0V1asumV0V2F">
<proof
prover="0"
timelimit="5"
......
module Heap
module PQueue
use import int.Int
use import avl.SelectionTypes
......@@ -94,11 +94,11 @@ module Heap
predicate selection_possible 'e (l:list 'g) = l <> Nil
predicate selected 'e (e:split (D.m 'b)) (l:list (D.m 'b)) =
predicate selected 'e (e:split (D.m 'b)) =
match e.middle with
| None -> false
| Some d -> S.lower_bound d.key e.left /\ S.lower_bound d.key e.right
end /\ rebuild e = l
end
let rec lemma monoid_sum_is_min (l:list (D.m 'b)) : unit
ensures { let x = M.sum D.measure l in
......@@ -109,10 +109,9 @@ module Heap
variant { l }
= match l with Cons _ q -> monoid_sum_is_min q | _ -> () end
let lemma selected_is_min (s:'d) (e:split (D.m 'b))
(l:list (D.m 'b)) : unit
requires { selected s e l }
ensures { match e.middle with
let lemma selected_is_min (s:'d) (e:split (D.m 'b)) : unit
requires { selected s e }
ensures { let l = rebuild e in match e.middle with
| None -> false
| Some d -> S.lower_bound d.key l && match M.sum D.measure l with
| None -> false
......@@ -122,24 +121,22 @@ module Heap
= ()
let selected_part (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:unit) (sl:M.t) (d:D.t 'a 'b) (sr:M.t) : part_base unit
requires { p.D.mp.inv d }
requires { base = llis ++ Cons (p.D.mp.mdl d) rlis }
requires { sl.M.m = M.sum D.measure llis /\ sr.M.m = M.sum D.measure rlis }
requires { M.c sl /\ M.c sr }
(* 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 s e2 base
right = rlis } in selected s e2
| Left sl -> selection_possible sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base
forall e. selected sl e /\ rebuild e = llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis)
| Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base }
forall e. selected sr e /\ rebuild e = rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) }
= let kd = get_key p d in
match sl , sr with
| None , None -> Here
......@@ -149,7 +146,7 @@ module Heap
then if CO.compare kd b <= 0
then Here
else begin
assert { forall e. selected () e rlis ->
assert { forall e. selected () e /\ rebuild e = rlis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key b.K.m && S.lower_bound d.key llis
......@@ -158,7 +155,7 @@ module Heap
end
else if CO.compare a b <= 0
then begin
assert { forall e. selected () e llis ->
assert { forall e. selected () e /\ rebuild e = llis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key a.K.m && S.lower_bound d.key rlis
......@@ -166,7 +163,7 @@ module Heap
Left ()
end
else begin
assert { forall e. selected () e rlis ->
assert { forall e. selected () e /\ rebuild e = rlis ->
match e.middle with
| None -> false
| Some d -> CO.eq d.key b.K.m && S.lower_bound d.key llis
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -63,27 +63,25 @@ module RAL
(* 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 (s:selector) (e:split 'b) (l:list 'b) =
predicate selected (s:selector) (e:split 'b) =
s.index = length e.left /\ (s.hole <-> e.middle = None)
let selected_part (ghost p:type_params 'a 'b)
(ghost base:list 'b)
(ghost llis:list 'b)
(ghost rlis:list 'b)
(s:selector) (sl:int) (d:'a) (sr:int) : part_base selector
requires { p.inv d }
requires { base = llis ++ Cons (p.mdl d) rlis }
requires { selection_possible s base }
requires { selection_possible s (llis ++ Cons (p.D.mp.mdl d) rlis) }
requires { sl = length llis /\ sr = length rlis }
returns { Here -> let e2 = { left = llis;
middle = Some (p.mdl d);
right = rlis } in selected s e2 base
right = rlis } in selected s e2
| Left sl -> selection_possible sl llis /\
forall e. selected sl e llis ->
selected s (right_extend e (p.mdl d) rlis) base
forall e. selected sl e /\ rebuild e = llis ->
selected s (right_extend e (p.mdl d) rlis)
| Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis ->
selected s (left_extend llis (p.mdl d) e) base }
forall e. selected sr e /\ rebuild e = rlis ->
selected s (left_extend llis (p.mdl d) e) }
= (* Use the size information to decide
where the index-th position is. *)
let ind = s.index in
......
......@@ -61,7 +61,7 @@
locfile="../sorted.mlw"
loclnum="42" loccnumb="16" loccnume="34"
expl="VC for increasing_precede"
sum="9969a4f64c4ebf0386accfdff4d09083"
sum="a14ea48db1b3aabb4f5217e92600d09d"
proved="true"
expanded="false"
shape="CaprecedeV0V1AaincreasingV1AaincreasingV0qaincreasingainfix ++V0V1aNilaprecedeV0V1AaincreasingV1AaincreasingV0qaincreasingainfix ++V0V1IaprecedeV2V1AaincreasingV1AaincreasingV2qaincreasingainfix ++V2V1ACfaNilainfix =V3V2aConswVV0aConswVV0F">
......@@ -78,7 +78,7 @@
locfile="../sorted.mlw"
loclnum="42" loccnumb="16" loccnume="34"
expl="1. postcondition"
sum="0a4ba65874f2c22311cc6710f1d6523a"
sum="e97aa8badbe4e689f2742f87c656b2cc"
proved="true"
expanded="false"
shape="postconditionCaprecedeV0V1AaincreasingV1AaincreasingV0qaincreasingainfix ++V0V1aNiltaConswVV0F">
......@@ -100,7 +100,7 @@
locfile="../sorted.mlw"
loclnum="42" loccnumb="16" loccnume="34"
expl="2. variant decrease"
sum="1a88d4928c69892d46c0608ee485cb5e"
sum="33dfddf564e363c9ad369c2ba5f3d618"
proved="true"
expanded="false"
shape="variant decreaseCtaNilCfaNilainfix =V3V2aConswVV0aConswVV0F">
......@@ -122,7 +122,7 @@
locfile="../sorted.mlw"
loclnum="42" loccnumb="16" loccnume="34"
expl="3. postcondition"
sum="587d6b2ac29f72297ee2d67bed6da41d"
sum="da67a6f64f677cca6070143461490f92"
proved="true"
expanded="false"
shape="postconditionCtaNilaprecedeV0V1AaincreasingV1AaincreasingV0qaincreasingainfix ++V0V1IaprecedeV2V1AaincreasingV1AaincreasingV2qaincreasingainfix ++V2V1aConswVV0F">
......@@ -146,7 +146,7 @@
locfile="../sorted.mlw"
loclnum="51" loccnumb="12" loccnume="31"
expl="VC for increasing_midpoint"
sum="eb2f665f56648e1475e9acd748fd3eee"
sum="86135d7a2621e6d364cd14684251e87b"
proved="true"
expanded="false"
shape="aupper_boundV3V0Aalower_boundV3V2AaincreasingV2AaincreasingV0qaincreasingainfix ++V0aConsV1V2LakeyV1F">
......@@ -168,7 +168,7 @@
locfile="../sorted.mlw"
loclnum="57" loccnumb="12" loccnume="27"
expl="VC for increasing_snoc"
sum="3503194ca7ef4bf086be10572757e409"
sum="23b4afe3c621eaad582701371dd9ac6a"
proved="true"
expanded="false"
shape="aupper_boundakeyV1V0AaincreasingV0qaincreasingainfix ++V0aConsV1aNilF">
......
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