programs/examples/dijkstra: implementation of relax (in progress)

examples/programs/dijkstra.mlw

@@ -66,25 +66,31 @@ parameter init :
       !q = S.add src S.empty and 
       !d = M.set (old !d) src 0  }
 
-parameter relax :
-  u:vertex -> v:vertex -> 
-    {} 
-    unit reads visited writes d,q 
-    { (S.mem v !visited and !q = old !q and !d = old !d) 
-      or
-      (S.mem v !q and M.get !d u + weight u v >= M.get !d v and 
+let relax u v =
+  {}
+  if not (S.mem v !visited) then
+    let x = M.get !d u + weight u v in
+    if S.mem v !q then begin
+      if x < M.get !d v then d := M.set !d v x
+    end else begin
+      q := S.add v !q;
+      d := M.set !d v x
+    end
+  { (S.mem v !visited and !q = old !q and !d = old !d) 
+    or
+    (S.mem v !q and M.get !d u + weight u v >= M.get !d v and 
         !q = old !q and !d = old !d) 
-      or	
-      (S.mem v !q  and M.get !d u + weight u v < M.get !d v and 
-        !q = old !q and !d = M.set (old !d) v (M.get !d u + weight u v))
-      or
-      (not S.mem v !visited and not S.mem v !q and !q = S.add v (old !q) and
-        !d = M.set (old !d) v (M.get !d u + weight u v)) }	
+    or	
+    (S.mem v !q  and M.get (old !d) u + weight u v < M.get (old !d) v and 
+        !q = old !q and !d = M.set (old !d) v (M.get (old !d) u + weight u v))
+    or
+    (not S.mem v !visited and not S.mem v !q and !q = S.add v (old !q) and
+        !d = M.set (old !d) v (M.get (old !d) u + weight u v)) }	
 
 {
 logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
   S.mem m q and 
-  forall x:vertex. S.mem x q -> M.get d x <= M.get d m
+  forall x:vertex. S.mem x q -> M.get d m <= M.get d x
 }
 
 parameter q_extract_min :

tests/test-jcf.why

@@ -4,7 +4,7 @@
 theory Test
   use import int.Int
   logic (*) int int
-  goal G : forall x : int. 1 * 2 -> x * 3
+  goal G : not 1=2 and 3=4
 end
 
 

tests/test-pgm-jcf.mlw

 
 {
-  use import list.List
 }
 
-parameter assign : r : ref 'a -> 'a -> unit
-
-parameter alloc : 'a -> ref 'a
-
-parameter head : list 'a -> 'a
-
-exception E of 'a
-
 let f x =
-  { x > 0 }
-  assert { x >= 0 };
-  let y = x+1 in
-  assert { y > 1 };
-  ()
   {}
+  if x = 1 then
+    1
+  else
+    if x = 2 then
+      2
+    else
+      3
+  {    x = 1
+    or (not x = 1 and x = 2)
+    or (not x = 1 and not x = 2 and result = 3) }
 
 (*
 Local Variables: