Commit 96ace312 authored by Mário Pereira's avatar Mário Pereira

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system

Conflicts:
	examples/schorr_waite.mlw
parents db60323e 74cd8301
......@@ -40,14 +40,15 @@ module SchorrWaite
type loc
constant null: loc
val (=) (a b: loc) : bool
ensures { result = (a = b) }
(** each (non-null) location holds four fields: two Boolean marks m and c
and two pointers left and right *)
val m: ref (map loc bool)
val c: ref (map loc bool)
val left: ref (map loc loc)
val right: ref (map loc loc)
val (=) (x y : loc) : bool ensures { result <-> x = y }
val (<<>>) (p1 p2: loc) : bool ensures { result <-> p1 <> p2 }
val get_left (p: loc) : loc
requires { p <> null }
......@@ -199,7 +200,7 @@ module SchorrWaite
ghost set_path_from_root !t !pth;
let ghost unmarked_nodes = ref graph in
let ghost c_false_nodes = ref graph in
while !p <<>> null || (!t <<>> null && not get_m !t) do
while !p <> null || (!t <> null && not get_m !t) do
invariant { forall n. mem n graph -> not_in_stack n !stackNodes \/
exists i : int. Seq.get !stackNodes i = n }
invariant { not_in_stack null !stackNodes }
......@@ -216,15 +217,15 @@ module SchorrWaite
invariant { forall i. 0 <= i < Seq.length !stackNodes - 1 ->
let p1 = Seq.get !stackNodes i in
let p2 = Seq.get !stackNodes (i+1) in
(!c[p2] -> (old !left )[p2] = !left[p2] /\
(old !right )[p2] = p1) /\
(not !c[p2] -> (old !left )[p2] = p1 /\
(old !right )[p2] = !right[p2]) }
(!c[p2] -> old !left[p2] = !left[p2] /\
old !right[p2] = p1) /\
(not !c[p2] -> old !left[p2] = p1 /\
old !right[p2] = !right[p2]) }
invariant { !path_from_root[root] = Nil }
invariant { forall n : loc. S.mem n graph ->
not_in_stack n !stackNodes ->
!left[n] = (old !left )[n] /\
!right[n] = (old !right )[n] }
!left[n] = old !left[n] /\
!right[n] = old !right[n] }
(* something like Leino's line 74; this is useful to prove that
* the stack is empty iff p = null *)
invariant { Seq.length !stackNodes <> 0 ->
......@@ -246,30 +247,30 @@ module SchorrWaite
(* something like Leino's line 68 *)
invariant { forall i. 0 <= i < Seq.length !stackNodes ->
let n = Seq.get !stackNodes i in
if !c[n] then !left[n] = (old !left )[n]
else !right[n] = (old !right )[n] }
if !c[n] then !left[n] = old !left[n]
else !right[n] = old !right[n] }
(* lines 80-81 from Leino's paper *)
invariant { Seq.length !stackNodes <> 0 ->
if !c[!p] then (old !right )[!p] = !t
else (old !left )[!p] = !t }
if !c[!p] then old !right[!p] = !t
else old !left[!p] = !t }
(* lines 78-79 from Leino's paper *)
invariant { forall k : int. 0 < k < Seq.length !stackNodes ->
let n = Seq.get !stackNodes k in
if !c[n]
then Seq.get !stackNodes (k - 1) = (old !right )[n]
else Seq.get !stackNodes (k - 1) = (old !left )[n] }
then Seq.get !stackNodes (k - 1) = old !right[n]
else Seq.get !stackNodes (k - 1) = old !left[n] }
(* line 70 from Leino's paper *)
invariant { !p <> null ->
path (old !left ) (old !right ) root !p !pth }
path (old !left) (old !right) root !p !pth }
(* line 72 from Leino's paper *)
invariant { forall n : loc. S.mem n graph -> !m[n] ->
reachable (old !left ) (old !right ) root n }
reachable (old !left) (old !right) root n }
invariant { !p = null -> !t = root }
(* line 70 from Leino's paper *)
invariant { forall n : loc, pth : list loc.
S.mem n graph -> !m[n] ->
pth = !path_from_root[n] ->
path (old !left ) (old !right ) root n pth }
path (old !left) (old !right) root n pth }
(* lines 61-62 from Leinos' paper *)
invariant { forall n : loc. S.mem n graph -> n <> null -> !m[n] ->
not_in_stack n !stackNodes ->
......@@ -311,7 +312,7 @@ module SchorrWaite
ghost if !p <> root then pth := !pth ++ (Cons q Nil) else pth := Nil;
ghost set_path_from_root !p !pth;
assert { !p = Seq.get !stackNodes 0 };
assert { path (old !left ) (old !right ) root !p !pth };
assert { path (old !left) (old !right) root !p !pth };
set_c !p false;
ghost c_false_nodes := S.add !p !c_false_nodes;
ghost unmarked_nodes := S.remove !p !unmarked_nodes
......
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