syntax for assignment

parent 26c19ce1
......@@ -8,30 +8,30 @@ module M
parameter a : array int
logic inv (a : array int) =
logic inv (a : array int) =
a[0] = 0 and length a = 11 and forall k:int. 1 <= k <= 10 -> 0 < a[k]
parameter loop1 : ref int
parameter loop2 : ref int
let insertion_sort () =
{ inv a and
{ inv a and
(* ghost *) loop1 = 0 and loop2 = 0 }
let i = ref 2 in
let i = ref 2 in
while !i <= 10 do
invariant { 2 <= i <= 11 and inv a and
(* ghost *) loop1 = i - 2 and 2 * loop2 <= (i-2) * (i-1) }
(* ghost *) loop1 = i - 2 and 2 * loop2 <= (i-2) * (i-1) }
variant { 10 - i }
(* ghost *) incr loop1;
let j = ref !i in
while a[!j] < a[!j - 1] do
invariant { 1 <= j <= i and inv a and
(* ghost *) 2 * loop2 <= (i-2) * (i-1) + 2*(i-j) }
invariant { 1 <= j <= i and inv a and
(* ghost *) 2 * loop2 <= (i-2) * (i-1) + 2*(i-j) }
variant { j }
(* ghost *) incr loop2;
let temp = a[!j] in
set a !j a[!j - 1];
set a (!j - 1) temp;
a[!j] <- a[!j - 1];
a[!j - 1] <- temp;
decr j
done;
incr i
......@@ -39,7 +39,7 @@ module M
{ loop1 = 9 and loop2 <= 45 }
end
module ARM
use export int.Int
......@@ -49,14 +49,14 @@ module ARM
(* 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 ->
parameter 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 :
parameter data_str :
a:int -> v:int -> {} int writes data { data = (old data)[a <- v] }
*)
......@@ -69,17 +69,17 @@ module ARM
parameter fp : ref int
parameter pc : ref int (* pc *)
parameter ldr :
parameter ldr :
r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { r = mem[a] }
parameter str :
parameter str :
r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { mem = (old mem)[a <- r] }
(* condition flags *)
parameter le : ref bool
parameter cmp : r:ref int -> v:int ->
{}
unit reads r.contents writes le.contents
parameter cmp : r:ref int -> v:int ->
{}
unit reads r.contents writes le.contents
{ le=True <-> r <= v }
end
......@@ -114,13 +114,13 @@ module InsertionSortExample
(* stack and data segment do not overlap *)
logic separation (fp : int) = a+10 < fp-24
logic inv (mem: map int int) =
logic inv (mem: map int int) =
mem[a] = 0 and forall k:int. 1 <= k <= 10 -> 0 < mem[a + k]
logic inv_l2 (mem: map int int) (fp : int) (l4 : int) =
2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem
let path_init_l2 () =
let path_init_l2 () =
{ separation fp and inv mem }
(* ghost *) l4 := 0; l7 := 0;
r3 := 2;
......@@ -137,7 +137,7 @@ module InsertionSortExample
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/arm.gui"
End:
End:
*)
......@@ -7,16 +7,16 @@ module M
(* iteration on a set *)
parameter set_has_next :
s:ref (S.set 'a) ->
{}
bool reads s
parameter 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 :
s:ref (S.set 'a) ->
s:ref (S.set 'a) ->
{ not S.is_empty s }
'a writes s
'a writes s
{ S.mem result (old s) and s = S.remove result (old s) }
(* the graph *)
......@@ -27,7 +27,7 @@ logic v : S.set vertex
logic g_succ(vertex) : S.set vertex
axiom G_succ_sound :
axiom G_succ_sound :
forall x:vertex. S.subset (g_succ x) v
logic weight vertex vertex : int (* edge weight, if there is an edge *)
......@@ -35,14 +35,14 @@ logic weight vertex vertex : int (* edge weight, if there is an edge *)
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
parameter eq_vertex :
parameter eq_vertex :
x:vertex -> y:vertex -> {} bool { if result=True then x=y else x<>y }
(* visited vertices *)
parameter visited : ref (S.set vertex)
parameter visited_add :
parameter visited_add :
x:vertex -> {} unit writes visited { visited = S.add x (old visited) }
(* current distances *)
......@@ -53,18 +53,18 @@ parameter d : ref (M.map vertex int)
parameter q : ref (S.set vertex)
parameter q_is_empty :
unit ->
{}
bool reads q
parameter q_is_empty :
unit ->
{}
bool reads 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
{}
unit writes visited q d
{ S.is_empty visited and
q = S.add src S.empty and
d = M.set (old d) src 0 }
let relax u v =
......@@ -77,38 +77,38 @@ 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)
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)
or
(S.mem v q and M.get (old d) u + weight u v < M.get (old d) v and
(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)) }
d = M.set (old d) v (M.get (old d) u + weight u v)) }
logic min (m:vertex) (q:S.set vertex) (d:M.map vertex int) =
S.mem m q and
S.mem m q and
forall x:vertex. S.mem x q -> M.get d m <= M.get d x
parameter q_extract_min :
unit ->
{ not S.is_empty q }
vertex reads d writes q
{ not S.is_empty q }
vertex reads d writes q
{ min result (old q) d and q = S.remove result (old q) }
(* paths and shortest paths
path x y d =
(* paths and shortest paths
path x y d =
there is a path from x to y of length d
shortest_path x y d =
shortest_path x y d =
there is a path from x to y of length d, and no shorter path *)
inductive path vertex vertex int =
| Path_nil :
inductive path vertex vertex int =
| Path_nil :
forall x:vertex. path x x 0
| Path_cons :
forall x y z:vertex. forall d:int.
| Path_cons :
forall x y z:vertex. forall d:int.
path x y d -> S.mem z (g_succ y) -> path x z (d+weight y z)
lemma Length_nonneg : forall x y:vertex. forall d:int. path x y d -> d >= 0
......@@ -128,18 +128,18 @@ lemma Path_shortest_path :
(* lemmas (those requiring induction) *)
lemma Main_lemma :
forall src v:vertex. forall d:int.
forall src v:vertex. forall d:int.
path src v d -> not shortest_path src v d ->
exists v':vertex. exists d':int.
exists v':vertex. exists d':int.
shortest_path src v' d' and S.mem v (g_succ v') and d' + weight v' v < d
lemma Completeness_lemma :
forall s:S.set vertex. forall src:vertex. forall dst:vertex. forall d:int.
forall s:S.set vertex. forall src:vertex. forall dst:vertex. forall d:int.
(* if s is closed under g_succ *)
(forall v:vertex.
(forall v:vertex.
S.mem v s -> forall w:vertex. S.mem w (g_succ v) -> S.mem w s) ->
(* and if s contains src *)
S.mem src s ->
S.mem src s ->
(* then any vertex reachable from s is also in s *)
path src dst d -> S.mem dst s
......@@ -153,7 +153,7 @@ logic inv (src:vertex) (s q:S.set vertex) (d:M.map vertex int) =
(* S,Q are contained in V *)
and S.subset s v and S.subset q v
(* S and Q are disjoint *)
and
and
(forall v:vertex. S.mem v q -> S.mem v s -> false)
(* we already found the shortest paths for vertices in S *)
and
......@@ -163,21 +163,21 @@ logic inv (src:vertex) (s q:S.set vertex) (d:M.map vertex int) =
(forall v:vertex. S.mem v q -> path src v (M.get d v))
(* vertices at distance < min(Q) are already in S *)
and
(forall m:vertex. min m q d ->
forall x:vertex. forall dx:int. shortest_path src x dx ->
dx < M.get d m -> S.mem x s)
(forall m:vertex. min m q d ->
forall x:vertex. forall dx:int. shortest_path src x dx ->
dx < M.get d m -> S.mem x s)
logic inv_succ (src:vertex) (s q : S.set vertex) =
(* successors of vertices in S are either in S or in Q *)
(forall x:vertex. S.mem x s ->
(forall x:vertex. S.mem x s ->
forall y:vertex. S.mem y (g_succ x) -> S.mem y s or S.mem y q)
logic inv_succ2 (src:vertex) (s q : S.set vertex)
(u:vertex) (su:S.set vertex) =
(* successors of vertices in S are either in S or in Q,
unless they are successors of u still in su *)
(forall x:vertex. S.mem x s ->
forall y:vertex. S.mem y (g_succ x) ->
(forall x:vertex. S.mem x s ->
forall y:vertex. S.mem y (g_succ x) ->
(x<>u or (x=u and not S.mem y su)) -> S.mem y s or S.mem y q)
(* code *)
......@@ -192,8 +192,8 @@ let shortest_path_code (src:vertex) (dst:vertex) =
assert { shortest_path src u (M.get d u) };
visited_add u;
let su = ref (g_succ u) in
while not (set_has_next su) do
invariant
while not (set_has_next su) do
invariant
{ S.subset su (g_succ u) and
inv src visited q d and inv_succ2 src visited q u su }
variant { S.cardinal su }
......@@ -201,16 +201,16 @@ let shortest_path_code (src:vertex) (dst:vertex) =
relax u v
done
done
{ (forall v:vertex.
S.mem v visited -> shortest_path src v (M.get d v))
{ (forall v:vertex.
S.mem v visited -> shortest_path src v (M.get d v))
and
(forall v:vertex.
(forall v:vertex.
not S.mem v visited -> forall dv:int. not path src v dv) }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/dijkstra"
End:
End:
*)
......@@ -83,14 +83,14 @@ module Distance
for i = 0 to n2 do
invariant { length t = n2+1 and
forall j:int. 0 <= j < i -> t[j] = n2-j }
set t i (n2 - i)
t[i] <- n2 - i
done;
(* loop over w1 *)
for i = n1-1 downto 0 do
invariant { length t = n2+1
and forall j:int. 0 <= j <= n2 -> min_suffix w1 w2 (i+1) j t[j] }
o := t[n2];
set t n2 (t[n2] + 1);
t[n2] <- t[n2] + 1;
(* loop over w2 *)
for j = n2-1 downto 0 do
invariant { length t = n2+1
......@@ -101,9 +101,9 @@ module Distance
let temp = !o in
o := t[j];
if w1[i] = w2[j] then
set t j temp
t[j] <- temp
else
set t j ((min t[j] t[j+1]) + 1)
t[j] <- (min t[j] t[j+1]) + 1
end
done
done;
......
......@@ -16,12 +16,12 @@ module Flag
{ 0 <= i < length a and 0 <= j < length a }
let v = a[i] in
begin
set a i a[j];
set a j v
a[i] <- a[j];
a[j] <- v
end
{ exchange a (old a) i j }
let dutch_flag (a:array color) (n:int) =
let dutch_flag (a:array color) (n:int) =
{ 0 <= n and length a = n }
let b = ref 0 in
let i = ref 0 in
......@@ -29,8 +29,8 @@ module Flag
label Init:
while !i < !r do
invariant { 0 <= b <= i and i <= r <= n and
monochrome a 0 b Blue and
monochrome a b i White and
monochrome a 0 b Blue and
monochrome a b i White and
monochrome a r n Red and
length a = n and
permut_sub a (at a Init) 0 (n-1) }
......@@ -47,16 +47,16 @@ module Flag
swap a !r !i
end
done
{ (exists b:int. exists r:int.
monochrome a 0 b Blue and
monochrome a b r White and
{ (exists b:int. exists r:int.
monochrome a 0 b Blue and
monochrome a b r White and
monochrome a r n Red)
and permut_sub a (old a) 0 (n-1) }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/flag.gui"
End:
End:
*)
......@@ -11,22 +11,22 @@ module Muller
let compact (a : array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
for i = 0 to length a - 1 do
invariant { 0 <= count = num_of a.elts 0 i <= i}
if a[i] <> 0 then incr count
done;
let u = make !count 0 in
count := 0;
for i = 0 to length a - 1 do
invariant { 0 <= count = num_of a.elts 0 i <= i and
invariant { 0 <= count = num_of a.elts 0 i <= i and
length u = num_of a.elts 0 (length a) }
if a[i] <> 0 then begin set u !count a[i]; incr count end
if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
done
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/muller.gui"
End:
End:
*)
......@@ -92,13 +92,13 @@ let search_safety () =
invariant { length x = m }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
set x d c;
x[d] <- c;
let k = div delta 9 in
for i = 0 to d - 1 do
invariant { length x = m }
if i < k then set x i 9
else if i = k then set x i (mod delta 9)
else set x i 0
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0
done;
raise Success
end
......@@ -132,7 +132,7 @@ let search () =
invariant { x = at x Init }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
set x d c;
x[d] <- c;
assert { sum x.elts d m = y - delta };
let k = div delta 9 in
assert { k <= d };
......@@ -140,9 +140,9 @@ let search () =
invariant { length x = m and is_integer x.elts and
sum x.elts d m = y - delta and
sum x.elts 0 i = if i <= k then 9*i else delta }
if i < k then set x i 9
else if i = k then set x i (mod delta 9)
else set x i 0
if i < k then x[i] <- 9
else if i = k then x[i] <- (mod delta 9)
else x[i] <- 0
done;
(* assume { sum !x 0 d = delta }; *)
assert { sum x.elts 0 d = delta };
......@@ -264,7 +264,7 @@ let search_smallest () =
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
assert { smallest_size delta <= d };
set x d c;
x[d] <- c;
assert { sum x.elts d m = y - delta };
assert { gt_digit x.elts (at x.elts Init) d };
let k = div delta 9 in
......@@ -278,9 +278,9 @@ let search_smallest () =
(j < smallest_size delta -> x[j] = M.get (smallest delta) j) and
(j >= smallest_size delta -> x[j] = 0)) and
gt_digit x.elts (at x.elts Init) d }
if i < k then set x i 9
else if i = k then set x i (mod delta 9)
else set x i 0;
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0;
assert { is_integer x.elts }
done;
assert { sum x.elts 0 d = delta };
......
(* Sorting an array using quicksort, with partitioning a la Bentley.
(* Sorting an array using quicksort, with partitioning a la Bentley.
We simply scan the segment l..r from left ro right, maintaining values
smaller than t[l] on the left part of it (in l+1..m).
......@@ -17,15 +17,13 @@ module Quicksort
let swap (t:array int) (i:int) (j:int) =
{ 0 <= i < length t and 0 <= j < length t }
let v = t[i] in
begin
set t i t[j];
set t j v
end
t[i] <- t[j];
t[j] <- v
{ exchange t (old t) i j }
let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l } =
{ 0 <= l and r < length t }
if l < r then begin
if l < r then begin
let v = t[l] in
let m = ref l in
label L: begin
......@@ -44,15 +42,15 @@ module Quicksort
(l > r and array_eq t (old t)) }
let quicksort (t : array int) =
{}
{}
quick_rec t 0 (length t - 1)
{ sorted t and permut t (old t) }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/quicksort.gui"
End:
End:
*)
......@@ -82,16 +82,6 @@ back +-+-+-+-------------------+
forall i : int. 0 <= i < a.card ->
a.idx[i] = dirichlet a.card a.back i && is_elt a i
(*
parameter create :
sz:int ->
{ 0 <= sz <= maxlen }
sparse_array
{ invariant_ result and
result.card = 0 and
length result = sz and forall i:int. model result i = default }
*)
parameter malloc : n:int -> {} array 'a { A.length result = n }
let create sz =
......@@ -124,11 +114,11 @@ back +-+-+-+-------------------+
let idx = idx a in
let back = back a in
let n = card a in
set val i v;
val[i] <- v;
if not (test a i) then begin
assert { n < length a };
set idx i n;
set back n i;
idx[i] <- n;
back[n] <- i;
() (*TODO a.card <- n+1 *)
end
{ invariant_ a and
......
......@@ -2,17 +2,17 @@ module M
use import int.Int
use import module ref.Ref
use import module array.Array as A
use import module array.Array
type uf = {| link : array int;
dist : array int; (* distance to representative *)
num : int; (* number of classes *) |}
logic size (u: uf) : int = A.length u.link
logic size (u: uf) : int = length u.link
logic inv (u : uf) =
let s = A.length u.link in
A.length u.dist = s and
let s = length u.link in
length u.dist = s and
(forall i:int. 0 <= i < s -> 0 <= u.link[i] < s) and
(forall i:int. 0 <= i < s ->
( (u.dist[i] = 0 and u.link[i] = i)
......@@ -46,20 +46,20 @@ module M
let create (n:int) =
{ 0 <= n }
let l = A.make n 0 in
let l = make n 0 in
for i = 0 to n-1 do
invariant { forall j:int. 0 <= j < i -> l[j] = j }
A.set l i i
l[i] <- i
done;
{| link = l; dist = A.make n 0; num = n |}
{| link = l; dist = make n 0; num = n |}
{ inv result and
num result = n and size result = n and
forall x:int. 0 <= x < n -> repr result x x }
let path_compression (u: uf) x r =
{ inv u and 0 <= x < size u and u.dist[x] > 0 and repr u x r }
A.set (link u) x r;
A.set (dist u) x 1
u.link[x] <- r;
u.dist[x] <- 1
{ inv u and size u = size (old u) and
num u = num (old u) and same_reprs (old u) u }
......
......@@ -25,7 +25,7 @@ module M
for i = 0 to n-1 do
invariant
{ length b = n and forall j: int. 0 <= j < i -> b[a[j]] = j }
set b a[i] i
b[a[i]] <- i
done
{ injective b n }
......
......@@ -84,7 +84,7 @@ module M
length board = n and eq_board board (at board Init) pos and
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
set board pos i;
board[pos] <- i;
assert { eq_board board (at board Init) pos };
if check_is_consistent board pos then bt_queens board n (pos+1)
done
......
......@@ -24,7 +24,7 @@ module M
j := !j - 1;
t := !t + 1
done;
set b !j a[i];
b[!j] <- a[i];
j := !j + 1
done;
assert { 0 <= t <= n }
......
......@@ -15,7 +15,7 @@ module Array
parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter set : a:array 'a -> i:int -> v:'a ->
parameter ([]<-) : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
(* unsafe get/set operations with no precondition *)
......
......@@ -180,14 +180,14 @@
/* program keywords */
%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 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
/* symbols */
%token ARROW
%token ARROW
%token BACKQUOTE BAR
%token COLON COMMA
%token DOT EQUAL FUNC LAMBDA LTGT
......@@ -428,7 +428,7 @@ list1_record_field:
;
record_field:
| opt_mutable lident labels COLON primitive_type
| opt_mutable lident labels COLON primitive_type
{ floc (), $1, add_lab $2 $3, $5 }
;
......@@ -1029,7 +1029,19 @@ expr:
{ let t = mk_infix $1 "=" $3 in
mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [t]) }
| expr LARROW expr
{ mk_infix $1 "<-" $3 }
{ match $1.expr_desc with
| Eapply (e11, e12) -> begin match e11.expr_desc with
| Eident x ->
mk_expr (Eassign (e12, x, $3))
| Eapply ({ expr_desc = Eident (Qident x) }, e11)
when x.id = mixfix "[]" ->
mk_mixfix3 "[]<-" e11 e12 $3
| _ ->
raise Parsing.Parse_error
end
| _ ->
raise Parsing.Parse_error
}
| expr OP1 expr
{ mk_infix $1 $2 $3 }
| expr OP2 expr
......
......@@ -211,6 +211,7 @@ and expr_desc =
| Eletrec of (ident * binder list * variant option * triple) list * expr
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eassign of expr * qualid * expr
(* control *)
| Esequence of expr * expr
| Eif of expr * expr * expr
......