Commit e73b3b1a authored by Mário Pereira's avatar Mário Pereira

Proof in progress (Schorr-Waite)

parent 6a5fc60f
...@@ -84,7 +84,7 @@ module SchorrWaite ...@@ -84,7 +84,7 @@ module SchorrWaite
ensures { forall n : loc. L.mem n result -> L.mem n stack } ensures { forall n : loc. L.mem n result -> L.mem n stack }
predicate edge (x y : loc) (left right : map loc loc) = predicate edge (x y : loc) (left right : map loc loc) =
x <> null && (left[x] = y || right[x] = y) x <> null /\ (left[x] = y \/ right[x] = y)
inductive path (left right : map loc loc) (x y : loc) (p : list loc) = inductive path (left right : map loc loc) (x y : loc) (p : list loc) =
| path_nil : forall x : loc, l r : map loc loc. path l r x x Nil | path_nil : forall x : loc, l r : map loc loc. path l r x x Nil
...@@ -174,8 +174,10 @@ module SchorrWaite ...@@ -174,8 +174,10 @@ module SchorrWaite
(old !right)[n] = !right[n] } (old !right)[n] = !right[n] }
(* all the non-null vertices reachable from root (* all the non-null vertices reachable from root
are marked at the end of the algorithm *) are marked at the end of the algorithm *)
ensures { forall n : loc. S.mem n graph /\ n <> null /\ (* update: following Leino's paper, I will specify that all reachable nodes
reachable root n (old !left) (old !right) -> !m[n] } * are marked as a transitive propertie, rather than using reachability *)
(* ensures { forall n : loc. S.mem n graph /\ n <> null /\
reachable root n (old !left) (old !right) -> !m[n] } *)
(* every marked node was reachable from 'root' in the pre-state *) (* every marked node was reachable from 'root' in the pre-state *)
ensures { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] -> ensures { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] ->
reachable root n (old !left) (old !right) } reachable root n (old !left) (old !right) }
...@@ -256,8 +258,8 @@ module SchorrWaite ...@@ -256,8 +258,8 @@ module SchorrWaite
(* lines 61-62 from Leinos' paper --> help establish the post that (* lines 61-62 from Leinos' paper --> help establish the post that
* all nodes reachable from root are marked *) * all nodes reachable from root are marked *)
invariant { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] /\ invariant { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] /\
not (L.mem n !stackNodes) /\ n <> !t -> not (L.mem n !stackNodes) -> (* /\ n <> !t ---> do I really need this 'n <> !t'? *)
(forall ch : loc. edge n ch !left !right /\ ch <> null -> !m[ch]) } (forall ch : loc. edge n ch !left !right /\ ch <> null -> !m[ch]) }
(* termination proved using lexicographic order over a triple *) (* termination proved using lexicographic order over a triple *)
variant { S.cardinal !unmarked_nodes, S.cardinal !c_false_nodes, length !stackNodes } variant { S.cardinal !unmarked_nodes, S.cardinal !c_false_nodes, length !stackNodes }
if !t = null || !m[!t] then begin if !t = null || !m[!t] then begin
......
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