Proof in progress (Schorr-Waite)

examples/in_progress/schorr_waite.mlw

@@ -44,7 +44,7 @@ module SchorrWaite
     ensures  { result = !right[p] }
 
   val get_path_from_root (p : loc) : list loc
-    requires { p <> null }
+    (*requires { p <> null } ---> maybe I don't need this pre-condition *)
     ensures  { result = !path_from_root[p] }
 
   val set_left (p: loc) (v: loc) : unit
@@ -157,7 +157,7 @@ module SchorrWaite
   lemma path_edge_cons : forall n x y : loc, left right : map loc loc, pth : list loc.
     reachable_via n x left right pth -> edge x y left right ->
     reachable_via n y left right (pth ++ (Cons x Nil))
-
+  
   let schorr_waite (root: loc) (graph : set loc) : unit
     requires { root <> null /\ S.mem root graph }
     (* what is set S --> closed under children of all vertices *)
@@ -175,7 +175,7 @@ module SchorrWaite
     (* all the non-null vertices reachable from root
        are marked at the end of the algorithm *)
     (* update: following Leino's paper, I will specify that all reachable nodes
-     * are marked as a transitive propertie, rather than using reachability *)
+     * are marked as a transitive property, 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 *)	       
@@ -199,7 +199,7 @@ module SchorrWaite
     let ghost unmarked_nodes = ref graph in
     let ghost c_false_nodes = ref graph in
     while !p <> null || (!t <> null && not !m[!t]) do
-      (*invariant { not (L.mem !t !stackNodes) } *)
+      invariant { not (L.mem null !stackNodes) }
       invariant { !stackNodes = Nil <-> !p = null }
       invariant { S.mem !t graph }
       invariant { !p <> null -> S.mem !p graph }
@@ -222,6 +222,11 @@ module SchorrWaite
       		  let first = hd (reverse !stackNodes) in
       		  if !c[first] then !right[first] = null
 		  else !left[first] = null }
+      (* something like lines 75-76 from Leino's paper --> with this invariant I believe there
+       * is no need to use 'stack_form' *)
+      invariant { forall k : int. 0 <= k < length !stackNodes - 1->
+      		  if !c[nth k !stackNodes] then !right[nth k !stackNodes] = nth (k+1) !stackNodes
+		  else !left[nth k !stackNodes] = nth (k+1) !stackNodes }
       (* all nodes in the stack are marked ---> I4a from Hubert and Marché's paper
        * and something alike line 57 from Leino's paper *)
       invariant { forall n : loc. L.mem n !stackNodes -> !m[n] }
@@ -259,15 +264,19 @@ module SchorrWaite
        * all nodes reachable from root are marked *)
       invariant { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] /\
       		  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]) }
+      (* help establishing the previous invariant for the pop case --->
+       * something like Leino's lines 57-59 *)
+      invariant { forall n : loc. L.mem n !stackNodes -> !c[n] ->
+      		  (forall ch : loc. edge n ch !left !right /\ ch <> null -> !m[ch]) }
       (* termination proved using lexicographic order over a triple *)
       variant   { S.cardinal !unmarked_nodes, S.cardinal !c_false_nodes, length !stackNodes }
       if !t = null || !m[!t] then begin
         if !c[!p] then begin (* pop *)
           let q = !t in
           t := !p;
-          p := !right[!p];
 	  stackNodes := tl_stackNodes !stackNodes;
+          p := !right[!p];
           set_right !t q;
 	  pth := get_path_from_root !p;
         end else begin (* swing *)
@@ -292,9 +301,14 @@ module SchorrWaite
 	set_path_from_root !p !pth;
 	(* this is assertion is automatically discharged and it helps 
  	 * proving that all marked nodes are reachable from root *)
-	(*assert { path (at !left 'Init) (at !right 'Init) root !p !pth }; *)
-        (*set_c !p false;*) (* if we assume at the pre-condition that all nodes start with c = 0,
-		   	       then this redundant *)
+	assert { path (at !left 'Init) (at !right 'Init) root !p !pth };
+        set_c !p false; (* if we assume at the pre-condition that all nodes start with c = 0,
+		   	 * then this redundant;
+			 * update: explicitly changing !c[p] to false and adding it to the
+			 * set of false nodes (even if it is already there) helps in proving
+			 * the invariant that all nodes in the stack with !c=1 have their 
+			 * children marked *)
+	c_false_nodes := S.add !p !c_false_nodes;
 	unmarked_nodes := S.remove !p !unmarked_nodes
       end
     done