programs: new bench loops.mlw

bench/programs/good/loops.mlw

+
+(** 1. A loop increasing [i] up to 10. *)
+
+parameter i : int ref
+
+let loop1 (u:unit) = 
+  { !i <= 10 }
+  while !i < 10 do
+    invariant { !i <= 10 } variant { 10 - !i }
+    i := !i + 1
+  done
+  { !i = 10 }
+
+
+(** 2. The same loop, followed by a function call. *)
+
+parameter x: int ref
+
+let negate (u:unit) = {} x := - !x { !x = -old(!x) }
+
+let loop2 (u:unit) = 
+  { !x <= 10 }
+  begin
+    while !x < 10 do invariant { !x <= 10 } variant { 10 - !x } 
+      x := !x + 1
+    done;
+    assert { !x = 10 };
+    if !x > 0 then (negate ());
+    assert { !x = -10 }
+  end
+  {}
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/loops"
+End: 
+*)

bench/valid/loops.mlw

+../programs/good/loops.mlw
\ No newline at end of file

examples/programs/vacid_0_sparse_array.mlw

 
+(*
+      If the sparse array contains three elements x y z, at index
+      a b c respectively, then the three arrays look like this:
+
+             b     a      c 
+val   +-----+-+---+-+----+-+----+
+      |     |y|   |x|    |z|    |
+      +-----+-+---+-+----+-+----+
+
+idx   +-----+-+---+-+----+-+----+
+      |     |1|   |0|    |2|    |  
+      +-----+-+---+-+----+-+----+
+
+       0 1 2  n=3
+back  +-+-+-+-------------------+
+      |a|b|c|                   |
+      +-+-+-+-------------------+
+
+*)
+
 {
   use array.ArrayLength as A