diff --git a/bench/programs/bad-typing/alias1.mlw b/bench/programs/bad-typing/alias1.mlw
index 8136381f6e9869c9320f75d2154e9b7c9222a285..64773150be040e70318c0f4bbdb1b34f7721a227 100644
--- a/bench/programs/bad-typing/alias1.mlw
+++ b/bench/programs/bad-typing/alias1.mlw
@@ -6,7 +6,7 @@ module M
x := 1;
y := 2
- parameter r : ref int
+ val r : ref int
let test () =
foo r r
diff --git a/bench/programs/bad-typing/effect1.mlw b/bench/programs/bad-typing/effect1.mlw
index 4f4eba3fa35f68c133334301e07f1d2fdaf78f52..1b7fa21c3241a274d7b6baaaf748414f8334b4eb 100644
--- a/bench/programs/bad-typing/effect1.mlw
+++ b/bench/programs/bad-typing/effect1.mlw
@@ -3,6 +3,6 @@ module M
use import module ref.Ref
- parameter f : x:int -> {} unit writes a.contents {}
+ val f : x:int -> {} unit writes a.contents {}
end
diff --git a/bench/programs/bad-typing/effect2.mlw b/bench/programs/bad-typing/effect2.mlw
index 908da447efb23ab6f451c02297a9e6b093b44a23..b06c55e6f5d80263309c91503d09a56722a50753 100644
--- a/bench/programs/bad-typing/effect2.mlw
+++ b/bench/programs/bad-typing/effect2.mlw
@@ -3,6 +3,6 @@ module M
use import module ref.Ref
- parameter f : x:int -> {} unit writes x.contents {}
+ val f : x:int -> {} unit writes x.contents {}
end
diff --git a/bench/programs/bad-typing/effect3.mlw b/bench/programs/bad-typing/effect3.mlw
index 79a4b873a886877024db2870b30e43f773f1fe4f..68299b0d3f42986beeff123b799b89b0036eef32 100644
--- a/bench/programs/bad-typing/effect3.mlw
+++ b/bench/programs/bad-typing/effect3.mlw
@@ -3,8 +3,8 @@ module M
use import module ref.Ref
- parameter a : int
+ val a : int
- parameter f : x:int -> {} unit writes a.contents {}
+ val f : x:int -> {} unit writes a.contents {}
end
diff --git a/bench/programs/bad-typing/effect4.mlw b/bench/programs/bad-typing/effect4.mlw
index c95456e24ba3fdd7ee453e7d7c210d3158065944..7321f31e9d34ebae82226a3a82429b93912fe40b 100644
--- a/bench/programs/bad-typing/effect4.mlw
+++ b/bench/programs/bad-typing/effect4.mlw
@@ -3,8 +3,8 @@ module M
use import module ref.Ref
- parameter foo : int -> int
+ val foo : int -> int
- parameter f : x:int -> {} unit writes foo.contents {}
+ val f : x:int -> {} unit writes foo.contents {}
end
diff --git a/bench/programs/bad-typing/effect5.mlw b/bench/programs/bad-typing/effect5.mlw
index fd5323f5314c492c6d991b21398a5a43a8eb79d5..704701892250c7d54a10701dd079b9a883d1cf3d 100644
--- a/bench/programs/bad-typing/effect5.mlw
+++ b/bench/programs/bad-typing/effect5.mlw
@@ -1,6 +1,6 @@
module M
- parameter f : x:int -> {} unit writes 1 {}
+ val f : x:int -> {} unit writes 1 {}
end
diff --git a/bench/programs/bad-typing/effect6.mlw b/bench/programs/bad-typing/effect6.mlw
index 41e4d8cf3f04417e6f7c9f0a520039b01b98ce65..21322f83f6d12da900fd0275825a76e71f800a5e 100644
--- a/bench/programs/bad-typing/effect6.mlw
+++ b/bench/programs/bad-typing/effect6.mlw
@@ -1,6 +1,6 @@
module M
- parameter f : x:int -> {} unit writes x {}
+ val f : x:int -> {} unit writes x {}
end
diff --git a/bench/programs/bad-typing/effect7.mlw b/bench/programs/bad-typing/effect7.mlw
index bdd1a6a7e3eaf9bb72a957d4c0acbb0306da8ee2..3c978c74268b705cfd00c31ba2ac663fd40674df 100644
--- a/bench/programs/bad-typing/effect7.mlw
+++ b/bench/programs/bad-typing/effect7.mlw
@@ -3,6 +3,6 @@ module M
type t = {| mutable a : int; mutable b : int |}
- parameter f : x:t -> {} unit writes x {}
+ val f : x:t -> {} unit writes x {}
end
diff --git a/bench/programs/bad-typing/polyref1.mlw b/bench/programs/bad-typing/polyref1.mlw
index 9161c98b7e8ebd9882002e907cb50644d1f45408..c495e946abfd073495531a3382058ae47647c02f 100644
--- a/bench/programs/bad-typing/polyref1.mlw
+++ b/bench/programs/bad-typing/polyref1.mlw
@@ -2,6 +2,6 @@ module M
use import module stdlib.Ref
- parameter r : ref 'a
+ val r : ref 'a
end
diff --git a/bench/programs/bad-typing/polyref3.mlw b/bench/programs/bad-typing/polyref3.mlw
index d9b97ff4bc90f25ce6b83b8367847d18590f95d8..eaf576c33cfd0e73d814f5355d3de8bed9ec0abc 100644
--- a/bench/programs/bad-typing/polyref3.mlw
+++ b/bench/programs/bad-typing/polyref3.mlw
@@ -3,6 +3,6 @@ module M
use import module stdlib.Ref
use import list.List
- parameter r : ref (list 'a)
+ val r : ref (list 'a)
end
diff --git a/bench/programs/good/booleans.mlw b/bench/programs/good/booleans.mlw
index 07fff6c7a39314b3e2511d878098678933f6debc..84f0c0d42e476e376de9b7b339fa7600672d74c3 100644
--- a/bench/programs/good/booleans.mlw
+++ b/bench/programs/good/booleans.mlw
@@ -3,13 +3,13 @@ module M
use import int.Int
use import module ref.Ref
-parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
+val incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
-parameter x : ref int
+val x : ref int
-parameter id_not_0 : x:int -> { x <> 0 } int { result = x }
+val id_not_0 : x:int -> { x <> 0 } int { result = x }
-parameter id : x:int -> { } int { result = x }
+val id : x:int -> { } int { result = x }
let test_and_1 () =
{ }
@@ -50,10 +50,10 @@ let test_all_1 () =
function d : int
-parameter vx : ref int
-parameter vy : ref int
+val vx : ref int
+val vy : ref int
-parameter sq : x:int -> {} int { result = x*x }
+val sq : x:int -> {} int { result = x*x }
let test_cd3d () =
{ true }
diff --git a/bench/programs/good/complex_arg_1.mlw b/bench/programs/good/complex_arg_1.mlw
index 51187b9a8de617c89dbc2fe5a96c25ca00338e4f..0fa244ff4dc7322b131a3156411d1a9a8d609947 100644
--- a/bench/programs/good/complex_arg_1.mlw
+++ b/bench/programs/good/complex_arg_1.mlw
@@ -2,12 +2,12 @@ module M
exception Exception
-parameter f0 : tt:unit ->
+val f0 : tt:unit ->
{ }
unit
{ true }
-parameter f1 : tt:unit ->
+val f1 : tt:unit ->
{ }
unit
raises Exception
diff --git a/bench/programs/good/complex_arg_2.mlw b/bench/programs/good/complex_arg_2.mlw
index bd5bf883b01633fd3f6872d8dc52d71796965a2b..902c443f9165ca3f3042c1460650a3606eca8389 100644
--- a/bench/programs/good/complex_arg_2.mlw
+++ b/bench/programs/good/complex_arg_2.mlw
@@ -4,9 +4,9 @@ exception Exception int
use import module ref.Ref
-parameter t : ref int
+val t : ref int
-parameter m : a:int -> b:int ->
+val m : a:int -> b:int ->
{ }
unit reads t raises Exception
{ true } | Exception -> { true }
diff --git a/bench/programs/good/exns.mlw b/bench/programs/good/exns.mlw
index 3bc36a905eaabe858e8bba1e60c878c844215204..20106b446a329972d98d50382f0876b105d0e666 100644
--- a/bench/programs/good/exns.mlw
+++ b/bench/programs/good/exns.mlw
@@ -45,7 +45,7 @@ let p6 () =
use import module ref.Ref
-parameter x : ref int
+val x : ref int
let p7 () =
{} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
diff --git a/bench/programs/good/loops.mlw b/bench/programs/good/loops.mlw
index 2c4d5d43c6b9e4cd4e63a82258fcec35dfa25981..dc04ab7b67bd0f3546add73a7b9f61b32981f6be 100644
--- a/bench/programs/good/loops.mlw
+++ b/bench/programs/good/loops.mlw
@@ -5,7 +5,7 @@ use import module ref.Ref
(** 1. A loop increasing [i] up to 10. *)
-parameter i : ref int
+val i : ref int
let loop1 (u:unit) =
{ !i <= 10 }
@@ -18,7 +18,7 @@ let loop1 (u:unit) =
(** 2. The same loop, followed by a function call. *)
-parameter x: ref int
+val x: ref int
let negate (u:unit) = {} x := - !x { !x = - (old !x) }
diff --git a/bench/programs/good/oldify.mlw b/bench/programs/good/oldify.mlw
index 350e035aa04c95e4a11ddceb2564d66b10b86145..6098239f02df54795e4299d2ca465e7ab10f17db 100644
--- a/bench/programs/good/oldify.mlw
+++ b/bench/programs/good/oldify.mlw
@@ -4,9 +4,9 @@ module M
predicate q1 int int int
- parameter r : ref int
+ val r : ref int
- parameter f1 : y:int ->
+ val f1 : y:int ->
{} unit writes r { q1 !r (old !r) y }
let g1 () = {} f1 !r { q1 !r (old !r) (old !r) }
@@ -14,7 +14,7 @@ module M
function foo int : int
predicate q int int int
- parameter f : t:ref int -> x:int ->
+ val f : t:ref int -> x:int ->
{} unit writes t { q !t (old !t) x }
let g (t:ref int) =
diff --git a/bench/programs/good/po.mlw b/bench/programs/good/po.mlw
index b4b245746773d216b0c01177965740bfdb5574fc..671a779a58b5cfd7e363075232048d7ec0861c05 100644
--- a/bench/programs/good/po.mlw
+++ b/bench/programs/good/po.mlw
@@ -5,7 +5,7 @@ use import module ref.Ref
(* Tests for proof obligations. *)
-parameter x : ref int
+val x : ref int
predicate q int
@@ -39,7 +39,7 @@ let p9a () = {} begin x := 1; 1 end + 1 { result = 2 /\ !x = 1 }
(* function with a post-condition *)
-parameter fsucc : x:int -> { } int { result = x + 1 }
+val fsucc : x:int -> { } int { result = x + 1 }
let p10 () = {} fsucc 0 { result = 1 }
@@ -49,7 +49,7 @@ 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 }
+val incrx : unit -> { } unit writes x { !x = (old !x) + 1 }
let p12 () = { !x = 0 } incrx () { !x = 1 }
@@ -59,7 +59,7 @@ 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 /\ result = !x }
+val incrx2 : unit -> { } int writes x { !x = old !x + 1 /\ result = !x }
let p14 () = { !x = 0 } incrx2 () { result = 1 }
diff --git a/bench/programs/good/recfun.mlw b/bench/programs/good/recfun.mlw
index 1966a47fab61582a5a7d51db75c8d5c53514b2fb..a8ce273d31a7f219f34bdf838038b3e987f17402 100644
--- a/bench/programs/good/recfun.mlw
+++ b/bench/programs/good/recfun.mlw
@@ -12,7 +12,7 @@ module M
(** 2. With effects but no argument *)
- parameter x : ref int
+ val 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 }
diff --git a/bench/programs/good/scopes.mlw b/bench/programs/good/scopes.mlw
index 63551a86129dd9cdc7db969c4ddf48ba57490e06..3775706e54c06ce3b01381d6e4a60521fbf42220 100644
--- a/bench/programs/good/scopes.mlw
+++ b/bench/programs/good/scopes.mlw
@@ -11,7 +11,7 @@ module LocalFunctions
f 2;
assert { !x = 2 }
- parameter r: ref int
+ val r: ref int
(* recursive function accessing a global reference *)
let rec test2 () =
diff --git a/bench/programs/good/see.mlw b/bench/programs/good/see.mlw
index 58f16ce7567a203b88e34ae5921019869e90d2bd..93859216d9f403f8ff3d32b5fda3abb2bc4e3520 100644
--- a/bench/programs/good/see.mlw
+++ b/bench/programs/good/see.mlw
@@ -5,9 +5,9 @@ use import module ref.Ref
(* Side effect in expressions (Bart Jacobs' tricky example) *)
-parameter b : ref int
-parameter b1 : ref int
-parameter b2 : ref int
+val b : ref int
+val b1 : ref int
+val b2 : ref int
let f () =
{} b := 1 - !b; !b { result = !b /\ !b = 1 - old !b }
diff --git a/bench/programs/good/set.mlw b/bench/programs/good/set.mlw
index aa6ecdebd274f8071af647192f8e299af27351d0..9c0c21f2ded726aa975a44d3d8e3a9d07d75b06c 100644
--- a/bench/programs/good/set.mlw
+++ b/bench/programs/good/set.mlw
@@ -5,9 +5,9 @@ module M
(* side effects in tests *)
- parameter x : ref int
+ val x : ref int
- parameter set_and_test_zero :
+ val set_and_test_zero :
v:int ->
{}
bool writes x
@@ -15,7 +15,7 @@ module M
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
- parameter set_and_test_nzero :
+ val set_and_test_nzero :
v:int ->
{}
bool writes x
diff --git a/bench/programs/good/wpcalls.mlw b/bench/programs/good/wpcalls.mlw
index aa34d21b95ebef7a3d8b9aa806fedffe69bd72b6..e9bc03f88e73bfe02f0e00173e8059cdb559caf2 100644
--- a/bench/programs/good/wpcalls.mlw
+++ b/bench/programs/good/wpcalls.mlw
@@ -3,9 +3,9 @@ module M
use import int.Int
use import module ref.Ref
-parameter x : ref int
+val x : ref int
-parameter f : unit -> { } unit writes x { !x = 1 - old !x }
+val f : unit -> { } unit writes x { !x = 1 - old !x }
let p () =
begin
diff --git a/doc/module.bnf b/doc/module.bnf
index d87de4d070b284c5333a107861149f49830c0f7a..e2debd5e3c9209d1a38a8ef4eb4844cfe88e00db 100644
--- a/doc/module.bnf
+++ b/doc/module.bnf
@@ -5,7 +5,7 @@
| "type" mtype-decl ("with" mtype-decl)* ; mutable types
| "let" lident label* pgm-defn ;
| "let" "rec" recfun ("with" recfun)* ;
- | "parameter" lident label* pgm-decl ;
+ | "val" lident label* pgm-decl ;
| "exception" lident label* type? ;
| "use" imp-exp "module" tqualid ("as" uident-opt)? ;
| "namespace" "import"? uident-opt mdecl* "end" ;
diff --git a/examples/programs/algo63.mlw b/examples/programs/algo63.mlw
index 86b25a8a58f37c49e0066d780174a70777a4f51e..e5da6759bfaf07f705a7adfa877ad3953ea4c908 100644
--- a/examples/programs/algo63.mlw
+++ b/examples/programs/algo63.mlw
@@ -19,7 +19,7 @@ module Algo63
use import module array.Array
use import module array.ArrayPermut
- parameter partition :
+ val partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ m < n }
unit writes a i j
diff --git a/examples/programs/algo64.mlw b/examples/programs/algo64.mlw
index 13948db6878c734503a7e552aef421e36acba0c7..22bb27fbfdc16cd3f98075d08b15162e1e5a7816 100644
--- a/examples/programs/algo64.mlw
+++ b/examples/programs/algo64.mlw
@@ -27,7 +27,7 @@ module Algo64
(* Algorithm 63 *)
- parameter partition :
+ val partition :
a:array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
diff --git a/examples/programs/algo65.mlw b/examples/programs/algo65.mlw
index 20b7c99c14f89c418c1b1185c552612113ccec4e..3b97791a879ebe71e3ca98feab0e39f121ecebbd 100644
--- a/examples/programs/algo65.mlw
+++ b/examples/programs/algo65.mlw
@@ -21,7 +21,7 @@ module Algo65
(* algorithm 63 *)
- parameter partition :
+ val partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
diff --git a/examples/programs/arm.mlw b/examples/programs/arm.mlw
index 152897a3a2a553ec21ad21af1ab2bfa2cda43493..13a5c94ad28b5440c3a27aaa8f337dad7986d5d7 100644
--- a/examples/programs/arm.mlw
+++ b/examples/programs/arm.mlw
@@ -6,13 +6,13 @@ module M
use import module ref.Refint
use import module array.Array
- parameter a : array int
+ val a : array int
predicate inv (a : array int) =
a[0] = 0 /\ length a = 11 /\ forall k:int. 1 <= k <= 10 -> 0 < a[k]
- parameter loop1 : ref int
- parameter loop2 : ref int
+ val loop1 : ref int
+ val loop2 : ref int
let insertion_sort () =
{ inv a /\
@@ -47,37 +47,37 @@ module ARM
use export module ref.Ref
(* memory *)
- parameter mem : ref (map int int)
- parameter mem_ldr : a:int -> {} int reads mem.contents { result = !mem[a] }
- parameter mem_str : a:int -> v:int ->
+ val mem : ref (map int int)
+ val mem_ldr : a:int -> {} int reads mem.contents { result = !mem[a] }
+ val mem_str : a:int -> v:int ->
{} int writes mem.contents { !mem = (old !mem)[a <- v] }
(* data segment *)
(*
- parameter data : ref (t int int)
- parameter data_ldr : a:int -> {} int reads data { result = data[a] }
- parameter data_str :
+ val data : ref (t int int)
+ val data_ldr : a:int -> {} int reads data { result = data[a] }
+ val data_str :
a:int -> v:int -> {} int writes data { data = (old data)[a <- v] }
*)
(* registers *)
- parameter r0 : ref int
- parameter r1 : ref int
- parameter r2 : ref int
- parameter r3 : ref int
+ val r0 : ref int
+ val r1 : ref int
+ val r2 : ref int
+ val r3 : ref int
(* ... *)
- parameter fp : ref int
- parameter pc : ref int (* pc *)
+ val fp : ref int
+ val pc : ref int (* pc *)
- parameter ldr :
+ val ldr :
r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { !r = !mem[a] }
- parameter str :
+ val str :
r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { !mem = (old !mem)[a <- !r] }
(* condition flags *)
- parameter le : ref bool
+ val le : ref bool
- parameter cmp : r:ref int -> v:int ->
+ val cmp : r:ref int -> v:int ->
{}
unit reads r.contents writes le.contents
{ !le=True <-> !r <= v }
@@ -106,8 +106,8 @@ module InsertionSortExample
j = fp-20
temp = fp-24 *)
- parameter l4 : ref int
- parameter l7 : ref int
+ val l4 : ref int
+ val l7 : ref int
function a : int
diff --git a/examples/programs/binary_search_c.mlw b/examples/programs/binary_search_c.mlw
index e6e34922b4dd1e8adad182af4e26d6ae38e99742..f6e6403771672da90f734fe0d367e6e02d23ab10 100644
--- a/examples/programs/binary_search_c.mlw
+++ b/examples/programs/binary_search_c.mlw
@@ -27,7 +27,7 @@ module M1
type memory
function get memory pointer int : int
- parameter mem : ref memory
+ val mem : ref memory
exception Return int
@@ -73,11 +73,11 @@ module M2
type memory
function get memory pointer int : int
- parameter mem : ref memory
+ val mem : ref memory
function block_size memory pointer : int
- parameter get_ :p : pointer -> ofs : int ->
+ val get_ :p : pointer -> ofs : int ->
{ 0 <= ofs < block_size !mem p }
int reads mem
{ result = get !mem p ofs }
@@ -122,18 +122,18 @@ module M3
axiom int32_domain : forall x:int32. -2147483648 <= to_int x <= 2147483647
- parameter of_int :
+ val of_int :
x:int -> { -2147483648 <= x <= 2147483647 } int32 { to_int result = x }
type pointer
type memory
function get memory pointer int : int32
- parameter mem : ref memory
+ val mem : ref memory
function block_size memory pointer : int
- parameter get_ : p:pointer -> ofs:int32 ->
+ val get_ : p:pointer -> ofs:int32 ->
{ 0 <= to_int ofs < block_size !mem p }
int32 reads mem
{ result = get !mem p (to_int ofs) }
diff --git a/examples/programs/course.mlw b/examples/programs/course.mlw
index 3a1d16f5c129f376349b23d09402c393856e73a1..f7dff09e395635e8f818cff8a16bcf457d267708 100644
--- a/examples/programs/course.mlw
+++ b/examples/programs/course.mlw
@@ -28,9 +28,9 @@ module M
predicate valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
forall i:int. n <= i <= m -> valid a (r[i])
-parameter alloc : ref first_free_addr
+val alloc : ref first_free_addr
-parameter new_pointer : tt:unit ->
+val new_pointer : tt:unit ->
{ }
pointer
writes alloc
diff --git a/examples/programs/dijkstra.mlw b/examples/programs/dijkstra.mlw
index cba2323d944e27cb488de685013df38698b9f9c9..f956cbfeff1b61f1b5443d14671c53d3c20489c1 100644
--- a/examples/programs/dijkstra.mlw
+++ b/examples/programs/dijkstra.mlw
@@ -9,13 +9,13 @@ module M
(* iteration on a set *)
- parameter set_has_next :
+ val set_has_next :
s:ref (S.set 'a) ->
{}
bool reads s
{ if result=True then S.is_empty !s else not S.is_empty !s }
- parameter set_next :
+ val set_next :
s:ref (S.set 'a) ->
{ not S.is_empty !s }
'a writes s
@@ -36,31 +36,31 @@ module M
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
- parameter eq_vertex :
+ val eq_vertex :
x:vertex -> y:vertex -> {} bool { if result=True then x=y else x<>y }
(* visited vertices *)
- parameter visited : ref (S.set vertex)
+ val visited : ref (S.set vertex)
- parameter visited_add :
+ val visited_add :
x:vertex -> {} unit writes visited { !visited = S.add x (old !visited) }
(* current distances *)
- parameter d : ref (M.map vertex int)
+ val d : ref (M.map vertex int)
(* priority queue *)
- parameter q : ref (S.set vertex)
+ val q : ref (S.set vertex)
- parameter q_is_empty :
+ val q_is_empty :
unit ->
{}
bool reads q
{ if result=True then S.is_empty !q else not S.is_empty !q }
- parameter init :
+ val init :
src:vertex ->
{}
unit writes visited q d
@@ -93,7 +93,7 @@ module M
S.mem m q /\
forall x:vertex. S.mem x q -> d[m] <= d[x]
- parameter q_extract_min :
+ val q_extract_min :
unit ->
{ not S.is_empty !q }
vertex reads d writes q
diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw
index 6ff15854f9b84d5d9c57ba687fddd8b8c151f935..34049ea053a868068e024513a98aba7e38ab13eb 100644
--- a/examples/programs/distance.mlw
+++ b/examples/programs/distance.mlw
@@ -30,18 +30,18 @@ module Distance
type word = list a
- parameter w1 : array a
- parameter w2 : array a
+ val w1 : array a
+ val w2 : array a
(* Global variables of the program. The program uses an auxiliary
array [t] of integers of size [n2+1] and three auxiliary
integer variables [i], [j] and [old]. *)
- parameter t : array int
+ val t : array int
- parameter i : ref int
- parameter j : ref int
- parameter o : ref int
+ val i : ref int
+ val j : ref int
+ val o : ref int
(* Auxiliary definitions for the program and its specification. *)
diff --git a/examples/programs/fib_memo.mlw b/examples/programs/fib_memo.mlw
index bf4a227ca99142856db0a3584d4e9de6c5f96607..c5dd8e6ad36c1173449f331b87d8ae4b1896e10f 100644
--- a/examples/programs/fib_memo.mlw
+++ b/examples/programs/fib_memo.mlw
@@ -19,15 +19,15 @@ module M
predicate inv (t : table) =
forall x y : int. t[x] = Some y -> y = fib x
- parameter table : ref table
+ val table : ref table
- parameter add :
+ val add :
x:int -> y:int ->
{} unit writes table { !table = (old !table)[x <- Some y] }
exception Not_found
- parameter find :
+ val find :
x:int ->
{}
int reads table raises Not_found
diff --git a/examples/programs/list_rev.mlw b/examples/programs/list_rev.mlw
index 675d2b03c5455d7b5b5ed17ddbc1c702b55657dd..7509638537509cf20a71e27b7f7b554fc6885a72 100644
--- a/examples/programs/list_rev.mlw
+++ b/examples/programs/list_rev.mlw
@@ -10,8 +10,8 @@ module M
type next = map pointer pointer
function null : pointer
- parameter value : ref (map pointer int)
- parameter next : ref (next)
+ val value : ref (map pointer int)
+ val next : ref (next)
inductive is_list (next : next) (p : pointer) =
| is_list_null:
@@ -193,8 +193,8 @@ module M2
type next = map pointer pointer
function null : pointer
- parameter value : ref (map pointer int)
- parameter next : ref (next)
+ val value : ref (map pointer int)
+ val next : ref (next)
inductive is_list (next : next) (p : pointer) =
| is_list_null:
diff --git a/examples/programs/my_cosine.mlw b/examples/programs/my_cosine.mlw
index a7a5a32ac80a1c8d1e7b80003c89a46fbdb32fdb..3175c0a822a671a26b125007128a12134309018d 100644
--- a/examples/programs/my_cosine.mlw
+++ b/examples/programs/my_cosine.mlw
@@ -6,22 +6,22 @@ module M
use import floating_point.Rounding
use import floating_point.Single
-parameter single_of_real_exact : x:real ->
+val single_of_real_exact : x:real ->
{ }
single
{ value result = x }
-parameter add : x:single -> y:single ->
+val add : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) +. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) +. (value y))}
-parameter sub : x:single -> y:single ->
+val sub : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) -. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) -. (value y))}
-parameter mul : x:single -> y:single ->
+val mul : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) *. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) *. (value y))}
diff --git a/examples/programs/next_digit_sum.mlw b/examples/programs/next_digit_sum.mlw
index 01c60668f2249fae4adf57bdeb89c97fe8a30cc1..65d4cab7d81cb115fa375ace457347e4b6ee4566 100644
--- a/examples/programs/next_digit_sum.mlw
+++ b/examples/programs/next_digit_sum.mlw
@@ -62,7 +62,7 @@ module M
forall x : M.map int int, i j : int.
i < j -> interp9 (M.set x i 9) i j = interp9 x (i+1) j
- parameter x : array int
+ val x : array int
(* the number of digits of X *)
function n : int
diff --git a/examples/programs/relabel.mlw b/examples/programs/relabel.mlw
index c45a72d5cfdbb42bae96e5430c7d8c0e06183e00..b0a18f748b150a6f5a87917d5c08377fab825615 100644
--- a/examples/programs/relabel.mlw
+++ b/examples/programs/relabel.mlw
@@ -39,7 +39,7 @@ module Relabel
use import int.Int
use import module ref.Ref
- parameter r : ref int
+ val r : ref int
let fresh () =
{} r := !r + 1; !r { !r = old !r + 1 /\ result = !r }
diff --git a/examples/programs/sf.mlw b/examples/programs/sf.mlw
index 6b27d42ba514504280825729af0ea441903f9115..1305283fc43fdbd61b9ca4857835f700cd87cd51 100644
--- a/examples/programs/sf.mlw
+++ b/examples/programs/sf.mlw
@@ -106,8 +106,8 @@ module MoreHoareLogic
| Cons x r -> x + sum r
end
- parameter head : l:list 'a -> { l<>Nil } 'a { Some result = hd l }
- parameter tail : l:list 'a -> { l<>Nil } list 'a { Some result = tl l }
+ val head : l:list 'a -> { l<>Nil } 'a { Some result = hd l }
+ val tail : l:list 'a -> { l<>Nil } list 'a { Some result = tl l }
let list_sum (l: ref (list int)) (y: ref int) =
{}
diff --git a/examples/programs/vacid_0_build_maze.mlw b/examples/programs/vacid_0_build_maze.mlw
index 36beb9de72c2c5a36da50488436037977c1f9bfd..191b6c9c5756ec0a30b9d26de6dde2296d4095a0 100644
--- a/examples/programs/vacid_0_build_maze.mlw
+++ b/examples/programs/vacid_0_build_maze.mlw
@@ -35,14 +35,14 @@ module UnionFind_sig
use export UnionFind
- parameter create :
+ val create :
n:int ->
{ 0 <= n }
ref uf
{ num !result = n /\ size !result = n /\
forall x:int. 0 <= x < n -> repr !result x x }
- parameter find :
+ val find :
u:ref uf -> x:int ->
{ 0 <= x < size !u }
int writes u
@@ -50,7 +50,7 @@ module UnionFind_sig
size !u = size (old !u) /\ num !u = num (old !u) /\
same_reprs !u (old !u) }
- parameter union :
+ val union :
u:ref uf -> a:int -> b:int ->
{ 0 <= a < size !u /\ 0 <= b < size !u /\ not same !u a b }
unit writes u
@@ -62,7 +62,7 @@ module UnionFind_sig
same (old !u) x a /\ same (old !u) b y \/
same (old !u) x b /\ same (old !u) a y }
- parameter get_num_classes :
+ val get_num_classes :
u:ref uf -> {} int reads u { result = num !u }
end
@@ -95,11 +95,11 @@ module Graph_sig
(* clone export Graph with type vertex = int *)
use export Graph_int
- parameter graph : ref graph
+ val graph : ref graph
- parameter num_edges : ref int
+ val num_edges : ref int
- parameter add_edge : a:int -> b:int ->
+ val add_edge : a:int -> b:int ->
{ not path !graph a b }
unit writes num_edges graph
{ !num_edges = old !num_edges + 1 /\
@@ -120,7 +120,7 @@ module BuildMaze
use import module UnionFind_sig
use import module Graph_sig
- parameter rand : s:int -> { 0 < s } int { 0 <= result < s }
+ val rand : s:int -> { 0 < s } int { 0 <= result < s }
lemma Ineq1 :
forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
diff --git a/examples/programs/vacid_0_red_black_trees_harness.mlw b/examples/programs/vacid_0_red_black_trees_harness.mlw
index b8f666880b77b781ea3be43665076adbd0173194..74af6d1e4c3854f31aa9584b94eaf7a02ae5a640 100644
--- a/examples/programs/vacid_0_red_black_trees_harness.mlw
+++ b/examples/programs/vacid_0_red_black_trees_harness.mlw
@@ -8,14 +8,14 @@ module M
function default rbt : value
predicate mem rbt key value
- parameter create :
+ val create :
d:value ->
{}
ref rbt
{ default !result = d /\
forall k:key, v:value. mem !result k v <-> v = d }
- parameter replace :
+ val replace :
m:ref rbt -> k:key -> v:value ->
{}
unit writes m
@@ -23,13 +23,13 @@ module M
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
- parameter lookup :
+ val lookup :
m:ref rbt -> k:key ->
{}
value reads m
{ mem !m k result }
- parameter remove :
+ val remove :
m:ref rbt -> k:key ->
{}
unit writes m
diff --git a/examples/programs/vacid_0_sparse_array.mlw b/examples/programs/vacid_0_sparse_array.mlw
index 290c1b2d950cf662e8317824e3eb0d2aca6b76a6..13ae3d4bb6ff93b0ae620d92183913201bf4aa2e 100644
--- a/examples/programs/vacid_0_sparse_array.mlw
+++ b/examples/programs/vacid_0_sparse_array.mlw
@@ -4,80 +4,80 @@ module SparseArray
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| |
- +-----+-+---+-+----+-+----+
+ b a c
+values +-----+-+---+-+----+-+----+
+ | |y| |x| |z| |
+ +-----+-+---+-+----+-+----+
-idx +-----+-+---+-+----+-+----+
- | |1| |0| |2| |
- +-----+-+---+-+----+-+----+
+index +-----+-+---+-+----+-+----+
+ | |1| |0| |2| |
+ +-----+-+---+-+----+-+----+
- 0 1 2 n=3
-back +-+-+-+-------------------+
- |a|b|c| |
- +-+-+-+-------------------+
+ 0 1 2 n=3
+back +-+-+-+-------------------+
+ |a|b|c| |
+ +-+-+-+-------------------+
*)
use import int.Int
use import module array.Array as A
- type sparse_array 'a = {| val : array 'a;
- idx : array int;
- back : array int;
- mutable card : int;
- default : 'a; |}
+ type sparse_array 'a = {| values : array 'a;
+ index : array int;
+ back : array int;
+ mutable card : int;
+ def : 'a; |}
predicate is_elt (a: sparse_array 'a) (i: int) =
- 0 <= a.idx[i] < a.card /\ a.back[a.idx[i]] = i
+ 0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i
function value (a: sparse_array 'a) (i: int) : 'a =
if is_elt a i then
- a.val[i]
+ a.values[i]
else
- a.default
+ a.def
(* invariant *)
function maxlen : int = 1000
- function length (a: sparse_array 'a) : int = A.length a.val
+ function length (a: sparse_array 'a) : int = A.length a.values
predicate sa_inv (a: sparse_array 'a) =
0 <= a.card <= length a <= maxlen /\
- A.length a.val = A.length a.idx = A.length a.back /\
+ A.length a.values = A.length a.index = A.length a.back /\
forall i : int.
0 <= i < a.card ->
- 0 <= a.back[i] < length a /\ a.idx[a.back[i]] = i
+ 0 <= a.back[i] < length a /\ a.index[a.back[i]] = i
(* creation *)
- parameter malloc : n:int -> {} array 'a { A.length result = n }
+ val malloc : n:int -> {} array 'a { A.length result = n }
let create (sz: int) (d: 'a) =
{ 0 <= sz <= maxlen }
- {| val = malloc sz;
- idx = malloc sz;
- back = malloc sz;
- card = 0;
- default = d |}
- { sa_inv result /\ result.card = 0 /\
- result.default = d /\ length result = sz }
+ {| values = malloc sz;
+ index = malloc sz;
+ back = malloc sz;
+ card = 0;
+ def = d |}
+ { sa_inv result /\ result.card = 0 /\
+ result.def = d /\ length result = sz }
(* access *)
let test (a: sparse_array 'a) i =
{ 0 <= i < length a /\ sa_inv a }
- 0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i
+ 0 <= a.index[i] && a.index[i] < a.card && a.back[a.index[i]] = i
{ result=True <-> is_elt a i }
let get (a: sparse_array 'a) i =
{ 0 <= i < length a /\ sa_inv a }
if test a i then
- a.val[i]
+ a.values[i]
else
- a.default
+ a.def
{ result = value a i }
(* assignment *)
@@ -89,10 +89,10 @@ back +-+-+-+-------------------+
let set (a: sparse_array 'a) i v =
{ 0 <= i < length a /\ sa_inv a }
- a.val[i] <- v;
+ a.values[i] <- v;
if not (test a i) then begin
assert { a.card < length a };
- a.idx[i] <- a.card;
+ a.index[i] <- a.card;
a.back[a.card] <- i;
a.card <- a.card + 1
end
@@ -107,24 +107,24 @@ module Harness
use import module SparseArray
type elt
- function default : elt
+ function def : elt
function c1 : elt
function c2 : elt
let harness () =
- let a = create 10 default in
- let b = create 20 default in
- let get_a_5 = get a 5 in assert { get_a_5 = default };
- let get_b_7 = get b 7 in assert { get_b_7 = default };
+ let a = create 10 def in
+ let b = create 20 def in
+ let get_a_5 = get a 5 in assert { get_a_5 = def };
+ let get_b_7 = get b 7 in assert { get_b_7 = def };
set a 5 c1;
set b 7 c2;
let get_a_5 = get a 5 in assert { get_a_5 = c1 };
let get_b_7 = get b 7 in assert { get_b_7 = c2 };
- let get_a_7 = get a 7 in assert { get_a_7 = default };
- let get_b_5 = get b 5 in assert { get_b_5 = default };
- let get_a_0 = get a 0 in assert { get_a_0 = default };
- let get_b_0 = get b 0 in assert { get_b_0 = default };
+ let get_a_7 = get a 7 in assert { get_a_7 = def };
+ let get_b_5 = get b 5 in assert { get_b_5 = def };
+ let get_a_0 = get a 0 in assert { get_a_0 = def };
+ let get_b_0 = get b 0 in assert { get_b_0 = def };
()
end
diff --git a/examples/programs/vacid_0_union_find.mlw b/examples/programs/vacid_0_union_find.mlw
index 8401a5bbe43d8d757d082b095f86363a24d73fd4..c1e1be31341f9c419c20e886268e46955c90cbb7 100644
--- a/examples/programs/vacid_0_union_find.mlw
+++ b/examples/programs/vacid_0_union_find.mlw
@@ -79,7 +79,7 @@ module M
(***
- parameter ghost_find : u:ref uf -> x:int ->
+ val ghost_find : u:ref uf -> x:int ->
{ inv !u /\ 0 <= x < size !u }
int reads u
{ repr !u x result }
diff --git a/modules/array.mlw b/modules/array.mlw
index 7fbb843600b3382131f160a5742a712908af4afb..1bd56f6d97967fe13d5792069b2aa4474b9b8a99 100644
--- a/modules/array.mlw
+++ b/modules/array.mlw
@@ -17,13 +17,13 @@ module Array
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
- parameter ([]) (a: array 'a) (i: int) :
+ val ([]) (a: array 'a) (i: int) :
{ 0 <= i < length a } 'a reads a { result = a[i] }
- parameter ([]<-) (a: array 'a) (i: int) (v: 'a) :
+ val ([]<-) (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
- parameter length (a: array 'a) : {} int { result = a.length }
+ val length (a: array 'a) : {} int { result = a.length }
(* unsafe get/set operations with no precondition *)
exception OutOfBounds
@@ -42,26 +42,26 @@ module Array
{ 0 <= i < length a /\ a = (old a)[i <- v] }
| OutOfBounds -> { i < 0 \/ i >= length a }
- parameter make (n: int) (v: 'a) :
+ val make (n: int) (v: 'a) :
{}
array 'a
{ result = {| length = n; elts = M.const v |} }
(* { length result = n /\ forall i:int. 0 <= i < n -> result[i] = v} *)
- parameter append (a1: array 'a) (a2: array 'a) :
+ val append (a1: array 'a) (a2: array 'a) :
{}
array 'a
{ length result = length a1 + length a2 /\
(forall i:int. 0 <= i < length a1 -> result[i] = a1[i]) /\
(forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]) }
- parameter sub (a: array 'a) (ofs: int) (len: int) :
+ val sub (a: array 'a) (ofs: int) (len: int) :
{ 0 <= ofs /\ ofs + len <= length a }
array 'a
{ length result = len /\
forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
- parameter copy (a: array 'a) :
+ val copy (a: array 'a) :
{}
array 'a
{ length result = length a /\
@@ -85,7 +85,7 @@ module Array
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
- parameter blit (a1: array 'a) (ofs1: int)
+ val blit (a1: array 'a) (ofs1: int)
(a2: array 'a) (ofs2: int) (len: int) :
{ 0 <= ofs1 /\ ofs1 + len <= length a1 /\
0 <= ofs2 /\ ofs2 + len <= length a2 }
diff --git a/modules/hashtbl.mlw b/modules/hashtbl.mlw
index 09ce54237c40d3eb87f842d68f3d1b88ec5cac35..555dbae5b60b6d0e0d11fa0290a5602f60468ea0 100644
--- a/modules/hashtbl.mlw
+++ b/modules/hashtbl.mlw
@@ -10,60 +10,60 @@ module Hashtbl
function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
- parameter create (n:int) :
+ val create (n:int) :
{} t 'a { forall k: key. result[k] = Nil }
- parameter clear (h: t 'a) :
+ val clear (h: t 'a) :
{} unit writes h { forall k: key. h[k] = Nil }
- parameter add (h: t 'a) (k: key) (v: 'a) :
+ val add (h: t 'a) (k: key) (v: 'a) :
{}
unit writes h
{ h[k] = Cons v (old h)[k] /\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
- parameter mem (h: t 'a) (k: key) :
+ val mem (h: t 'a) (k: key) :
{}
bool reads h
{ result=True <-> h[k] <> Nil }
- parameter find (h: t 'a) (k: key) :
+ val find (h: t 'a) (k: key) :
{ h[k] <> Nil }
'a reads h
{ match h[k] with Nil -> false | Cons v _ -> result = v end }
- parameter find_all (h: t 'a) (k: key) :
+ val find_all (h: t 'a) (k: key) :
{}
list 'a reads h
{ result = h[k] }
exception NotFound
- parameter defensive_find (h: t 'a) (k: key) :
+ val defensive_find (h: t 'a) (k: key) :
{}
'a reads h raises NotFound
{ match h[k] with Nil -> false | Cons v _ -> result = v end }
| NotFound -> { h[k] = Nil }
- parameter copy (h: t 'a) :
+ val copy (h: t 'a) :
{}
t 'a reads h
{ forall k: key. result[k] = h[k] }
- parameter remove (h: t 'a) (k: key) :
+ val remove (h: t 'a) (k: key) :
{ h[k] <> Nil }
unit writes h
{ (match (old h)[k] with Nil -> false | Cons _ l -> h[k] =l end) /\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
- parameter replace (h: t 'a) (k: key) (v: 'a) :
+ val replace (h: t 'a) (k: key) (v: 'a) :
{}
unit writes h
{ (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end))
/\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
- parameter length (h: t 'a) :
+ val length (h: t 'a) :
{}
int reads h
{} (* = the number of distinct keys *)
diff --git a/modules/queue.mlw b/modules/queue.mlw
index 215f061a88532af2937490391f8216318d6dcab3..d1658a3df718aab098249d0c42dcb198e2a0ee69 100644
--- a/modules/queue.mlw
+++ b/modules/queue.mlw
@@ -9,14 +9,14 @@ module Queue
type t 'a model {| mutable elts: list 'a |}
- parameter create : unit -> {} t 'a { result.elts = Nil }
+ val create : unit -> {} t 'a { result.elts = Nil }
- parameter push :
+ val push :
x:'a -> s:t 'a -> {} unit writes s { s.elts = old s.elts ++ Cons x Nil }
exception Empty
- parameter pop :
+ val pop :
s:t 'a ->
{}
'a
@@ -25,7 +25,7 @@ module Queue
| Cons x t -> result = x /\ s.elts = t end }
| Empty -> { s.elts = old s.elts = Nil }
- parameter top :
+ val top :
s:t 'a ->
{}
'a
@@ -33,14 +33,14 @@ module Queue
{ match s.elts with Nil -> false | Cons x _ -> result = x end }
| Empty -> { s.elts = Nil }
- parameter clear : s:t 'a -> {} unit writes s { s.elts = Nil }
+ val clear : s:t 'a -> {} unit writes s { s.elts = Nil }
- parameter copy : s:t 'a -> {} t 'a { result = s }
+ val copy : s:t 'a -> {} t 'a { result = s }
- parameter is_empty :
+ val is_empty :
s:t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
- parameter length : s:t 'a -> {} int reads s { result = length s.elts }
+ val length : s:t 'a -> {} int reads s { result = length s.elts }
end
diff --git a/modules/random.mlw b/modules/random.mlw
index 05372e4414238c900845061f1d31cf922d589f59..28bab274d4068acf187835cc83355646a7521bdb 100644
--- a/modules/random.mlw
+++ b/modules/random.mlw
@@ -5,7 +5,7 @@
is to take advantage of the non-determinism of Hoare triples.
Simply declaring a function
- parameter random_int: unit -> {} int {}
+ val random_int: unit -> {} int {}
is typically enough. Two calls to random_int return values that can not
be proved equal, which is exactly what we need.
@@ -49,21 +49,21 @@ module State
type state model {| mutable state: generator |}
- parameter create (seed: int) :
+ val create (seed: int) :
{} state { result.state = create seed }
- parameter init (s: state) (seed: int) :
+ val init (s: state) (seed: int) :
{} unit writes s { s.state = create seed }
- parameter self_init (s: state) :
+ val self_init (s: state) :
{} unit writes s {}
- parameter random_bool (s: state) :
+ val random_bool (s: state) :
{}
bool writes s
{ s.state = next (old s.state) /\ result = get_bool s.state }
- parameter random_int (s: state) (n: int) :
+ val random_int (s: state) (n: int) :
{ 0 < n }
int writes s
{ s.state = next (old s.state) /\ result = get_int s.state n /\
@@ -78,7 +78,7 @@ module Random
use import int.Int
use import module State
- parameter s: state
+ val s: state
let init (seed: int) =
{} init s seed { s.state = create seed }
diff --git a/modules/ref.mlw b/modules/ref.mlw
index d24947117e6d4fd53db8eff5c9a26f215eeed18e..17fb5fa2e8c1c1afe34dc63097d0ab34075bc471 100644
--- a/modules/ref.mlw
+++ b/modules/ref.mlw
@@ -6,13 +6,13 @@ module Ref
function (!) (x: ref 'a) : 'a = x.contents
- (* parameter ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
+ (* val ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
- (* parameter (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
+ (* val (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
let (!) (r:ref 'a) = {} r.contents { result = !r }
- (* parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
+ (* val (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
let (:=) (r:ref 'a) (v:'a) = {} r.contents <- v { !r = v }
end
@@ -22,10 +22,10 @@ module Refint
use export int.Int
use export module Ref
- (* parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
+ (* val incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
let incr (r: ref int) = {} r := !r + 1 { !r = old !r + 1 }
- (* parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
+ (* val decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
let decr (r: ref int) = {} r := !r - 1 { !r = old !r - 1 }
let (+=) (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
diff --git a/modules/stack.mlw b/modules/stack.mlw
index aa266e4d1e48b441ddaec2fb7784d7dd448f4920..7ef5181619cf351d2ca24627fe3ff0702b83a19f 100644
--- a/modules/stack.mlw
+++ b/modules/stack.mlw
@@ -8,14 +8,14 @@ module Stack
type t 'a model {| mutable elts: list 'a |}
- parameter create : unit -> {} t 'a { result.elts = Nil }
+ val create : unit -> {} t 'a { result.elts = Nil }
- parameter push :
+ val push :
x:'a -> s:t 'a -> {} unit writes s { s.elts = Cons x (old s.elts) }
exception Empty
- parameter pop :
+ val pop :
s:t 'a ->
{}
'a
@@ -24,7 +24,7 @@ module Stack
| Cons x t -> result = x /\ s.elts = t end }
| Empty -> { s.elts = old s.elts = Nil }
- parameter top :
+ val top :
s:t 'a ->
{}
'a
@@ -32,14 +32,14 @@ module Stack
{ match s.elts with Nil -> false | Cons x _ -> result = x end }
| Empty -> { s.elts = Nil }
- parameter clear : s:t 'a -> {} unit writes s { s.elts = Nil }
+ val clear : s:t 'a -> {} unit writes s { s.elts = Nil }
- parameter copy : s:t 'a -> {} t 'a { result = s }
+ val copy : s:t 'a -> {} t 'a { result = s }
- parameter is_empty :
+ val is_empty :
s:t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
- parameter length : s:t 'a -> {} int reads s { result = length s.elts }
+ val length : s:t 'a -> {} int reads s { result = length s.elts }
end
diff --git a/modules/string.mlw b/modules/string.mlw
index 1d2ce42fb7e1c526d3903ac86b3b8891a6a8925b..7465e9dba88e6c82955c7ed638340250ee8bb935 100644
--- a/modules/string.mlw
+++ b/modules/string.mlw
@@ -5,9 +5,9 @@ module Char
type char model int
- parameter chr : x:int -> { 0 <= x <= 255 } char { result = x }
+ val chr : x:int -> { 0 <= x <= 255 } char { result = x }
- parameter code : c:char -> {} int { result = c /\ 0 <= c <= 255 }
+ val code : c:char -> {} int { result = c /\ 0 <= c <= 255 }
function uppercase int : int
function lowercase int : int
@@ -22,8 +22,8 @@ module Char
axiom lowercase_other:
forall c:int. 0 <= c < 65 \/ 90 < c <= 127 -> lowercase c = c
- parameter uppercase : c:char -> {} char { result = uppercase c }
- parameter lowercase : c:char -> {} char { result = lowercase c }
+ val uppercase : c:char -> {} char { result = uppercase c }
+ val lowercase : c:char -> {} char { result = lowercase c }
(* TODO
- compare ?
@@ -39,43 +39,43 @@ module String
type string model {| length: int; mutable chars: map int char |}
- parameter create : len:int -> { len >= 0 } string { length result = len }
+ val create : len:int -> { len >= 0 } string { length result = len }
function ([]) (s: string) (i :int) : char = M.([]) s.chars i
function get (s: string) (i :int) : char = M.([]) s.chars i
- parameter make : len:int -> c:char ->
+ val make : len:int -> c:char ->
{ len >= 0 }
string
{ length result = len /\
forall i:int. 0 <= i < len -> result[i] = c }
- parameter get : s:string -> i:int ->
+ val get : s:string -> i:int ->
{ 0 <= i < length s } char reads s { result = s[i] }
- parameter unsafe_get : s:string -> i:int ->
+ val unsafe_get : s:string -> i:int ->
{ } char reads s { result = s[i] }
- parameter set : s:string -> i:int -> v:char ->
+ val set : s:string -> i:int -> v:char ->
{ 0 <= i < length s } unit writes s { s.chars = (old s.chars)[i <- v] }
- parameter unsafe_set : s:string -> i:int -> v:char ->
+ val unsafe_set : s:string -> i:int -> v:char ->
{ } unit writes s { s.chars = (old s.chars)[i <- v] }
- parameter length : s:string -> {} int reads s { result = length s }
+ val length : s:string -> {} int reads s { result = length s }
- parameter copy : s:string ->
+ val copy : s:string ->
{}
string
{ length result = length s /\
forall i:int. 0 <= i < length result -> result[i] = s[i] }
- parameter uppercase : s:string ->
+ val uppercase : s:string ->
{}
string
{ length result = length s /\
forall i:int. 0 <= i < length result ->
result[i] = Char.uppercase s[i] }
- parameter lowercase : s:string ->
+ val lowercase : s:string ->
{}
string
{ length result = length s /\
@@ -104,12 +104,12 @@ module Buffer
type t model {| mutable length: int; mutable contents: map int char |}
- parameter create : size:int -> { size >= 0 } t { result.length = 0 }
+ val create : size:int -> { size >= 0 } t { result.length = 0 }
(** [size] is only given as a hint for the initial size *)
- parameter contents : b:t -> { } string { S.length result = length b }
+ val contents : b:t -> { } string { S.length result = length b }
- parameter add_char :
+ val add_char :
b:t -> c:char ->
{ }
unit writes b.length b.contents
@@ -118,7 +118,7 @@ module Buffer
0 <= i < length b -> b.contents[i] = (old b.contents)[i]) /\
b.contents[length b - 1] = c }
- parameter add_string :
+ val add_string :
b:t -> s:string ->
{ }
unit reads s writes b.length b.contents
diff --git a/share/emacs/why.el b/share/emacs/why.el
index ba485766e80fea6876efaac764d1e0c7610366ad..141e00f6880e4b4afb69883bac697a34c05a505e 100644
--- a/share/emacs/why.el
+++ b/share/emacs/why.el
@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
- `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
+ `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
`(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
diff --git a/share/lang/why.lang b/share/lang/why.lang
index 2310f794db5a1dbc56bf9f5ac312cf3ead263f2d..d1e53b612d441f69445c430a777f289438b575f1 100644
--- a/share/lang/why.lang
+++ b/share/lang/why.lang
@@ -161,7 +161,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
with
module
exception
- parameter
+ val
match
@@ -173,6 +173,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
else
for
to
+ downto
do
done
forall
diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll
index 58ba5b79c5a80d583157853cd14b5a14cabd823b..1982a69d0d63d0abeccf87fabeff040d9079fbc5 100644
--- a/src/parser/lexer.mll
+++ b/src/parser/lexer.mll
@@ -95,13 +95,13 @@
"model", MODEL;
"module", MODULE;
"mutable", MUTABLE;
- "parameter", PARAMETER;
"raise", RAISE;
"raises", RAISES;
"reads", READS;
"rec", REC;
"to", TO;
"try", TRY;
+ "val", VAL;
"variant", VARIANT;
"while", WHILE;
"writes", WRITES;
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index bc5ffa2c9038c874f16e3f05ed1f891ab7fe6740..d58dabe98446a16f0ed4a974fa20cc96642c63d7 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -187,8 +187,8 @@ end
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
-%token FUN INVARIANT LABEL LOOP MODEL MODULE MUTABLE PARAMETER RAISE
-%token RAISES READS REC TO TRY VARIANT WHILE WRITES
+%token FUN INVARIANT LABEL LOOP MODEL MODULE MUTABLE RAISE
+%token RAISES READS REC TO TRY VAL VARIANT WHILE WRITES
/* symbols */
@@ -986,9 +986,9 @@ program_decl:
{ Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
-| PARAMETER lident_rich_pgm labels COLON type_v
+| VAL lident_rich_pgm labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
-| PARAMETER lident_rich_pgm labels list1_type_v_param COLON type_c
+| VAL lident_rich_pgm labels list1_type_v_param COLON type_c
{ let tv = Tarrow ($4, $6) in
Dparam (add_lab $2 $3, tv) }
| EXCEPTION uident labels
diff --git a/src/why3doc/to_html.mll b/src/why3doc/to_html.mll
index fc3f2dddac0c479c9c1051d17b9803a98ea44a1d..b3ef472af0707dfdf1124fd410e41805e72ff470 100644
--- a/src/why3doc/to_html.mll
+++ b/src/why3doc/to_html.mll
@@ -56,15 +56,15 @@
List.iter
(fun s -> Hashtbl.add ht s ())
[ "theory"; "end";
- "type"; "logic"; "clone"; "use"; "import"; "export";
- "axiom"; "inductive"; "goal"; "lemma";
+ "type"; "function"; "predicate"; "clone"; "use";
+ "import"; "export"; "axiom"; "inductive"; "goal"; "lemma";
"match"; "with"; "let"; "in"; "if"; "then"; "else";
- "forall"; "exists"; "and"; "or";
+ "forall"; "exists";
"as"; "assert"; "begin";
"do"; "done"; "downto"; "else";
- "exception"; "parameter"; "for"; "fun";
+ "exception"; "val"; "for"; "fun";
"if"; "in";
"module"; "mutable";
"rec"; "then"; "to";
diff --git a/tests/test-bobot.why b/tests/test-bobot.why
index 55b353151da8cd11259a7d7848e973a38de79f06..1b6683ae8d560395c9da05f4398da486565fcd21 100644
--- a/tests/test-bobot.why
+++ b/tests/test-bobot.why
@@ -3,8 +3,8 @@
theory Test_inline_trivial
type t
- logic c : t
- logic eq (x y :'a) = x=y
+ function c : t
+ predicate eq (x y :'a) = x=y
goal G : eq c c
end
@@ -17,15 +17,15 @@ end
(*
theory Test_encoding
use import int.Int
- logic id(x: int) : int = x
- logic id2(x: int) : int = id(x)
- logic succ(x:int) : int = id(x+1)
+ function id(x: int) : int = x
+ function id2(x: int) : int = id(x)
+ function succ(x:int) : int = id(x+1)
type myt
- logic f (int) : myt
+ function f (int) : myt
clone transform.encoding_decorate.Kept with type t = myt
- goal G : (forall x:int.f(x)=f(x)) or
+ goal G : (forall x:int.f(x)=f(x)) \/
(forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y
end
@@ -33,49 +33,49 @@ end
theory Test_simplify_array
use import int.Int
- use import array.Array
- goal G1 : forall x y:int. forall m: t int int.
+ use import map.Map
+ goal G1 : forall x y:int. forall m: map int int.
get (set m y x) y = x
- goal G2 : forall x y:int. forall m: t int int.
+ goal G2 : forall x y:int. forall m: map int int.
get (set m y x) y = y
- goal G3 : forall x y:int. forall m: t int int.
- get (create_const x) y = x
+ goal G3 : forall x y:int. forall m: map int int.
+ get (const x) y = x
end
theory Test_simplify_array2
use import int.Int
- use import array.Array
+ use import map.Map
type t2 'a
- goal G1 : forall y:int. forall x:t2 int. forall m: t int (t2 int).
+ goal G1 : forall y:int. forall x:t2 int. forall m: map int (t2 int).
get (set m y x) y = x
end
theory Test_guard
type t
- logic f t : t
- logic a : t
- logic b : t
+ function f t : t
+ function a : t
+ function b : t
goal G : forall x:t. f a = x
end
theory Test_conjunction
use import int.Int
- axiom Trivial : 2 * 2 = 4 and 4 * 2 = 8
+ axiom Trivial : 2 * 2 = 4 /\ 4 * 2 = 8
goal G :
- forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
+ forall x:int. x*x=4 -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8)
goal G2 :
forall x:int.
- (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
+ (x+x=4 \/ x*x=4) -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8)
end
theory Split_conj
- logic p(x:int)
- (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
- (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
+ predicate p(x:int)
+ (*goal G : forall x,y,z:int. ((p(x) -> p(y)) /\ ((not p(x)) -> p(z))) -> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*)
+ (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
goal G : forall x y z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
- (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *)
- (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
+ (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) /\ (not p(x)) \/ ((p(z)) /\ (p(x))))) *)
+ (*goal G : forall x,y,z:int. (p(x) \/ p(y)) -> p(z)*)
end
@@ -85,19 +85,19 @@ theory TestEnco
use import int.Int
meta "encoding : kept" type int
type mytype 'a
- logic id(x: int) : int = x
- logic id2(x: int) : int = id(x)
- logic succ(x:int) : int = id(x+1)
+ function id(x: int) : int = x
+ function id2(x: int) : int = id(x)
+ function succ(x:int) : int = id(x+1)
- goal G : (forall x:int. x=x) or
+ goal G : (forall x:int. x=x) \/
(forall x:int. x=x+1)
- logic p('a ) : mytype 'a
- logic p2(mytype 'a) : 'a
+ function p('a ) : mytype 'a
+ function p2(mytype 'a) : 'a
type toto
- logic f (toto) : mytype toto
+ function f (toto) : mytype toto
axiom A0 : forall x : toto. f(x) = p(x)
- logic g (mytype int) : toto
- logic h (int) : toto
+ function g (mytype int) : toto
+ function h (int) : toto
axiom A05 : forall x : int. g(p(x)) = h(x)
axiom A1 : forall x : mytype 'a. p(p2(x)) = x
goal G2 : forall x:mytype toto. f(p2(x)) = x
@@ -107,7 +107,7 @@ theory TestIte
use import int.Int
use list.Length
use list.Mem
- logic abs(x:int) : int = if x >= 0 then x else -x
+ function abs(x:int) : int = if x >= 0 then x else -x
goal G : forall x:int. abs(x) >= 0
goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0
end
@@ -127,10 +127,10 @@ end
theory TestEncodingEnumerate
type t = A | B | C
- goal G : forall x : t. (x = A or x = B) -> x<>C
+ goal G : forall x : t. (x = A \/ x = B) -> x<>C
goal G1 : forall x : t. B <> A
- goal G2 : forall x : t. x = A or x = B or x=C
- goal G3 : forall x : t. x = A or x = B or x <> C
+ goal G2 : forall x : t. x = A \/ x = B \/ x=C
+ goal G3 : forall x : t. x = A \/ x = B \/ x <> C
end
(*
diff --git a/tests/test-claude.why b/tests/test-claude.why
index 3ea34949ce4967dcc22c969d957f065a49b51743..dbe2cd036a7d6049e2c52470a8146ae71b90d6cc 100644
--- a/tests/test-claude.why
+++ b/tests/test-claude.why
@@ -4,11 +4,11 @@ theory TestProp
goal Test0_5 : true -> false
- logic a
+ predicate a
- logic b
+ predicate b
- goal Test1: a and b -> a
+ goal Test1: a /\ b -> a
end
@@ -26,29 +26,29 @@ theory TestInt
goal Test5: forall x:int. x <> 0 -> x*x > 0
- goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)
+ goal Test6: 2+3 = 5 /\ (forall x:int. x*x >= 0)
- goal Test7: 0 = 2 and 2 = 3 and 4 = 5 and 6 = 7
+ goal Test7: 0 = 2 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
- goal Test8: 2+2=4 and 3+3=6
+ goal Test8: 2+2=4 /\ 3+3=6
axiom A : 1 = 2
- goal Test9: 2+2=5 and 3+3=8
+ goal Test9: 2+2=5 /\ 3+3=8
end
theory TestSplit
- logic aa int
+ predicate aa int
- logic bb int
+ predicate bb int
- goal G1 : (aa 5) and ("stop_split" aa 0 and bb 6) and ("stop_split" aa 1 and bb 2)
+ goal G1 : (aa 5) /\ ("stop_split" aa 0 /\ bb 6) /\ ("stop_split" aa 1 /\ bb 2)
goal G2 : ("stop_split" aa 0 && bb 1) && ("stop_split" aa 1 && bb 2)
- goal G3 : forall x:int. ("stop_split" aa x and bb 1) and ("stop_split" aa 1 and bb 2)
+ goal G3 : forall x:int. ("stop_split" aa x /\ bb 1) /\ ("stop_split" aa 1 /\ bb 2)
goal G4 : forall x:int. ("stop_split" aa x && bb 1) && ("stop_split" aa 1 && bb 2)
@@ -85,13 +85,13 @@ theory TestList
use import int.Int
use import list.List
- logic x : list int
+ function x : list int
(*
goal Test1:
match x with
- | Nil -> 1 = 0 and 2 = 3
- | Cons _ Nil -> 4 = 5 and 6 = 7
+ | Nil -> 1 = 0 /\ 2 = 3
+ | Cons _ Nil -> 4 = 5 /\ 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
*)
@@ -109,7 +109,7 @@ theory TestReal
goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
- goal T: forall x y:real. abs x <= 1.0 and abs y <= 1.0 -> x - y <= 2.0
+ goal T: forall x y:real. abs x <= 1.0 /\ abs y <= 1.0 -> x - y <= 2.0
end
@@ -128,14 +128,14 @@ theory TestRealize
type t
- logic p t t
+ predicate p t t
axiom P_arefl: forall x:t. not (p x x)
(*
- axiom P_total: forall x y:t. p x y or p y x or x=y
+ axiom P_total: forall x y:t. p x y \/ p y x \/ x=y
- logic f t : t
+ function f t : t
axiom A : forall x:t. p (f x) x
@@ -151,7 +151,7 @@ theory TestRealizeUse
use import TestRealize
- logic q t : t
+ function q t : t
axiom C : forall x:t. p (q x) x
@@ -163,7 +163,7 @@ theory TestInline
goal T : 1 = 2
- logic p (x:int) (y:int) = x <= 3 and y <= 7
+ predicate p (x:int) (y:int) = x <= 3 /\ y <= 7
goal G : p 4 4
diff --git a/tests/test-jcf.why b/tests/test-jcf.why
index 14befb9172209bff2cd8b5482f1123175075c4b6..256ffc0f22a442d1a63d422087d192010bb6b1b5 100644
--- a/tests/test-jcf.why
+++ b/tests/test-jcf.why
@@ -1,22 +1,22 @@
theory Bijection
use export int.Int
- logic n : int
- logic f int : int
+ function n : int
+ function f int : int
axiom dom_f : forall i: int. 0 <= i < n -> 0 <= f i < n
- logic g int : int
+ function g int : int
axiom gf : forall i: int. 0 <= i < n -> g (f i) = i
end
theory Test1
- logic id (i: int) : int = i
- clone import Bijection with logic f = id, lemma dom_f
+ function id (i: int) : int = i
+ clone import Bijection with function f = id, lemma dom_f
goal G: n > 4 -> g (id 4) = 4
end
theory Order
type t
- logic (<=) t t
+ predicate (<=) t t
axiom le_refl : forall x : t. x <= x
axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
diff --git a/tests/test-pgm-jcf.mlw b/tests/test-pgm-jcf.mlw
index 799cde15969d19aa9556cfbba31d39bd7b462b4e..36fd68fe73eadcc5d8aa9104cd9128dd0b4d4b41 100644
--- a/tests/test-pgm-jcf.mlw
+++ b/tests/test-pgm-jcf.mlw
@@ -22,10 +22,10 @@ module PoorArrays
type array_contents 'a = {| length: int; elts : map int 'a |}
type array 'a = ref (array_contents 'a)
- parameter get (a: array 'a) (i: int) :
+ val get (a: array 'a) (i: int) :
{ 0 <= i < length !a } 'a { result = M.get !a.elts i }
- parameter set (a: array 'a) (i: int) (v: 'a) :
+ val set (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length !a }
unit writes a
{ !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v }
@@ -44,7 +44,7 @@ module M
(***
use import option.Option
- parameter clear (o : option (ref int)) :
+ val clear (o : option (ref int)) :
{} unit writes (match o with Some r -> r end).contents { !r = 0 }
***)
diff --git a/theories/pervasives.mlw b/theories/pervasives.mlw
deleted file mode 100644
index d44174b8ece49a2d30b8bdc0a0ea112f969203e3..0000000000000000000000000000000000000000
--- a/theories/pervasives.mlw
+++ /dev/null
@@ -1,10 +0,0 @@
-module Ref
-
- { use import programs.Prelude }
-
- parameter ref : v:'a -> {} ref 'a { !result = v }
-
- parameter set : r:ref 'a -> v:'a -> {} unit writes r { !r = v }
-
-end
-