porting programs to mutable types

bench/bench

@@ -58,10 +58,10 @@ drivers () {
 programs () {
     for f in $1/*.mlw; do
 	echo -n "  "$f"... "
-	if ! $pgml $pgml_options $f > /dev/null 2>&1; then 
+	if ! $pgml -L modules $pgml_options $f > /dev/null 2>&1; then 
 	    echo 
 	    echo "$pgml $pgml_options $f"
-	    $pgml $pgml_options $f
+	    $pgml -L modules $pgml_options $f
 	    echo "FAILED!"
 	    exit 1 
         else 
@@ -73,7 +73,7 @@ programs () {
 bad_programs () {
     for f in $1/*.mlw; do
 	echo -n "  "$f"... "
-	if $pgml $pgml_options $f > /dev/null 2>&1; then 
+	if $pgml -L modules $pgml_options $f > /dev/null 2>&1; then 
 	    echo 
 	    echo "$pgml $pgml_options $f"
 	    echo "SHOULD FAIL!"
@@ -87,10 +87,10 @@ bad_programs () {
 valid_goals () {
     for f in $1/*.mlw; do
 	echo -n "  "$f"... "
-	if $pgml -P alt-ergo $f | grep -q -v Valid; then
+	if $pgml -L modules -P alt-ergo $f | grep -q -v Valid; then
 	    echo "valid test $f failed!"
 	    echo "$pgml -P alt-ergo $f"
-	    $pgml -P alt-ergo $f
+	    $pgml -L modules -P alt-ergo $f
 	    exit 1
        else 
 	    echo "ok"
@@ -102,7 +102,7 @@ valid_goals () {
 test_provers () {
     for f in $1/*.mlw; do
 	echo -n "  "$f"... "
-	if $pgml -P alt-ergo $f | grep -q -v Valid; then
+	if $pgml -L modules -P alt-ergo $f | grep -q -v Valid; then
 	    echo "valid test $f failed!"
 	    exit 1
        else 
@@ -123,10 +123,6 @@ echo "=== Checking drivers ==="
 drivers drivers
 echo ""
 
-echo "=== Checking valid goals ==="
-valid_goals bench/valid
-echo ""
-
 echo "=== Parsing good files  ==="
 goods bench/typing/bad --parse-only
 echo ""
@@ -169,6 +165,10 @@ programs bench/programs/good
 programs examples/programs
 echo ""
 
+echo "=== Checking valid goals ==="
+valid_goals bench/valid
+echo ""
+
 echo "=== Checking provers ==="
 echo -n "Test provers on true..."
 provers=$($pgm --list-provers | cut -d " " -f 3 |grep -v "^$")

bench/programs/good/exns.mlw

@@ -8,7 +8,7 @@ let p1 () = {} (raise E : unit) { false } | E -> { true }
 
 (* exception with an argument *)
 
-exception F of int
+exception F int
 
 let p2 () = {} raise (F 1) : unit { false } | F -> { result = 1 }
 
@@ -43,20 +43,22 @@ let p6 () =
 
 (* composition of exceptions with side-effect on a reference *)
 
+use import module stdlib.Ref
+
 parameter x : ref int
 
 let p7 () = 
-  {} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
+  {} begin x := 1; raise E; x := 2 end { false } | E -> { x = 1 }
 
 let p8 () = 
   {}
   begin x := 1; raise (F !x); x := 2 end 
-  { false } | F -> { !x = 1 and result = 1 }
+  { false } | F -> { x = 1 and result = 1 }
 
 let p9 () = 
   {}
   (raise (F begin x := 1; !x end) : unit) 
-  { false } | F -> { !x = 1 and result = 1 }
+  { false } | F -> { x = 1 and result = 1 }
 
 (* try / with *)
 
@@ -80,7 +82,7 @@ let p13 () =
   with E -> x := 2
      | F _ -> x := 3
   end
-  { !x = 2 }
+  { x = 2 }
 
 let p13a () =
   {}
@@ -90,7 +92,7 @@ let p13a () =
   with E ->
     x := 0
   end
-  { !x <> 1 }
+  { x <> 1 }
 
 exception E1 
 exception E2
@@ -104,17 +106,17 @@ let p14 () =
     if !x = 3 then raise E3;
     raise E : unit
   end
-  { false } | E1 -> {  !x = 1 } | E2 -> {  !x = 2 } | E3 -> { !x = 3 } 
-  | E -> { !x <> 1 and !x <> 2 and !x <> 3 }
+  { false } | E1 -> {  x = 1 } | E2 -> {  x = 2 } | E3 -> { x = 3 } 
+  | E -> { x <> 1 and x <> 2 and x <> 3 }
 
 let p15 () = 
   {} 
   if !x = 0 then raise E else (x := 0; raise (F !x)) : unit
-  { false } | E -> { !x=0 } | F -> { result=0 }
+  { false } | E -> { x=0 } | F -> { result=0 }
 
-let p16 () = {} if !x = 0 then (x:=1; raise E) { !x<>0 } | E -> { !x=1 }
+let p16 () = {} if !x = 0 then (x:=1; raise E) { x<>0 } | E -> { x=1 }
 
-let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { !x=0 }
+let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { x=0 }
 
 end
 

bench/programs/good/for.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 (* for loop with invariant *)
 let test1 () =
   let x = ref 0 in
   for i = 1 to 10 do
-    invariant { !x = i-1 }
+    invariant { x = i-1 }
     x := !x + 1
   done;
-  assert { !x = 10 }
+  assert { x = 10 }
 
 (* we don't even enter *)
 let test2 () =
@@ -15,7 +18,7 @@ let test2 () =
   for i = 2 to 1 do
     x := 1
   done;
-  assert { !x = 0 }
+  assert { x = 0 }
 
 exception E
 
@@ -47,17 +50,17 @@ let test4 x =
 let test1d () =
   let x = ref 11 in
   for i = 10 downto 1 do
-    invariant { !x = i+1 }
+    invariant { x = i+1 }
     x := !x - 1
   done;
-  assert { !x = 1 }
+  assert { x = 1 }
 
 let test2d () =
   let x = ref 0 in
   for i = 1 downto 2 do
     x := 1
   done;
-  assert { !x = 0 }
+  assert { x = 0 }
 
 let test3d () =
   { }

bench/programs/good/list.mlw

 module M
 
+  use import int.Int
   use import list.List
   use import list.Length
 

bench/programs/good/loops.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 (** 1. A loop increasing [i] up to 10. *)
 
 parameter i : ref int
 
 let loop1 (u:unit) = 
-  { !i <= 10 }
+  { i <= 10 }
   while !i < 10 do
-    invariant { !i <= 10 } variant { 10 - !i }
+    invariant { i <= 10 } variant { 10 - i }
     i := !i + 1
   done
-  { !i = 10 }
+  { i = 10 }
 
 
 (** 2. The same loop, followed by a function call. *)
 
 parameter x: ref int
 
-let negate (u:unit) = {} x := - !x { !x = -old(!x) }
+let negate (u:unit) = {} x := - !x { x = - (old x) }
 
 let loop2 (u:unit) = 
-  { !x <= 10 }
+  { x <= 10 }
   begin
-    while !x < 10 do invariant { !x <= 10 } variant { 10 - !x } 
+    while !x < 10 do invariant { x <= 10 } variant { 10 - x } 
       x := !x + 1
     done;
-    assert { !x = 10 };
+    assert { x = 10 };
     if !x > 0 then (negate ());
-    assert { !x = -10 }
+    assert { x = -10 }
   end
   {}
 

bench/programs/good/mutual.mlw

 module M
 
+  use import int.Int
   use import int.EuclideanDivision
 
   logic even (x : int) = x = 2 * (div x 2)

bench/programs/good/oldify.mlw

 module M
 
+  use import module stdlib.Ref
+
   logic q1 int int int
 
 parameter r : ref int
 
 parameter f1 : y:int ->
-             {} unit writes r { q1 (!r) (old (!r)) y }
+             {} unit writes r { q1 r (old r) y }
 
-let g1 () = {} f1 !r { q1 (!r) (old (!r)) (old (!r)) }
+let g1 () = {} f1 !r { q1 r (old r) (old r) }
 
   logic foo int : int
   logic q int int int
 
 parameter f : t:ref int -> x:int -> 
-             {} unit reads t writes t { q (!t) (old (!t)) x }
+             {} unit reads t writes t { q t (old t) x }
 
 let g (t:ref int) =
   {}
   f t (foo !t)
-  { q (!t) (old (!t)) (foo (old (!t))) }
+  { q t (old t) (foo (old t)) }
 
 end
 

bench/programs/good/po.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 (* Tests for proof obligations. *)
 
 parameter x : ref int
@@ -8,13 +11,13 @@ parameter x : ref int
 
 (* basic stuff: assignment, sequence and local variables *)
 
-let p1 () = { q(!x+1) } begin x := !x + 1 end { q(!x) }
+let p1 () = { q (x+1) } begin x := !x + 1 end { q x }
 
-let p2 () = { q(7) } begin x := 3 + 4 end { q(!x) }
+let p2 () = { q 7 } begin x := 3 + 4 end { q x }
 
-let p3 () = {} begin x := !x + 1; x := !x + 2 end { !x = old(!x) + 3 }
+let p3 () = {} begin x := !x + 1; x := !x + 2 end { x = (old x) + 3 }
 
-let p4 () = {} begin x := 7; x := 2 * !x end { !x = 14 }
+let p4 () = {} begin x := 7; x := 2 * !x end { x = 14 }
 
 let p5 () = {} 3 + 4 { result = 7 }
 
@@ -25,14 +28,14 @@ let p7 () = {} 3 + (let a = 4 in a + a) { result = 11 }
 (* side effects in function arguments *)
 
 let p8 () = 
-  { q(!x+1) } 3 + begin x := !x + 1; !x end { q(!x) and result = old(!x) + 4 }
+  { q (x+1) } 3 + begin x := !x + 1; !x end { q x and result = (old x) + 4 }
 
 (* evaluation order (argument first) *)
 
 let p9 () = 
-  {} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and !x = 2 }
+  {} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and x = 2 }
 
-let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and !x = 1 }
+let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and x = 1 }
 
 (* function with a post-condition *)
 
@@ -46,19 +49,19 @@ let p11a () = {} let a = (fsucc 1) in a + a { result = 4 }
 
 (* function with a post-condition and side-effects *)
 
-parameter incrx : unit -> { } unit writes x { !x = old(!x) + 1 }
+parameter incrx : unit -> { } unit writes x { x = (old x) + 1 }
 
-let p12 () = { !x = 0 } incrx () { !x = 1 }
+let p12 () = { x = 0 } incrx () { x = 1 }
 
-let p13 () = {} begin incrx (); incrx () end { !x = old(!x) + 2 }
+let p13 () = {} begin incrx (); incrx () end { x = (old x) + 2 }
 
-let p13a () = {} incrx (incrx ()) { !x = old(!x) + 2 }
+let p13a () = {} incrx (incrx ()) { x = (old x) + 2 }
 
 (* function with side-effects, result and post-condition *)
 
-parameter incrx2 : unit -> { } int writes x { !x = old(!x) + 1 and result = !x }
+parameter incrx2 : unit -> { } int writes x { x = old x + 1 and result = x }
 
-let p14 () = { !x = 0 } incrx2 () { result = 1 }
+let p14 () = { x = 0 } incrx2 () { result = 1 }
 
 end
 

bench/programs/good/recfun.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 (** Recursive functions *)
 
 (** 1. Pure function *)
@@ -11,33 +14,35 @@ let rec f1 (x:int) : int variant { x } =
 
 parameter x : ref int
 
-let rec f2 (u:unit) : unit variant { !x } =
-  { !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
+let rec f2 (u:unit) : unit variant { x } =
+  { x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { x = 0 }
 
 (** 3. With effects and a pure argument *)
 
 let rec f3 (a:int) : unit variant { a } =
   { a >= 0 } 
   if a > 0 then begin x := !x + 1; (f3 (a-1)) end
-  { !x = old !x + a }
+  { x = old x + a }
 
 (** 4. With effects and a reference as argument *)
 
-let rec f4 (a:ref int) : unit variant { !a } =
-  { !a >= 0 } 
+let rec f4 (a:ref int) : unit variant { a } =
+  { a >= 0 } 
   if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
-  { !x = old !x + old !a }
+  { x = old x + old a }
 
 (** 5. The acid test: 
        partial application of a recursive function with effects *)
 
-let rec f5 (a b:ref int) variant { !a } = 
-  { !a >= 0 } 
+(* FIXME
+let rec f5 (a b:ref int) variant { a } = 
+  { a >= 0 } 
   if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end 
-  { result = old !a + old !b }
+  { result = old a + old b }
 
 let test_f5 () = 
-  { !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
+  { x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
+*)
 
 end
 

bench/programs/good/see.mlw

@@ -10,7 +10,7 @@ parameter b1 : ref int
 parameter b2 : ref int
 
 let f () = 
-  {} b := 1 - !b; !b { result = !b and !b = 1 - old(!b) }
+  {} b := 1 - !b; !b { result = b and b = 1 - old b }
 
 let k () = 
   {} 
@@ -19,7 +19,7 @@ let k () =
     b1 := (1 - (f ())) + (f ());
     b2 := (f ()) * (1 - (f ())) 
   end
-  { !b1 = 0 and !b2 = 1 }
+  { b1 = 0 and b2 = 1 }
 
 end
 

bench/programs/good/set.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 (* side effects in tests *)
 
 parameter x : ref int
 
 parameter set_and_test_zero : 
   v:int -> 
-    {} bool writes x { !x = v and if result=True then !x = 0 else !x <> 0 }
+    {} bool writes x { x = v and if result=True then x = 0 else x <> 0 }
 
 let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
 
 parameter set_and_test_nzero : 
   v:int -> 
-    {} bool writes x { !x = v and if result=True then !x <> 0 else !x = 0 }
+    {} bool writes x { x = v and if result=True then x <> 0 else x = 0 }
 
 let p2 (y:ref int) = 
-  { !y >= 0 } 
+  { y >= 0 } 
   while set_and_test_nzero !y do 
-    invariant { !y >= 0 } variant { !y } 
+    invariant { y >= 0 } variant { y } 
     y := !y - 1 
   done 
-  { !y = 0 }
+  { y = 0 }
 
 let p3 (y:ref int) = 
-  { !y >= 0 } 
+  { y >= 0 } 
   while let b = set_and_test_nzero !y in b do 
-    invariant { !y >= 0 } variant { !y } 
+    invariant { y >= 0 } variant { y } 
     y := !y - 1 
   done 
-  { !y = 0 }
+  { y = 0 }
 
 let p4 (y:ref int) = 
-  { !y >= 1 } 
+  { y >= 1 } 
   while begin y := !y - 1; (set_and_test_nzero !y) end do 
-    invariant { !y >= 1 } variant { !y } 
+    invariant { y >= 1 } variant { y } 
     ()
   done 
-  { !y = 0 }
+  { y = 0 }
 
 end
 

bench/programs/good/wpcalls.mlw

 module M
 
+use import int.Int
+use import module stdlib.Ref
+
 parameter x : ref int
 
-parameter f : unit -> { } unit writes x { !x = 1 - old (!x) }
+parameter f : unit -> { } unit writes x { x = 1 - old x }
 
 let p () =
   begin
@@ -10,7 +13,7 @@ let p () =
     let t = () in ();
     (f ());
     (f ());
-    assert { !x = at (!x) Init };
+    assert { x = at x Init };
     ()
   end
 

examples/programs/binary_search.mlw

 module M
 
-(* Binary search
-
-   The classical example. Searches a sorted array for a given value v. 
-*)
-
-(* the usual array modeling *)
-
-  use array.ArrayLength as A
+  use import int.Int
   use import int.ComputerDivision
+  use import module stdlib.Ref
+  use import module stdlib.Array
 
-  type array = A.t int int
-
-  logic (#) (a : array) (i : int) : int = A.get a i
+  (* Binary search
 
-let array_get (a : ref array) i = 
-  { 0 <= i < A.length !a } A.get !a i { result = A.get !a i }
-
-let array_set (a : ref array) i v = 
-  { 0 <= i < A.length !a } a := A.set !a i v { !a = A.set (old !a) i v }
-
-let length (a : ref array) =
-  { } A.length !a { result = A.length !a }
-
-(* the code and its specification *)
-
-exception Break of int (* raised to exit the loop *)
-exception Not_found    (* raised to signal a search failure *)
-
-let binary_search (a : ref array) (v : int) =
-  { forall i1 i2 : int. 0 <= i1 <= i2 < A.length !a -> !a#i1 <= !a#i2 }
-  try
-    let l = ref 0 in
-    let u = ref (length a - 1) in
-    while !l <= !u do
-      invariant {
-	0 <= !l and !u < A.length !a and 
-        forall i : int. 0 <= i < A.length !a -> !a#i = v -> !l <= i <= !u }
-      variant { !u - !l }
-      let m = !l + div (!u - !l) 2 in
-      assert { !l <= m <= !u };
-      if array_get a m < v then
-        l := m + 1
-      else if array_get a m > v then
-        u := m - 1
-      else 
-        raise (Break m)
-    done;
-    raise Not_found
-  with Break i ->
-    i
-  end
-  { 0 <= result < A.length !a and !a#result = v }
-  | Not_found -> { forall i:int. 0 <= i < A.length !a -> !a#i <> v }
+   The classical example. Searches a sorted array for a given value v. 
+  *)
+
+  (* the code and its specification *)
+
+  exception Break int (* raised to exit the loop *)
+  exception Not_found (* raised to signal a search failure *)
+
+  let binary_search (a :array int) (v : int) =
+    { forall i1 i2 : int. 0 <= i1 <= i2 < A.length a -> a#i1 <= a#i2 }
+    try
+      let l = ref 0 in
+      let u = ref (length a - 1) in
+      while !l <= !u do
+        invariant {
+	  0 <= l and u < A.length a and 
+          forall i : int. 0 <= i < A.length a -> a#i = v -> l <= i <= u }
+        variant { u - l }
+        let m = !l + div (!u - !l) 2 in
+        assert { l <= m <= u };
+        if get a m < v then
+          l := m + 1
+        else if get a m > v then
+          u := m - 1
+        else 
+          raise (Break m)
+      done;
+      raise Not_found
+    with Break i ->
+      i
+    end
+    { 0 <= result < A.length a and a#result = v }
+    | Not_found -> { forall i:int. 0 <= i < A.length a -> a#i <> v }
 
 end
 

examples/programs/bresenham.mlw

@@ -3,6 +3,7 @@ module M
 (* Bresenham line drawing algorithm. *)
 
 use import int.Int
+use import module stdlib.Ref
 
 (*  Parameters. 
     Without loss of generality, we can take [x1=0] and [y1=0]. 
@@ -38,10 +39,10 @@ let bresenham () =
   let y = ref 0 in
   let e = ref (2 * y2 - x2) in
   while !x <= x2 do
-    invariant {0 <= !x and !x <= x2 + 1 and invariant_ !x !y !e }
-    variant   { x2 + 1 - !x }
+    invariant {0 <= x and x <= x2 + 1 and invariant_ x y e }
+    variant   { x2 + 1 - x }
     (* here we would plot (x, y) *) 
-    assert { best !x !y };
+    assert { best x y };
     if !e < 0 then
       e := !e + 2 * y2
     else begin

examples/programs/course.mlw

 module M
 
+  use import int.Int
+  use import module stdlib.Ref
+ 
   (* preliminaries *)
 
   use array.Array as A
@@ -31,7 +34,7 @@ parameter new_pointer : tt:unit ->
   { }
   pointer
   writes alloc
-  { !alloc = old !alloc + 1 and result = old !alloc }
+  { alloc = old alloc + 1 and result = old alloc }
 
 (*
 record Student =
@@ -128,9 +131,9 @@ let createCourse (r: (ref (region course))) : pointer =
     let (rStud,student,count,sum) = A.get !r c in
     let newc = (rStud,student,0,0) in
     r := A.set !r c newc;
-    assert { invCourse !alloc newc };
+    assert { invCourse alloc newc };
     c
-  { valid !alloc result }
+  { valid alloc result }
 
 (*
 fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
@@ -149,15 +152,15 @@ fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
 
 let registerStudent
     (r: (ref (region course))) (c:pointer) (name:string) : pointer =
-{ valid !alloc c and invCourse !alloc (A.get !r c) }
+{ valid alloc c and invCourse alloc (A.get r c) }
   let s = new_pointer () in
   let (rStud,student,count,sum) = A.get !r c in
   let newstud = (name,0) in
   let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
   r := A.set !r c newc;
-  assert { invCourse !alloc newc };
+  assert { invCourse alloc newc };
   s
-{ valid !alloc result }
+{ valid alloc result }
 
 (*
 
@@ -178,8 +181,8 @@ fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
 
 end
 
-
-
-
-
-
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/course"
+End: 
+*)

examples/programs/dijkstra.mlw

 module M
 
+  use import int.Int
+  use import module stdlib.Ref
   use set.Fset as S
   use array.Array as M
 
@@ -9,13 +11,13 @@ parameter set_has_next :
   s:ref (S.t 'a) -> 
     {} 
     bool reads s 
-    { if result=True then S.is_empty !s else not S.is_empty !s }
+    { if result=True then S.is_empty s else not S.is_empty s }
 
 parameter set_next :
   s:ref (S.t 'a) -> 
-    { not S.is_empty !s }
+    { not S.is_empty s }
     'a writes s 
-    { S.mem result (old !s) and !s = S.remove result (old !s) }
+    { S.mem result (old s) and s = S.remove result (old s) }
 
 (* the graph *)
 
@@ -41,7 +43,7 @@ parameter eq_vertex :
 parameter visited : ref (S.t vertex)
 
 parameter visited_add : 
-  x:vertex -> {} unit writes visited { !visited = S.add x (old !visited) }
+  x:vertex -> {} unit writes visited { visited = S.add x (old visited) }
 
 (* current distances *)
 
@@ -55,15 +57,15 @@ parameter q_is_empty :
   unit -> 
     {} 
     bool reads q 
-    { if result=True then S.is_empty !q else not S.is_empty !q }
+    { if result=True then S.is_empty q else not S.is_empty q }
 
 parameter init :
   src:vertex ->
     {} 
     unit writes visited q d 
-    { S.is_empty !visited and 
-      !q = S.add src S.empty and 
-      !d = M.set (old !d) src 0  }
+    { S.is_empty visited and 
+      q = S.add src S.empty and 
+      d = M.set (old d) src 0  }
 
 let relax u v =
   {}
@@ -75,16 +77,16 @@ let relax u v =
       q := S.add v !q;
       d := M.set !d v x
     end
-  { (S.mem v !visited and !q = old !q and !d = old !d) 
+  { (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) 
+    (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 (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))
+    (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 (old !q) and !q = S.add v (old !q) and
-        !d = M.set (old !d) v (M.get (old !d) u + weight u v)) }	
+    (not S.mem v visited and not S.mem v (old 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 
@@ -92,9 +94,9 @@ logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
 
 parameter q_extract_min :
   unit ->
-    { not S.is_empty !q } 
+    { not S.is_empty q } 
     vertex reads d writes q 
-    { min result (old !q) !d and !q = S.remove result (old !q) }
+    { min result (old q) d and q = S.remove result (old q) }
 
 (* paths and shortest paths 
    path x y d = 
@@ -184,26 +186,26 @@ let shortest_path_code (src:vertex) (dst:vertex) =
   { S.mem src v and S.mem dst v }
   init src;
   while not (q_is_empty ()) do
-    invariant { inv src !visited !q !d and inv_succ src !visited !q }