program examples now all updated

parent 5f6e63a2
......@@ -82,6 +82,7 @@ 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 }
......@@ -89,16 +90,16 @@ back +-+-+-+-------------------+
{ 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 =
{ 0 <= sz <= maxlen }
Mk_sparse_array (malloc sz) (malloc sz) (malloc sz) 0
{| val = malloc sz; idx = malloc sz; back = malloc sz; card = 0 |}
{ invariant_ result and
sa_sz result = sz and forall i:int. model result i = default }
*)
result.card = 0 and
length result = sz and forall i:int. model result i = default }
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
......
......@@ -48,26 +48,24 @@ module M
{ 0 <= n }
let l = A.make n 0 in
for i = 0 to n-1 do
invariant { forall j:int. 0 <= j < i -> u.link[j] = j }
invariant { forall j:int. 0 <= j < i -> l[j] = j }
A.set l i i
done;
mk_uf l (A.make n 0) n
{| link = l; dist = A.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 : ref uf) x r =
{ inv u and 0 <= x < size u and dist u # x > 0 and repr u x r }
let UF l d s n = !u in
let l = A.set l x r in
let d = A.set d x 1 in
u := UF l d s n
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
{ inv u and size u = size (old u) and
num u = num (old u) and same_reprs (old u) u }
let rec find (u:ref uf) (x:int) variant { dist u # x } =
let rec find (u: uf) (x: int) variant { u.dist[x] } =
{ inv u and 0 <= x < size u }
let y = A.get (link !u) x in
let y = (link u)[x] in
if y <> x then begin
let r = find u y in
path_compression u x r;
......
......@@ -6,33 +6,33 @@ module M
use import int.Int
use import module array.Array
logic injective (a : t int int) (n : int) =
forall i j : int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic injective (a: array int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic surjective (a : t int int) (n : int) =
forall i : int [i]. 0 <= i < n -> exists j : int. (0 <= j < n and a[j] = i)
logic surjective (a: array int) (n: int) =
forall i: int [i]. 0 <= i < n -> exists j: int. (0 <= j < n and a[j] = i)
logic range (a : t int int) (n : int) =
forall i : int. 0 <= i < n -> 0 <= a[i] < n
logic range (a: array int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
lemma Injective_surjective :
forall a : t int int, n : int.
lemma Injective_surjective:
forall a: array int, n: int.
injective a n -> range a n -> surjective a n
let inverting (a : array int) (b : array int) n =
{ n >= 0 and length a = n and length b = n and
let inverting (a: array int) (b: array int) n =
{ n >= 0 and length a = n and length b = n and
injective a n and range a n }
for i = 0 to n-1 do
invariant
{ length b = n and forall j : int. 0 <= j < i -> b[a[j]] = j }
b[a[i] <- i]
invariant
{ length b = n and forall j: int. 0 <= j < i -> b[a[j]] = j }
set b a[i] i
done
{ injective b n }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_inverting.gui"
End:
End:
*)
......@@ -7,7 +7,7 @@ module M
use import module ref.Ref
use import module array.Array
let max_sum a n =
let max_sum (a: array int) (n: int) =
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in
let max = ref 0 in
......@@ -22,7 +22,7 @@ module M
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_max_sum.gui"
End:
End:
*)
......@@ -6,45 +6,47 @@ module M
use import int.Int
use import module array.Array
logic eq_board (b1 b2 : map int) (pos : int) =
logic eq_board (b1 b2: array int) (pos: int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]
lemma eq_board_set :
forall b : map int, pos q i : int.
(*
lemma eq_board_set:
forall b: array int, pos q i: int.
pos <= q -> eq_board b b[q <- i] pos
*)
lemma eq_board_sym :
forall b1 b2 : map int, pos : int.
lemma eq_board_sym:
forall b1 b2: array int, pos: int.
eq_board b1 b2 pos -> eq_board b2 b1 pos
lemma eq_board_trans :
forall b1 b2 b3 : map int, pos : int.
lemma eq_board_trans:
forall b1 b2 b3: array int, pos: int.
eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos
lemma eq_board_extension :
forall b1 b2 : map int, pos : int.
lemma eq_board_extension:
forall b1 b2: array int, pos: int.
eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1)
logic consistent_row (board : map int) (pos : int) (q : int) =
logic consistent_row (board: array int) (pos: int) (q: int) =
board[q] <> board[pos] and
board[q] - board[pos] <> pos - q and
board[pos] - board[q] <> pos - q
lemma consistent_row_eq :
forall b1 b2 : map int, pos : int.
eq_board b1 b2 (pos+1) -> forall q : int. 0 <= q < pos ->
lemma consistent_row_eq:
forall b1 b2: array int, pos: int.
eq_board b1 b2 (pos+1) -> forall q: int. 0 <= q < pos ->
consistent_row b1 pos q -> consistent_row b2 pos q
logic is_consistent (board : map int) (pos : int) =
logic is_consistent (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q
lemma is_consistent_eq :
forall b1 b2 : map int, pos : int.
lemma is_consistent_eq:
forall b1 b2: array int, pos: int.
eq_board b1 b2 (pos+1) -> is_consistent b1 pos -> is_consistent b2 pos
exception Inconsistent int
let check_is_consistent (board : array int) pos =
let check_is_consistent (board: array int) pos =
{ 0 <= pos < length board }
try
for q = 0 to pos-1 do
......@@ -62,50 +64,50 @@ module M
end
{ result=True <-> is_consistent board pos }
logic is_board (board : map int) (pos : int) =
logic is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
logic solution (board : map int) (pos : int) =
logic solution (board: array int) (pos: int) =
is_board board pos and
forall q:int. 0 <= q < pos -> is_consistent board q
lemma solution_eq_board :
forall b1 b2 : map int, pos : int. length b1 = length b2 ->
lemma solution_eq_board:
forall b1 b2: array int, pos: int. length b1 = length b2 ->
eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos
exception Solution
let rec bt_queens (board : array int) n pos variant { n - pos } =
let rec bt_queens (board: array int) n pos variant { n - pos } =
{ length board = n and 0 <= pos <= n and solution board pos }
label Init:
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
invariant {
length board = n and eq_board board (at board Init) pos and
forall b:map int. length b = n -> is_board b n ->
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos <- i];
set 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
{ (* no solution *)
{ (* no solution *)
length board = n and eq_board board (old board) pos and
forall b:map int. length b = n -> is_board b n ->
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> not (solution b n) }
| Solution ->
| Solution ->
{ (* a solution *)
solution board n }
let queens (board : array int) n =
let queens (board: array int) n =
{ length board = n }
bt_queens board n 0
{ forall b:map int. length b = n -> is_board b n -> not (solution b n) }
{ forall b:array int. length b = n -> is_board b n -> not (solution b n) }
| Solution -> { solution board n }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_queens.gui"
End:
End:
*)
module M
(* WCET example
(* WCET example
This double loop program is actually O(n).
We show it by introducing a variable t which counts the number of times
......@@ -9,34 +9,30 @@ module M
use import int.Int
use import module ref.Ref
use array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
use import module array.Array
logic n : int
axiom N_non_negative : n >= 0
let hull a b =
let j = ref 0 in
let t = ref 0 in (* WCET *)
for i = 0 to n-1 do
invariant { 0 <= j <= i <= n and i = j + t }
while !j > 0 && !b#(!j-1) > a#(i) do
invariant { 0 <= j <= i and i = j + t } variant { j }
j := !j - 1;
t := !t + 1
let hull (a: array int) (b: array int) =
let j = ref 0 in
let t = ref 0 in (* WCET *)
for i = 0 to n-1 do
invariant { 0 <= j <= i <= n and i = j + t }
while !j > 0 && b[!j-1] > a[i] do
invariant { 0 <= j <= i and i = j + t } variant { j }
j := !j - 1;
t := !t + 1
done;
set b !j a[i];
j := !j + 1
done;
b := A.set !b !j (a#i);
j := !j + 1
done;
assert { 0 <= t <= n }
assert { 0 <= t <= n }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/wcet_hull.gui"
End:
End:
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment