Commit a1e3ab18 authored by Andrei Paskevich's avatar Andrei Paskevich

rename "parameter" to "val"

parent 33f61172
......@@ -6,7 +6,7 @@ module M
x := 1;
y := 2
parameter r : ref int
val r : ref int
let test () =
foo r r
......
......@@ -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
......@@ -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
......@@ -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
......@@ -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
module M
parameter f : x:int -> {} unit writes 1 {}
val f : x:int -> {} unit writes 1 {}
end
module M
parameter f : x:int -> {} unit writes x {}
val f : x:int -> {} unit writes x {}
end
......@@ -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
......@@ -2,6 +2,6 @@ module M
use import module stdlib.Ref
parameter r : ref 'a
val r : ref 'a
end
......@@ -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
......@@ -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 }
......
......@@ -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
......
......@@ -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 }
......
......@@ -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 }
......
......@@ -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) }
......
......@@ -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) =
......
......@@ -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 }
......
......@@ -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 }
......
......@@ -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 () =
......
......@@ -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 }
......
......@@ -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
......
......@@ -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
......
......@@ -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" ;
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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) }
......
......@@ -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
......
......@@ -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
......
......@@ -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. *)
......
......@@ -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
......
......@@ -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:
......
......@@ -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))}
......
......@@ -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
......
......@@ -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 }
......
......@@ -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) =
{}
......
......@@ -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
......
......@@ -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 :