whyml: new specification syntax

bench/programs/bad-typing/alias1.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   let foo (x : ref int) (y : ref int) =
     x := 1;

bench/programs/bad-typing/alias2.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   let foo (x : ref int) (y : ref int) =
     x := 1;

bench/programs/bad-typing/alias3.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   let foo (x : ref int) (y : ref int) =
     x := 1;

bench/programs/bad-typing/alias4.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   val r : ref int
 

bench/programs/bad-typing/alias5.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   let foo (x : ref int) (y: ref int) =
     x := 1;

bench/programs/bad-typing/at1.mlw

 module M
 
   use import int.Int
-  use import module ref.Ref
+  use import ref.Ref
 
-  let test (a: (ref int, int)) =
-    {}
-    let (r,_) = a in r := !r + 1
-    { let (x, _) = a in !x = (old !x) + 1 }
+  let test (a: (ref int, int))
+    ensures { let (x, _) = a in !x = (old !x) + 1 }
+  = let (r,_) = a in r := !r + 1
 
 end
 

bench/programs/bad-typing/at2.mlw

 module M
 
   use import int.Int
-  use import module ref.Ref
+  use import ref.Ref
 
   let test (a: (ref int, int)) =
  'L:

bench/programs/bad-typing/effect1.mlw

 
 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
-  val f : x:int -> {} unit writes a.contents {}
+  val f (x:int) : unit writes {a.contents}
 
 end

bench/programs/bad-typing/effect2.mlw

 
 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
-  val f : x:int -> {} unit writes x.contents {}
+  val f (x:int) : unit writes { x.contents }
 
 end

bench/programs/bad-typing/effect3.mlw

 
 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   val a : int
 
-  val f : x:int -> {} unit writes a.contents {}
+  val f (x:int) : unit writes { a.contents }
 
 end

bench/programs/bad-typing/effect4.mlw

 
 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
-  val foo : int -> int
+  val foo (_x : int) : int
 
-  val f : x:int -> {} unit writes foo.contents {}
+  val f (x:int) : unit writes { foo.contents }
 
 end

bench/programs/bad-typing/effect5.mlw

 
 module M
 
-  val f : x:int -> {} unit writes 1 {}
+  val f (x:int) : unit writes { 1 }
 
 end

bench/programs/bad-typing/effect6.mlw

 
 module M
 
-  val f : x:int -> {} unit writes x {}
+  val f (x:int) : unit writes {x}
 
 end

bench/programs/bad-typing/effect7.mlw

@@ -3,10 +3,10 @@ module Bad
   use import int.Int
   use import ref.Ref
 
-  let f (x y : ref int) : unit =
-  { !x = !y }
-    x := !x + 1
-  { !x = !y + 1 }
+  let f (x y : ref int) : unit
+    requires { !x = !y }
+    ensures  { !x = !y + 1 }
+  = x := !x + 1
 
   let g () : unit =
     let r = ref 0 in

bench/programs/bad-typing/escape1.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   (* reference would escape its scope *)
 
   let test () =
     let x = ref 0 in
-    fun y -> { } x := y; !x { result = !x }
+    fun y -> ensures { result = !x } x := y; !x
 
 end

bench/programs/bad-typing/old1.mlw

 module M
   use import int.Int
-  use import module ref.Ref
-  let test1 (x: ref int) =
-    { !x >= 0}
-    while !x > 0 do
+  use import ref.Ref
+  let test1 (x: ref int)
+    requires { !x >= 0 }
+    ensures  { !x >= old !x }
+  = while !x > 0 do
       invariant { !x >= old !x }
       x := !x - 1
     done
-    { !x >= old !x }
 end
 
 (*

bench/programs/bad-typing/old2.mlw

 module M
   use import int.Int
-  use import module ref.Ref
-  let test1 (x: ref int) =
-    { !x >= 0}
-    x := !x - 1;
+  use import ref.Ref
+  let test1 (x: ref int)
+    ensures  { !x >= old !x }
+    requires { !x >= 0}
+  = x := !x - 1;
     assert { !x >= old !x }
-    { !x >= old !x }
 end
 
 (*

bench/programs/bad-typing/old3.mlw

@@ -2,7 +2,7 @@
 
 module Test
 
-  use import module ref.Refint
+  use import ref.Refint
 
   let test (x: ref int) =
     if !x = old !x then 1 else 2

bench/programs/bad-typing/polyref1.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
 
   val r : ref 'a
 

bench/programs/bad-typing/polyref3.mlw

 module M
 
-  use import module ref.Ref
+  use import ref.Ref
   use import list.List
 
   val r : ref (list 'a)

bench/programs/bad-typing/reset1.mlw

@@ -3,12 +3,11 @@ module Bad
   use import int.Int
   use import ref.Ref
 
-  type dref 'a = {| mutable dcontents : ref 'a |}
+  type dref 'a = { mutable dcontents : ref 'a }
 
-  let one (x : dref 'a) (y : ref 'a) =
-  { }
-    x.dcontents <- y;
+  let one (x : dref 'a) (y : ref 'a)
+    ensures { !(x.dcontents) = !(old y) }
+  = x.dcontents <- y;
     y
-  { !(x.dcontents) = !(old y) }
 
 end

bench/programs/bad-typing/reset2.mlw

@@ -3,11 +3,10 @@ module Bad
   use import int.Int
   use import ref.Ref
 
-  type dref 'a = {| mutable dcontents : ref 'a |}
+  type dref 'a = { mutable dcontents : ref 'a }
 
-  let one (x : dref 'a) (y : ref 'a) =
-  { }
-    x.dcontents <- y
-  { !(x.dcontents) = !y }
+  let one (x : dref 'a) (y : ref 'a)
+    ensures { !(x.dcontents) = !y }
+  = x.dcontents <- y
 
 end

bench/programs/bad-typing/theory1.mlw

-(* a theory is not a module *)
-
-theory T
-end
-
-module M
-  use import module T
-end

bench/programs/bad-typing/variant2.mlw

@@ -7,7 +7,7 @@ module M
 
   predicate rel int int
 
-  let rec even (x:int) : int variant {x} with rel =
+  let rec even (x:int) : int variant {x with rel} =
     odd (x-1)
   with odd (x:int) : int variant {x} =
     even (x-1)

bench/programs/bad-typing/with1.mlw

@@ -2,10 +2,10 @@ module M
 
   use import int.Int
 
-  type t 'a = {| a: 'a; b: bool; c: 'a |}
+  type t 'a = { a: 'a; b: bool; c: 'a }
 
   let test1 (x: t bool) =
-    {| x with a = 0 |}
+    { x with a = 0 }
 
 end
 

bench/programs/bad-typing/with2.mlw

@@ -2,10 +2,10 @@ module M
 
   use import int.Int
 
-  type t 'a = {| a: 'a; b: bool; c: 'a |}
+  type t 'a = { a: 'a; b: bool; c: 'a }
 
   let test1 (x: t bool) =
-    {| x with a = 0; c = True |}
+    { x with a = 0; c = True }
 
 end
 

bench/programs/good/booleans.mlw

 module M
 
 use import int.Int
-use import module ref.Ref
+use import ref.Ref
 
-val incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
+val incr (x:ref int) : unit writes {x} ensures { !x = old !x + 1 }
 
 val x : ref int
 
-val id_not_0 : x:int -> { x <> 0 } int { result = x }
+val id_not_0 (x:int) : int requires { x <> 0 } ensures { result = x }
 
-val id : x:int -> { } int { result = x }
+val id (x:int) : int ensures { result = x }
 
-let test_and_1 () =
-  { }
-  if (incr x; !x > 0) && id !x = 1 then !x else 0+1
-  { result = 1 }
+let test_and_1 ()
+  ensures  { result = 1 }
+  = if (incr x; !x > 0) && id !x = 1 then !x else 0+1
 
-let test_and_2 () =
-  { !x <> 0 }
-  if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
-  { result = 1 }
+let test_and_2 ()
+  requires { !x <> 0 }
+  ensures  { result = 1 }
+  = if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
 
-let test_or_1 () =
-  { }
-  if (incr x; !x > 0) || !x < 0 then 1 else 2
-  { result = 1 -> !x <> 0 }
+let test_or_1 ()
+  ensures  { result = 1 -> !x <> 0 }
+  = if (incr x; !x > 0) || !x < 0 then 1 else 2
 
-let test_or_2 () =
-  { }
-  if !x = 0 || !x = 1 then !x else 1
-  { 0 <= result <= 1 }
+let test_or_2 ()
+  ensures  { 0 <= result <= 1 }
+  = if !x = 0 || !x = 1 then !x else 1
 
-let test_not_1 () =
-  { }
-  if not (!x = 0) then x := 0
-  { !x = 0 }
+let test_not_1 ()
+  ensures  { !x = 0 }
+  = if not (!x = 0) then x := 0
 
-let test_not_2 () =
-  { !x <= 0 }
-  while not (!x = 0) do invariant { !x <= 0 } incr x done
-  { !x = 0 }
+let test_not_2 ()
+  requires { !x <= 0 }
+  ensures  { !x = 0 }
+  = while not (!x = 0) do invariant { !x <= 0 } incr x done
 
-let test_all_1 () =
-  { }
-  (!x >= 0 && not (!x = 0) || !x >= 1)
-  { result=True <-> !x>=1 }
+let test_all_1 ()
+  ensures  { result=True <-> !x>=1 }
+  = (!x >= 0 && not (!x = 0) || !x >= 1)
 
 (* from Cesar Munoz's CD3D *)
 
-  function d : int
+function d : int
 
 val vx : ref int
 val vy : ref int
 
-val sq : x:int -> {} int { result = x*x }
+val sq (x:int) : int ensures { result = x*x }
 
-let test_cd3d () =
- { true }
- if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d  then 1 else 2
- { result=1 -> !vx=0 /\ !vy=0 }
+let test_cd3d ()
+  ensures { result=1 -> !vx=0 /\ !vy=0 }
+  = if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
 
 end
 

bench/programs/good/complex_arg_1.mlw

@@ -2,21 +2,13 @@ module M
 
 exception Exception
 
-val f0 : tt:unit ->
-   { }
-   unit
-   { true }
+val f0 (tt:unit) : unit
 
-val f1 : tt:unit ->
-  { }
-  unit
-  raises Exception
-  { true } | Exception -> { true }
+val f1 (tt:unit) : unit raises { Exception }
 
-let f () =
-  { }
-  f0 (f1 ())
-  { true } | Exception -> { true }
+let f ()
+  raises { Exception -> true }
+  = f0 (f1 ())
 
 end
 

bench/programs/good/complex_arg_2.mlw

@@ -2,19 +2,13 @@ module M
 
 exception Exception int
 
-use import module ref.Ref
+use import ref.Ref
 
 val t : ref int
 
-val m : a:int -> b:int ->
-    { }
-    unit reads t raises Exception
-    { true } | Exception -> { true }
+val m (a:int) (b:int) : unit reads {t} raises { Exception }
 
-let test () =
-  { }
-  (m ( assert { true } ; 0) 0)
-  { true } | Exception -> { true }
+let test () raises { Exception } = (m ( assert { true } ; 0) 0)
 
 end
 

bench/programs/good/exceptions.mlw

 module M
 
 use import int.Int
-use import module ref.Ref
+use import ref.Ref
 
 exception Break
 
-let f (n : int) : int  =
-  { true }
-  let i = ref n in
+let f (n : int) : int ensures { result <= 10 }
+= let i = ref n in
   try
     while (!i > 0) do
       invariant { true }
@@ -18,7 +17,6 @@ let f (n : int) : int  =
   with Break -> ()
   end;
   !i
-  { result <= 10 }
 
 end
 

bench/programs/good/exns.mlw

@@ -4,119 +4,104 @@ module M
 
 exception E
 
-let p1 () = {} (raise E : unit) { false } | E -> { true }
+let p1 () ensures { false } raises { E -> true }
+= raise E : unit
 
 (* exception with an argument *)
 
 exception F int
 
-let p2 () = {} raise (F 1) : unit { false } | F -> { result = 1 }
+let p2 () ensures { false } raises { F result -> result = 1 }
+= raise (F 1) : unit
 
-let p2a () =
-  {} raise (F (raise E : int)) : unit { false } | E -> { true } | F -> { false }
+let p2a () ensures { false } raises { E -> true | F _ -> false }
+= raise (F (raise E : int)) : unit
 
 (* composition of exceptions with other constructs *)
 
-let p3 () =
-  {} begin raise (F 1); raise (F 2) : unit end { false } | F -> { result = 1 }
+let p3 () ensures { false } raises { F result -> result = 1 }
+= begin raise (F 1); raise (F 2) : unit end
 
-let p4 () =
-  {}
-  (if True then raise (F 1) else raise (F 2)) : unit
-  { false } | F -> { result = 1 }
+let p4 () ensures { false } raises { F result -> result = 1 }
+= (if True then raise (F 1) else raise (F 2)) : unit
 
-let p5 () =
-  {}
-  begin
+let p5 () ensures { false } raises { E -> false | F result -> result = 1 }
+= begin
     if True then raise (F 1);
     raise E : unit
   end
-  { false } | E -> { false } | F -> { result = 1 }
 
-let p6 () =
-  {}
-  begin
+let p6 () ensures { false } raises { E -> true | F _ -> false }
+= begin
     if False then raise (F 1);
     raise E : unit
   end
-  { false } | E -> { true } | F -> { false }
 
 (* composition of exceptions with side-effect on a reference *)
 
-use import module ref.Ref
+use import ref.Ref
 
 val x : ref int
 
-let p7 () =
-  {} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
+let p7 () ensures { false } raises { E -> !x = 1 }
+= begin x := 1; raise E; x := 2 end
 
-let p8 () =
-  {}
-  begin x := 1; raise (F !x); x := 2 end
-  { false } | F -> { !x = 1 /\ result = 1 }
+let p8 () ensures { false } raises { F result -> !x = 1 /\ result = 1 }
+= begin x := 1; raise (F !x); x := 2 end
 
-let p9 () =
-  {}
-  (raise (F begin x := 1; !x end) : unit)
-  { false } | F -> { !x = 1 /\ result = 1 }
+let p9 () ensures { false } raises { F result -> !x = 1 /\ result = 1 }
+= (raise (F begin x := 1; !x end) : unit)
 
 (* try / with *)
 
-let p10 () = {} (try raise E : int with E -> 0 end) { result = 0 }
+let p10 () ensures { result = 0 } = (try raise E : int with E -> 0 end)
 
-let p11 () = {} (try raise (F 1) : int with F x -> x end) { result = 1 }
+let p11 () ensures { result = 1 } = (try raise (F 1) : int with F x -> x end)
 
-let p12 () =
-  {}
-  try
+let p12 () ensures { result = 2 }
+= try
     begin raise E; raise (F 1); 1 end
   with E -> 2
      | F x -> 3
   end
-  { result = 2 }
 
-let p13 () =
-  {}
-  try
+let p13 () ensures { !x = 2 }
+= try
     begin raise E; raise (F 1); x := 1 end
   with E -> x := 2
      | F _ -> x := 3
   end
-  { !x = 2 }
 
-let p13a () =
-  {}
-  try
+let p13a () ensures { !x <> 1 }
+= try
     (if !x = 1 then raise E)
     (*{ true | E => x = 1 }*)
   with E ->
     x := 0
   end
-  { !x <> 1 }
 
 exception E1
 exception E2
 exception E3
 
-let p14 () =
-  {}
-  begin
+let p14 () ensures { false } raises {
+  | E1 -> !x = 1 | E2 -> !x = 2 | E3 -> !x = 3
+  | E -> !x <> 1 /\ !x <> 2 /\ !x <> 3 }
+= begin
     if !x = 1 then raise E1;
     if !x = 2 then raise E2;
     if !x = 3 then raise E3;
     raise E : unit
   end
-  { false } | E1 -> {  !x = 1 } | E2 -> {  !x = 2 } | E3 -> { !x = 3 }
-  | E -> { !x <> 1 /\ !x <> 2 /\ !x <> 3 }
 
-let p15 () =
-  {}
-  if !x = 0 then raise E else (x := 0; raise (F !x)) : unit
-  { false } | E -> { !x=0 } | F -> { result=0 }
+let p15 () ensures { false } raises { E -> !x=0 | F result -> result=0 }
+= if !x = 0 then raise E else (x := 0; raise (F !x)) : unit
 
-let p16 () = {} if !x = 0 then (x:=1; raise E) { !x<>0 } | E -> { !x=1 }
+let p16 () ensures { !x<>0 } raises { E -> !x=1 }
+  = if !x = 0 then (x:=1; raise E)
 
-let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { !x=0 }
+let p17 () ensures { false } raises { E -> !x=0 }
+  = (x := 0; (raise E; x := 1))
 
 end
 

bench/programs/good/for.mlw

 module M
 
 use import int.Int
-use import module ref.Ref
+use import ref.Ref
 
 (* for loop with invariant *)
 let test1 () =
@@ -24,17 +24,16 @@ exception E
 
 (* the body raises an exception (for sure)
    subtle: the invariant is required *)
-let test3 () =
-  { }
-  for i = 1 to 10 do invariant { i >= 2 -> false }
+let test3 ()
+  ensures { false } raises { E -> true }
+= for i = 1 to 10 do invariant { i >= 2 -> false }
     raise E
   done
-  { false } | E -> { true }
 
 (* the body may raise an exception *)
-let test4 x =
-  { }
-  try
+let test4 x
+  ensures { result=True <-> 0 <= x <= 10 }
+= try
     for i = 0 to 10 do
       invariant { x < 0 \/ x >= i }