1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
logic m,n,p : int
type matrix
logic get : matrix, int, int -> int
parameter c : matrix ref
logic ab : int,int -> int
let test () =
{ 0 < m and 0 < n and 0 < p }
let i = ref 0 in
while !i < m do
{ invariant i <= m and
forall i',j':int.
0 <= i' < i -> 0 <= j' < p -> get(c,i',j') = ab(i',j') }
L2:
let j = ref 0 in
while !j < p do
{ invariant 0 <= j <= p and
(forall j':int. 0 <= j' < j -> get(c,i,j') = ab(i,j')) and
(forall i',j':int. 0 <= i' < i -> 0 <= j' < p
-> get(c,i',j') = get(c@L2,i',j')) }
[ {} unit writes c
{ get(c,i,j) = ab(i,j) and
(forall j':int. 0 <= j' < j -> get(c,i,j') = ab(i,j')) and
(forall i',j':int. 0 <= i' < i -> 0 <= j' < p -> get(c,i',j') = ab(i',j')) }
];
j := !j + 1
done;
i := !i + 1
done
{ forall i',j':int. 0 <= i' < m -> 0 <= j' < p -> get(c,i',j') = ab(i',j') }
|
