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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
(* ########################################################################## *)
(* Definitions of matrices *)
(* Frdric Gava (Universit Paris 12) *)
(* ########################################################################## *)
(* ************************** *)
(* Definition of the matrices *)
(* ************************** *)
type 'a fmatrice
(* ****************************** *)
(* access and update of a matrice *)
(* ****************************** *)
logic mat_access : 'a fmatrice, int,int -> 'a
logic mat_update : 'a fmatrice, int,int,'a -> 'a fmatrice
(* *************** *)
(* axiom of update *)
(* *************** *)
axiom mat_access_update :
forall m : 'a fmatrice. forall i : int. forall j : int. forall v : 'a.
mat_access(mat_update(m,i,j,v), i,j) = v
axiom access_update_neq :
forall m : 'a fmatrice. forall i1 : int. forall j1 : int.
forall i2 : int. forall j2 : int.
forall v : 'a.
(i1 <> i2) or (j1<>j2) -> mat_access(mat_update(m,i1,j1,v),i2,j2) = mat_access(m,i2,j2)
(* ********************** *)
(* size of row and column *)
(* ********************** *)
logic mat_size_row : 'a fmatrice -> int
logic mat_size_column : 'a fmatrice -> int
(* ************************************ *)
(* effective size of the row and column *)
(* ************************************ *)
parameter mat_size_row_ :
m:'a fmatrice ref -> {} int reads m { result=mat_size_row(m) }
parameter mat_size_column_ :
m:'a fmatrice ref -> {} int reads m { result=mat_size_column(m) }
(* *************************** *)
(* effective access and update *)
(* *************************** *)
parameter mat_get :
m:'a fmatrice ref -> i:int -> j:int ->
{ 0 <= i < mat_size_row(m)
and 0 <= j < mat_size_column(m)} 'a reads m { result = mat_access(m,i,j) }
parameter mat_set :
m:'a fmatrice ref -> i:int -> j:int -> v:'a ->
{ 0 <= i < mat_size_row(m)
and 0 <= j < mat_size_column(m) } unit writes m { m = mat_update(m@,i,j,v) }
(* *********************************** *)
(* axioms on row and column and update *)
(* *********************************** *)
axiom mat_size_row_update :
forall m:'a fmatrice. forall i:int. forall j:int. forall v:'a.
mat_size_row(mat_update(m,i,j,v)) = mat_size_row(m)
axiom mat_size_column_update :
forall m:'a fmatrice. forall i:int. forall j:int. forall v:'a.
mat_size_column(mat_update(m,i,j,v)) = mat_size_column(m)
(* ########################################################################## *)
(* Multiplication of square matrices C=A*B *)
(* ########################################################################## *)
(* ******************** *)
(* size of the matrices *)
(* ******************** *)
logic N : int
axiom N_range : 1 <= N
(* ****************** *)
(* Usefull Predicates *)
(* ****************** *)
(* sigma_mat_mult A B mini maxi i j === sigma_{r=mini}^{maxi} A[i,r]*B[r,j] *)
logic sigma_mat_mult : real fmatrice,real fmatrice,int,int,int,int -> real
axiom sigma_mat_mult_def_1 :
forall A,B:real fmatrice. forall mini,maxi,i,j:int.
maxi > mini -> sigma_mat_mult(A,B,mini,maxi,i,j) = 0.
axiom sigma_mat_mult_def_2 :
forall A,B:real fmatrice. forall mini,maxi,i,j:int.
mini < maxi ->
sigma_mat_mult(A,B,mini,maxi,i,j) =
sigma_mat_mult(A,B,mini,maxi-1,i,j) +
mat_access(A,i,maxi) * mat_access(B,maxi,j)
(* Part of C that have been completly calulated *)
predicate mat_mult_done(A:real fmatrice, B:real fmatrice,C:real fmatrice,iu:int,id:int,jl:int,jr:int) =
forall i,j:int. (iu<=i<id and jl<=j<jr) -> mat_access(C,i,j)=sigma_mat_mult(A,B,0,N-1,i,j)
(* Part of C that need to be calculated *)
predicate mat_mult_todo(C:real fmatrice,C':real fmatrice,iu:int,id:int,jl:int,jr:int) =
forall i,j:int. (iu<=i<id and jl<=j<jr) -> mat_access(C,i,j)=mat_access(C',i,j)
(* C=A*B *)
predicate mat_mult(A:real fmatrice, B:real fmatrice,C:real fmatrice) =
mat_mult_done(A,B,C,0,N,0,N)
(* ******************************** *)
(* Definition of the multiplication *)
(* ******************************** *)
let mult (A : real fmatrice ref)
(B : real fmatrice ref)
(C : real fmatrice ref) =
{
mat_size_row(A) = N
and mat_size_row(B) = N
and mat_size_row(C) = N
and mat_size_column(A) = N
and mat_size_column(B) = N
and mat_size_column(C) = N
and (forall x,y:int. 0<=x<N and 0<=y<N -> mat_access(C,x,y)=0.)
}
init:
let i=ref 0 in
while !i<N do
{ invariant
0<=i<=N
and mat_mult_done(A,B,C,0,i,0,N)
and mat_mult_todo(C,C@init,i,N,0,N)
and (mat_size_column(C) = mat_size_column(C@init))
and (mat_size_row(C) = mat_size_row(C@init))
variant N-i}
let j=ref 0 in
begin
while !j<N do
{ invariant
0<=j<=N
and mat_mult_done(A,B,C,0,i,0,N)
and mat_mult_todo(C,C@init,i+1,N,0,N)
and mat_mult_done(A,B,C,i,i+1,0,j)
and mat_mult_todo(C,C@init,i,i+1,j,N)
and (mat_size_column(C) = mat_size_column(C@init))
and (mat_size_row(C) = mat_size_row(C@init))
variant N-j }
let r=ref 0 in
while !r<N do
{ invariant
0<=r<=N
and mat_mult_done(A,B,C,0,i,0,N)
and mat_mult_todo(C,C@init,i+1,N,0,N)
and mat_mult_done(A,B,C,i,i+1,0,j)
and mat_mult_todo(C,C@init,i,i+1,j+1,N)
and (mat_access(C,i,j)=mat_access(C@init,i,j)+sigma_mat_mult(A,B,0,r-1,i,j))
and (mat_size_column(C) = mat_size_column(C@init))
and (mat_size_row(C) = mat_size_row(C@init))
variant N-r}
mat_set C !i !j ((mat_get C !i !j) + ((mat_get A !i !r) * (mat_get B !r !j)));
r:=!r+1
done;
j:=!j+1
done
end;
i:=!i+1
done
{ mat_mult(A,B,C) }
|
