blocking_semantics4.mlw 29.4 KB
Newer Older
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
1
2
3
4
5
6
7
8
9
10
11

(** {1 A certified WP calculus} *)

(** {2 A simple imperative language with expressions, syntax and semantics} *)

theory ImpExpr

use import int.Int
use import int.MinMax
use import bool.Bool
use export list.List
atafat's avatar
atafat committed
12
use export list.Append
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
use map.Map as IdMap

(** types and values *)

type datatype = TYunit | TYint | TYbool
type value = Vvoid | Vint int | Vbool bool

(** terms and formulas *)

type operator = Oplus | Ominus | Omult | Ole

(** ident for mutable variables *)
type mident

atafat's avatar
atafat committed
27

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
28
29
30
31
axiom mident_decide :
  forall m1 m2: mident. m1 = m2 \/ m1 <> m2

(** ident for immutable variables *)
32
type ident = { ident_index : int }
Andrei Paskevich's avatar
Andrei Paskevich committed
33

atafat's avatar
atafat committed
34
35
36
37
constant result : ident

axiom ident_decide :
  forall m1 m2: ident. m1 = m2 \/ m1 <> m2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
38
39

(** Terms *)
atafat's avatar
atafat committed
40
type term =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
41
42
43
44
45
46
47
48
  | Tvalue value
  | Tvar ident
  | Tderef mident
  | Tbin term operator term


predicate var_occurs_in_term (x:ident) (t:term) =
  match t with
atafat's avatar
atafat committed
49
50
51
52
  | Tvalue _  -> false
  |  Tvar i  -> x=i
  |  Tderef _  -> false
  |  Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
53
54
  end

Asma Tafat's avatar
Asma Tafat committed
55
56
57
58
59
60
61
62
(* predicate mvar_occurs_in_term (x:mident) (t:term) = *)
(*   match t with *)
(*   | Tvalue _  -> false *)
(*   |  Tvar i  -> x = i *)
(*   |  Tderef _  -> false *)
(*   |  Tbin t1 _ t2 -> mvar_occurs_in_term x t1 \/ mvar_occurs_in_term x t2 *)
(*   end *)

atafat's avatar
atafat committed
63
64
(* predicate term_inv (t:term) = *)
(*   forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
65
66

function mk_tvalue (v:value) : term =
atafat's avatar
atafat committed
67
   Tvalue v
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
68
69

function mk_tvar (i:ident) : term =
atafat's avatar
atafat committed
70
   Tvar i
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
71
72

function mk_tderef (r:mident) : term =
atafat's avatar
atafat committed
73
   Tderef r
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
74
75

function mk_tbin (t1:term) (o:operator) (t2:term) : term =
atafat's avatar
atafat committed
76
    Tbin t1 o t2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
77
78
79
80
81
82
83
84
85
86

(** Formulas *)
type fmla =
  | Fterm term
  | Fand fmla fmla
  | Fnot fmla
  | Fimplies fmla fmla
  | Flet ident term fmla         (* let id = term in fmla *)
  | Fforall ident datatype fmla  (* forall id : ty, fmla *)

atafat's avatar
atafat committed
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
(** Expressions *)
type expr =
  | Evalue value
  | Ebin expr operator expr
  | Evar ident
  | Ederef mident
  | Eassign mident expr
  | Eseq expr expr
  | Elet ident expr expr
  | Eif expr expr expr
  | Eassert fmla
  | Ewhile expr fmla expr  (* while cond invariant inv body *)

function mk_evalue (v:value) : expr =
   Evalue v
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
102

atafat's avatar
atafat committed
103
104
105
106
107
108
109
110
111
112
113
function mk_evar (i:ident) : expr =
   Evar i

function mk_ederef (r:mident) : expr =
   Ederef r

function mk_ebin (e1:expr) (o:operator) (e2:expr) : expr =
    Ebin e1 o e2

(* lemma decide_is_skip: *)
(*   forall s:stmt. s = Sskip \/ s <> Sskip *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

(** Typing *)

function type_value (v:value) : datatype =
    match v with
      | Vvoid  -> TYunit
      | Vint int ->  TYint
      | Vbool bool -> TYbool
end

inductive type_operator (op:operator) (ty1 ty2 ty: datatype) =
      | Type_plus : type_operator Oplus TYint TYint TYint
      | Type_minus : type_operator Ominus TYint TYint TYint
      | Type_mult : type_operator Omult TYint TYint TYint
      | Type_le : type_operator Ole TYint TYint TYbool

type type_stack = list (ident, datatype)  (* map local immutable variables to their type *)
function get_vartype (i:ident) (pi:type_stack) : datatype =
  match pi with
  | Nil -> TYunit
  | Cons (x,ty) r -> if x=i then ty else get_vartype i r
  end

Andrei Paskevich's avatar
Andrei Paskevich committed
137

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
138
139
140
141
142
type type_env = IdMap.map mident datatype  (* map global mutable variables to their type *)
function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i

inductive type_term type_env type_stack term datatype =
  | Type_value :
atafat's avatar
atafat committed
143
144
      forall sigma: type_env, pi:type_stack, v:value.
	type_term sigma pi  (Tvalue v) (type_value v)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
145
  | Type_var :
atafat's avatar
atafat committed
146
      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
147
        (get_vartype v pi = ty) ->
atafat's avatar
atafat committed
148
        type_term sigma pi (Tvar v) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
149
  | Type_deref :
atafat's avatar
atafat committed
150
      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
151
        (get_reftype v sigma = ty) ->
atafat's avatar
atafat committed
152
        type_term sigma pi (Tderef v) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
153
154
  | Type_bin :
      forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator,
atafat's avatar
atafat committed
155
        ty1 ty2 ty:datatype.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
156
157
158
        type_term sigma pi t1 ty1 ->
	type_term sigma pi t2 ty2 ->
	type_operator op ty1 ty2 ty ->
atafat's avatar
atafat committed
159
        type_term sigma pi (Tbin t1 op t2) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
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
187
188
189
190
191
192
193
194
195
196
197

inductive type_fmla type_env type_stack fmla =
  | Type_term :
      forall sigma: type_env, pi:type_stack, t:term.
	type_term sigma pi t TYbool ->
	type_fmla sigma pi (Fterm t)
  | Type_conj :
      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
	type_fmla sigma pi f1 ->
        type_fmla sigma pi f2 ->
        type_fmla sigma pi (Fand f1 f2)
  | Type_neg :
      forall sigma: type_env, pi:type_stack, f:fmla.
	type_fmla sigma pi f ->
        type_fmla sigma pi (Fnot f)
  | Type_implies :
      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
	type_fmla sigma pi f1 ->
        type_fmla sigma pi f2 ->
        type_fmla sigma pi (Fimplies f1 f2)
  | Type_let :
      forall sigma: type_env, pi:type_stack, x:ident, t:term, f:fmla, ty:datatype.
	type_term sigma pi t ty ->
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Flet x t f)
  | Type_forall1 :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYint) pi) f ->
  	type_fmla sigma pi (Fforall x TYint f)
  | Type_forall2 :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYbool) pi) f ->
  	type_fmla sigma pi (Fforall x TYbool f)
  | Type_forall3:
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYunit) pi) f ->
  	type_fmla sigma pi (Fforall x TYunit f)

atafat's avatar
atafat committed
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
inductive type_expr type_env type_stack expr datatype =
  | Type_Evalue :
      forall sigma: type_env, pi:type_stack, v:value.
	type_expr sigma pi (Evalue v) (type_value v)
  | Type_Evar :
      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
        (get_vartype v pi = ty) -> type_expr sigma pi (Evar v) ty
  | Type_Ederef :
      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
        (get_reftype v sigma = ty) -> type_expr sigma pi (Ederef v) ty
  | Type_Ebinop :
      forall sigma: type_env, pi:type_stack, e1 e2 : expr, op:operator, ty1 ty2 ty:datatype.
        type_expr sigma pi e1 ty1 ->
        type_expr sigma pi e2 ty2 ->
        type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
213
  | Type_seq :
atafat's avatar
atafat committed
214
      forall sigma: type_env, pi:type_stack, e1 e2:expr, ty:datatype.
atafat's avatar
atafat committed
215
216
217
        type_expr sigma pi e1 TYunit ->
	type_expr sigma pi e2 ty ->
	type_expr sigma pi (Eseq e1 e2) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
218
  | Type_assigns :
atafat's avatar
atafat committed
219
      forall sigma: type_env, pi:type_stack, x:mident, e:expr, ty:datatype.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
220
	(get_reftype x sigma = ty) ->
atafat's avatar
atafat committed
221
222
        type_expr sigma pi e ty ->
        type_expr sigma pi (Eassign x e) TYunit
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
223
  | Type_if :
atafat's avatar
atafat committed
224
225
226
227
228
      forall sigma: type_env, pi:type_stack, t e1 e2:expr, ty:datatype.
	type_expr sigma pi t TYbool ->
	type_expr sigma pi e1 ty ->
	type_expr sigma pi e2 ty ->
    	type_expr sigma pi (Eif t e1 e2) ty
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
229
230
231
  | Type_assert :
      forall sigma: type_env, pi:type_stack, p:fmla.
	type_fmla sigma pi p ->
atafat's avatar
atafat committed
232
    	type_expr sigma pi (Eassert p) TYbool
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
233
  | Type_while :
atafat's avatar
atafat committed
234
      forall sigma: type_env, pi:type_stack, guard:expr, body:expr, inv:fmla, ty:datatype.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
235
	type_fmla sigma pi inv ->
atafat's avatar
atafat committed
236
237
238
239
240
241
242
243
        type_expr sigma pi guard TYbool ->
        type_expr sigma pi body ty ->
        type_expr sigma pi (Ewhile guard inv body) ty
  | Type_Elet :
      forall sigma: type_env, pi:type_stack, x:ident, e1 e2:expr, ty1 ty2 :datatype.
	type_expr sigma pi e1 ty1 ->
        type_expr sigma (Cons (x,ty1) pi) e2 ty2 ->
	type_expr sigma pi (Elet x e1 e2) ty2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279

(** Operational semantic *)
type env = IdMap.map mident value  (* map global mutable variables to their value *)
function get_env (i:mident) (e:env) : value = IdMap.get e i

type stack = list (ident, value)  (* map local immutable variables to their value *)
function get_stack (i:ident) (pi:stack) : value =
  match pi with
  | Nil -> Vvoid
  | Cons (x,v) r -> if x=i then v else get_stack i r
  end

lemma get_stack_eq:
  forall x:ident, v:value, r:stack.
    get_stack x (Cons (x,v) r) = v

lemma get_stack_neq:
  forall x i:ident, v:value, r:stack.
    x <> i -> get_stack i (Cons (x,v) r) = get_stack i r

(** semantics of formulas *)

function eval_bin (x:value) (op:operator) (y:value) : value =
  match x,y with
  | Vint x,Vint y ->
     match op with
     | Oplus -> Vint (x+y)
     | Ominus -> Vint (x-y)
     | Omult -> Vint (x*y)
     | Ole -> Vbool (if x <= y then True else False)
     end
  | _,_ -> Vvoid
  end

function eval_term (sigma:env) (pi:stack) (t:term) : value =
  match t with
atafat's avatar
atafat committed
280
281
282
283
  | Tvalue v -> v
  |  Tvar id  -> get_stack id pi
  |  Tderef id  -> get_env id sigma
  |  Tbin t1 op t2  ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
284
     eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
atafat's avatar
atafat committed
285
end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309


lemma eval_bool_term:
  forall sigma:env, pi:stack, sigmat:type_env, pit:type_stack, t:term.
    type_term sigmat pit t TYbool ->
    (* TODO: compatibility sigma, sigmat and pi,pit *)
    exists b:bool.
      eval_term sigma pi t = Vbool b

predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
  match f with
  | Fterm t -> eval_term sigma pi t = Vbool True
  | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
  | Fnot f -> not (eval_fmla sigma pi f)
  | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
  | Flet x t f ->
      eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
  | Fforall x TYint f ->
     forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
  | Fforall x TYbool f ->
     forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
  | Fforall x TYunit f ->  eval_fmla sigma (Cons (x,Vvoid) pi) f
  end

310

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
(* function eval_expr (sigma:env) (pi:stack) (e:expr) : value = *)
(*   match e with *)
(*   | Evalue v -> v *)
(*   | Evar id  -> get_stack id pi *)
(*   | Ederef id  -> get_env id sigma *)
(*   | Ebin e1 op e2  -> *)
(*      eval_bin (eval_expr sigma pi e1) op (eval_expr sigma pi e2) *)
(*   | Eassign id e1  *)
(*   | Eseq e1 e2  *)
(*   | Elet id e1 e2 -> void *)
(*   | Eif e1 e2 e3 ->  *)
(*     if ((eval_expr sigma pi e1) = (Vbool True))  *)
(*     then eval_expr sigma pi e2 *)
(*     else eval_expr sigma pi e3 *)
(*   | Eassert f -> eval_fmla f *)
(*   | Ewhile expr fmla expr  ->  *)
(* end *)
328

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
329
330
331
332
333
334
(** substitution of a reference [r] by a logic variable [v]
   warning: proper behavior only guaranted if [v] is "fresh",
   i.e index(v) > term_maxvar(t) *)

function msubst_term (t:term) (r:mident) (v:ident) : term =
  match t with
atafat's avatar
atafat committed
335
336
337
  | Tvalue _ | Tvar _  -> t
  | Tderef x -> if r = x then mk_tvar v else t
  | Tbin t1 op t2  ->
Andrei Paskevich's avatar
Andrei Paskevich committed
338
      mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
339
340
341
342
  end

function subst_term (t:term) (r:ident) (v:ident) : term =
  match t with
atafat's avatar
atafat committed
343
344
  | Tvalue _ | Tderef _  -> t
  | Tvar x  ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
345
      if r = x then mk_tvar v else t
atafat's avatar
atafat committed
346
  | Tbin t1 op t2  ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347
348
349
     mk_tbin (subst_term t1 r v) op (subst_term t2 r v)
  end

Asma Tafat's avatar
Asma Tafat committed
350

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
351
352
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (id:ident) (t:term) =
atafat's avatar
atafat committed
353
    not (var_occurs_in_term id t)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
354

Asma Tafat's avatar
Asma Tafat committed
355
356
357
(* predicate mfresh_in_term (id:mident) (t:term) = *)
(*     not (mvar_occurs_in_term id t) *)

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
358
359
360
361
lemma fresh_in_binop:
  forall t t':term, op:operator, v:ident.
    fresh_in_term v (mk_tbin t op t') ->
      fresh_in_term v t  /\ fresh_in_term v t'
Andrei Paskevich's avatar
Andrei Paskevich committed
362

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
(* lemma eval_subst_term: *)
(*   forall sigma:env, pi:stack, e:term, x:ident, v:ident. *)
(*     fresh_in_term v e -> *)
(*     eval_term sigma pi (subst_term e x v) = *)
(*     eval_term sigma (Cons (x, (get_stack v pi)) pi) e *)

predicate fresh_in_fmla (id:ident) (f:fmla) =
  match f with
  | Fterm e -> fresh_in_term id e
  | Fand f1 f2   | Fimplies f1 f2 ->
      fresh_in_fmla id f1 /\ fresh_in_fmla id f2
  | Fnot f -> fresh_in_fmla id f
  | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
  | Fforall y ty f -> id <> y /\ fresh_in_fmla id f
  end

Asma Tafat's avatar
Asma Tafat committed
379
380
381
382
383
384
385
386
387
388
(* predicate mfresh_in_fmla (id:mident) (f:fmla) = *)
(*   match f with *)
(*   | Fterm e -> mfresh_in_term id e *)
(*   | Fand f1 f2   | Fimplies f1 f2 -> *)
(*       mfresh_in_fmla id f1 /\ mfresh_in_fmla id f2 *)
(*   | Fnot f -> mfresh_in_fmla id f *)
(*   | Flet y t f -> id <> y /\ mfresh_in_term id t /\ mfresh_in_fmla id f *)
(*   | Fforall y ty f -> id <> y /\ mfresh_in_fmla id f *)
(* end *)

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
function subst (f:fmla) (x:ident) (v:ident) : fmla =
  match f with
  | Fterm e -> Fterm (subst_term e x v)
  | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
  | Fnot f -> Fnot (subst f x v)
  | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v)
  | Flet y t f -> Flet y (subst_term t x v) (subst f x v)
  | Fforall y ty f -> Fforall y ty (subst f x v)
  end

function msubst (f:fmla) (x:mident) (v:ident) : fmla =
  match f with
  | Fterm e -> Fterm (msubst_term e x v)
  | Fand f1 f2 -> Fand (msubst f1 x v) (msubst f2 x v)
  | Fnot f -> Fnot (msubst f x v)
  | Fimplies f1 f2 -> Fimplies (msubst f1 x v) (msubst f2 x v)
  | Flet y t f -> Flet y (msubst_term t x v) (msubst f x v)
  | Fforall y ty f -> Fforall y ty (msubst f x v)
  end

atafat's avatar
atafat committed
409
410
411
412
lemma subst_fresh_term :
  forall t:term, x:ident, v:ident.
   fresh_in_term x t -> subst_term t x v = t

Asma Tafat's avatar
Asma Tafat committed
413
(*Needed ???*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
414
415
416
417
lemma subst_fresh :
  forall f:fmla, x:ident, v:ident.
   fresh_in_fmla x f -> subst f x v = f

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
418

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
419
420
421
422
423
(* Not needed *)
(* lemma let_subst: *)
(*     forall t:term, f:fmla, x id':ident, id :mident. *)
(*     msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)

atafat's avatar
atafat committed
424
425
426
427
428
429
lemma eval_msubst_term:
  forall e:term, sigma:env, pi:stack, x:mident, v:ident.
    fresh_in_term v e ->
    eval_term sigma pi (msubst_term e x v) =
    eval_term (IdMap.set sigma x (get_stack v pi)) pi e

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
430
431
432
433
434
435
436
437
438
439
440
441
442
443
(* Need it for monotonicity and wp_reduction *)
lemma eval_msubst:
  forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
    fresh_in_fmla v f ->
    (eval_fmla sigma pi (msubst f x v) <->
     eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)

(* lemma eval_subst: *)
(*   forall f:fmla, sigma:env, pi:stack, x:ident, v:ident. *)
(*     fresh_in_fmla v f -> *)
(*     (eval_fmla sigma pi (subst f x v) <-> *)
(*      eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)

lemma eval_swap_term:
atafat's avatar
atafat committed
444
445
446
447
448
449
forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)

lemma eval_swap_term_2:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
450
451
452
453
454
455
  forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
    eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)

lemma eval_swap:
atafat's avatar
atafat committed
456
  forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
457
    id1 <> id2 ->
atafat's avatar
atafat committed
458
459
460
461
462
463
464
    (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
    eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)

lemma eval_swap_2:
  forall f:fmla, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
      forall sigma:env, pi:stack.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
465
466
467
    (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
    eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)

atafat's avatar
atafat committed
468
469
470
471
472
lemma eval_term_change_free :
  forall t:term, sigma:env, pi:stack, id:ident, v:value.
    fresh_in_term id t ->
    eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
473
474
 (* Need it for monotonicity*)
lemma eval_change_free :
atafat's avatar
atafat committed
475
  forall f:fmla, id:ident, v:value.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
476
    fresh_in_fmla id f ->
atafat's avatar
atafat committed
477
      forall sigma:env, pi:stack.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
    (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)

(** [valid_fmla f] is true when [f] is valid in any environment *)
  predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p

(* Not needed *)
(* axiom msubst_implies : *)
(* forall p q:fmla. *)
(*   valid_fmla (Fimplies p q) -> *)
(*   forall sigma:env, pi:stack, x:mident, id:ident. *)
(*     fresh_in_fmla id (Fand p q) ->  *)
(*     eval_fmla sigma (Cons (id, (get_env x sigma)) pi) (Fimplies (msubst p x id) (msubst q x id))  *)

(** let id' = t in f[id <- id'] <=> let id = t in f*)
(* Not needed *)
(* lemma let_equiv : *)
(*   forall id:ident, id':ident, t:term, f:fmla. *)
(*     forall sigma:env, pi:stack. *)
(*       fresh_in_fmla id' f -> *)
(* 	eval_fmla sigma pi (Flet id' t (subst f id id')) *)
(* 	 -> eval_fmla sigma pi (Flet id t f) *)

(* lemma let_implies : *)
(*   forall id:ident, t:term, p q:fmla. *)
(*     valid_fmla (Fimplies p q) -> *)
(*     valid_fmla (Fimplies (Flet id t p) (Flet id t q)) *)

atafat's avatar
atafat committed
505
506
507
508
predicate fresh_in_expr (id:ident) (e:expr) =
  match e with
  | Evalue _ -> true
  | Ebin e1 op e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
Andrei Paskevich's avatar
Andrei Paskevich committed
509
  | Evar v -> id <> v
atafat's avatar
atafat committed
510
511
  | Ederef _ -> true
  | Eassign x e -> fresh_in_expr id e
Andrei Paskevich's avatar
Andrei Paskevich committed
512
  | Eseq e1 e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
atafat's avatar
atafat committed
513
514
515
516
  | Elet v e1 e2 -> id <> v /\ fresh_in_expr id e1 /\ fresh_in_expr id e2
  | Eif e1 e2 e3 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 /\ fresh_in_expr id e3
  | Eassert f -> fresh_in_fmla id f
  | Ewhile cond inv body -> fresh_in_expr id cond /\ fresh_in_fmla id inv /\ fresh_in_expr id body
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
517
518
  end

atafat's avatar
atafat committed
519
constant void : expr = Evalue Vvoid
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
520
521
522

(** small-steps semantics for expressions *)

atafat's avatar
atafat committed
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
inductive one_step env stack expr env stack expr =

  | one_step_var:
      forall sigma:env, pi:stack, v:ident.
        one_step sigma pi (Evar v) sigma pi (Evalue (get_stack v pi))

  | one_step_deref:
      forall sigma:env, pi:stack, v:mident.
        one_step sigma pi (Ederef v) sigma pi (Evalue (get_env v sigma))

  | one_step_bin_ctxt1:
      forall sigma sigma':env, pi pi':stack, op:operator,
        e1 e1' e2:expr.
        one_step sigma pi e1 sigma' pi' e1' ->
          one_step sigma pi (Ebin e1 op e2) sigma' pi' (Ebin e1' op e2)

  | one_step_bin_ctxt2:
      forall sigma sigma':env, pi pi':stack, op:operator, v1:value, e2 e2':expr.
        one_step sigma pi e2 sigma' pi' e2' ->
          one_step sigma pi (Ebin (Evalue v1) op e2) sigma' pi' (Ebin (Evalue v1) op e2')
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
543

atafat's avatar
atafat committed
544
  | one_step_bin_value:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
545
546
      forall sigma :env, pi :stack, op:operator, v1 v2:value.
        one_step sigma pi (Ebin (Evalue v1) op (Evalue v2)) sigma pi (Evalue (eval_bin v1 op v2))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
547

atafat's avatar
atafat committed
548
549
550
551
 | one_step_assign_ctxt:
     forall sigma sigma':env, pi pi':stack, x:mident, e e':expr.
       one_step sigma pi e sigma' pi' e' ->
       one_step sigma pi (Eassign x e) sigma' pi' (Eassign x e')
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
552

atafat's avatar
atafat committed
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
  | one_step_assign_value:
      forall sigma sigma':env, pi:stack, x:mident, v:value.
        sigma' = IdMap.set sigma x v ->
    one_step sigma pi (Eassign x (Evalue v)) sigma' pi void

  | one_step_seq_ctxt:
      forall sigma sigma':env, pi pi':stack, e1 e1' e2:expr.
        one_step sigma pi e1 sigma' pi' e1' ->
          one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1' e2)

  | one_step_seq_value:
      forall sigma:env, pi:stack, e:expr.
        one_step sigma pi (Eseq void e) sigma pi e

  | one_step_let_ctxt:
      forall sigma sigma':env, pi pi':stack, id:ident, e1 e1' e2:expr.
        one_step sigma pi e1 sigma' pi' e1' ->
          one_step sigma pi (Elet id e1 e2) sigma' pi' (Elet id e1' e2)

  | one_step_let_value:
      forall sigma:env, pi:stack, id:ident, v:value, e:expr.
        one_step sigma pi (Elet id (Evalue v) e) sigma (Cons (id,v) pi) e

  | one_step_if_ctxt:
      forall sigma sigma':env, pi pi':stack, e1 e1' e2 e3:expr.
        one_step sigma pi e1 sigma' pi' e1' ->
          one_step sigma pi (Eif e1 e2 e3) sigma' pi' (Eif e1' e2 e3)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
580
581

  | one_step_if_true:
atafat's avatar
atafat committed
582
583
      forall sigma:env, pi:stack, e1 e2:expr.
        one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
584
585

  | one_step_if_false:
atafat's avatar
atafat committed
586
587
      forall sigma:env, pi:stack, e1 e2 :expr.
        one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
588
589
590
591
592

  | one_step_assert:
      forall sigma:env, pi:stack, f:fmla.
        (* blocking semantics *)
        eval_fmla sigma pi f ->
atafat's avatar
atafat committed
593
          one_step sigma pi (Eassert f) sigma pi void
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
594
595

  | one_step_while_true:
atafat's avatar
atafat committed
596
      forall sigma:env, pi:stack, cond body:expr, inv:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
597
598
        (* blocking semantics *)
        eval_fmla sigma pi inv ->
atafat's avatar
atafat committed
599
600
        one_step sigma pi (Ewhile (Evalue (Vbool True)) inv body) sigma pi
        (Eseq body (Ewhile cond inv body))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
601
602

  | one_step_while_false:
atafat's avatar
atafat committed
603
      forall sigma:env, pi:stack, inv:fmla, body:expr.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
604
605
        (* blocking semantics *)
        eval_fmla sigma pi inv ->
atafat's avatar
atafat committed
606
        one_step sigma pi (Ewhile (Evalue (Vbool False)) inv body) sigma pi void
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
607
608
609

 (** many steps of execution *)

atafat's avatar
atafat committed
610
 inductive many_steps env stack expr env stack expr int =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
611
   | many_steps_refl:
atafat's avatar
atafat committed
612
     forall sigma:env, pi:stack, s:expr. many_steps sigma pi s sigma pi s 0
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
613
   | many_steps_trans:
atafat's avatar
atafat committed
614
     forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:expr, n:int.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
615
616
617
       n > 0 -> one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
       many_steps sigma2 pi2 s2 sigma3 pi3 s3 (n - 1) ->
       many_steps sigma1 pi1 s1 sigma3 pi3 s3 n
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
618
619

lemma steps_non_neg:
atafat's avatar
atafat committed
620
  forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:expr, n:int.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
621
622
623
624
    many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0

(* Used by Hoare_logic/seq_rule*)
  lemma many_steps_seq:
atafat's avatar
atafat committed
625
626
    forall sigma1 sigma3:env, pi1 pi3:stack, e1 e2:expr, n:int.
      many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3 void n ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
627
      exists sigma2:env, pi2:stack, n1 n2:int.
atafat's avatar
atafat committed
628
629
        many_steps sigma1 pi1 e1 sigma2 pi2 void n1 /\
        many_steps sigma2 pi2 e2 sigma3 pi3 void n2 /\
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
630
631
632
633
634
635
636
637
638
639
640
641
        n = 1 + n1 + n2

 (* lemma one_step_change_free : *)
 (*  forall s s':stmt, sigma sigma':env, pi pi':stack, id:ident, v:value. *)
 (*    fresh_in_stmt id s -> *)
 (*    one_step sigma (Cons (id,v) pi) s sigma' pi' s' -> *)
 (*    one_step sigma pi s sigma' pi' s' *)


(** {3 Hoare triples} *)

(** partial correctness *)
atafat's avatar
atafat committed
642
predicate valid_triple (p:fmla) (e:expr) (q:fmla) =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
643
644
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      forall sigma':env, pi':stack, n:int.
atafat's avatar
atafat committed
645
        many_steps sigma pi e sigma' pi' void n ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
646
647
648
          eval_fmla sigma' pi' q

(*** total correctness *)
atafat's avatar
atafat committed
649
predicate total_valid_triple (p:fmla) (e:expr) (q:fmla) =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
650
651
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      exists sigma':env, pi':stack, n:int.
atafat's avatar
atafat committed
652
        many_steps sigma pi e sigma' pi' void n /\
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
        eval_fmla sigma' pi' q

end


theory TestSemantics

use import ImpExpr

function my_sigma : env = IdMap.const (Vint 0)
constant x : ident
constant y : mident

function my_pi : stack = Cons (x, Vint 42) Nil

goal Test13 :
  eval_term my_sigma my_pi (mk_tvalue (Vint 13)) = Vint 13

atafat's avatar
atafat committed
671
672
673
goal Test13expr :
  many_steps my_sigma my_pi (Evalue (Vint 13)) my_sigma my_pi (Evalue (Vint 13)) 0

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
674
goal Test42 :
atafat's avatar
atafat committed
675
676
677
  eval_term my_sigma my_pi (Tvar x) = Vint 42

goal Test42expr :
678
  one_step my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
679
680

goal Test0 :
atafat's avatar
atafat committed
681
682
683
  eval_term my_sigma my_pi (Tderef y) = Vint 0

goal Test0expr :
684
  one_step my_sigma my_pi (Ederef y) my_sigma my_pi (Evalue (Vint 0))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
685
686

goal Test55 :
atafat's avatar
atafat committed
687
688
689
690
  eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55

goal Test55expr :
  many_steps my_sigma my_pi (Ebin (Evar x) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
691
692
693

goal Ass42 :
  forall sigma':env, pi':stack.
atafat's avatar
atafat committed
694
    one_step my_sigma my_pi (Eassign y (Evalue (Vint 42))) sigma' pi' void ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
695
696
697
      IdMap.get sigma' y = Vint 42

goal If42 :
atafat's avatar
atafat committed
698
    forall sigma1 sigma2:env, pi1 pi2:stack, e:expr.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
699
      one_step my_sigma my_pi
atafat's avatar
atafat committed
700
701
702
703
704
        (Eif (Ebin (Ederef y) Ole (Evalue (Vint 10)))
             (Eassign y (Evalue (Vint 13)))
             (Eassign y (Evalue (Vint 42))))
        sigma1 pi1 e ->
      one_step sigma1 pi1 e sigma2 pi2 void ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
705
706
707
708
709
710
711
712
713
714
715
716
717
718
        IdMap.get sigma2 y = Vint 13

end

(** {2 Hoare logic} *)

theory HoareLogic

use import ImpExpr


(** Hoare logic rules (partial correctness) *)

lemma consequence_rule:
atafat's avatar
atafat committed
719
  forall p p' q q':fmla, s:expr.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
720
721
722
723
724
725
  valid_fmla (Fimplies p' p) ->
  valid_triple p s q ->
  valid_fmla (Fimplies q q') ->
  valid_triple p' s q'

lemma skip_rule:
atafat's avatar
atafat committed
726
  forall q:fmla. valid_triple q void q
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
727

atafat's avatar
atafat committed
728
729
730
731
(* lemma assign_rule: *)
(*   forall p:fmla, x:mident, id:ident, t:term. *)
(*   fresh_in_fmla id p -> *)
(*   valid_triple (Flet id t (msubst p x id)) (Eassign x t) p *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
732
733

lemma seq_rule:
atafat's avatar
atafat committed
734
735
736
  forall p q r:fmla, e1 e2:expr.
  valid_triple p e1 r /\ valid_triple r e2 q ->
  valid_triple p (Eseq e1 e2) q
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
737

atafat's avatar
atafat committed
738
739
740
741
742
(* lemma if_rule: *)
(*   forall t:term, p q:fmla, e1 e2:expr. *)
(*   valid_triple (Fand p (Fterm t)) e1 q /\ *)
(*   valid_triple (Fand p (Fnot (Fterm t))) e2 q -> *)
(*   valid_triple p (Eif t e1 e2) q *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
743
744
745

lemma assert_rule:
  forall f p:fmla. valid_fmla (Fimplies p f) ->
atafat's avatar
atafat committed
746
  valid_triple p (Eassert f) p
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
747
748
749

lemma assert_rule_ext:
  forall f p:fmla.
atafat's avatar
atafat committed
750
  valid_triple (Fimplies f p) (Eassert f) p
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799

(*
lemma while_rule:
  forall e:term, inv:fmla, i:expr.
  valid_triple (Fand (Fterm e) inv) i inv ->
  valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)

lemma while_rule_ext:
  forall e:term, inv inv':fmla, i:expr.
  valid_fmla (Fimplies inv' inv) ->
  valid_triple (Fand (Fterm e) inv') i inv' ->
  valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e)) inv')
*)

end

(** {2 WP calculus} *)

theory WP

use import ImpExpr
use import bool.Bool

use set.Set

(** [assigns sigma W sigma'] is true when the only differences between
    [sigma] and [sigma'] are the value of references in [W] *)

predicate assigns (sigma:env) (a:Set.set mident) (sigma':env) =
  forall i:mident. not (Set.mem i a) ->
    IdMap.get sigma i = IdMap.get sigma' i

lemma assigns_refl:
  forall sigma:env, a:Set.set mident. assigns sigma a sigma

lemma assigns_trans:
  forall sigma1 sigma2 sigma3:env, a:Set.set mident.
    assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
    assigns sigma1 a sigma3

lemma assigns_union_left:
  forall sigma sigma':env, s1 s2:Set.set mident.
    assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'

lemma assigns_union_right:
  forall sigma sigma':env, s1 s2:Set.set mident.
    assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'

(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
atafat's avatar
atafat committed
800
predicate expr_writes (s:expr) (w:Set.set mident) =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
801
  match s with
atafat's avatar
atafat committed
802
803
804
805
806
807
808
  | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
  | Eassign id _ -> Set.mem id w
  | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Eif e1 e2 e3 -> expr_writes e1 w /\ expr_writes e2 w /\ expr_writes e3 w
  | Ewhile cond  _ body -> expr_writes cond w /\ expr_writes body w
  | Ebin e1 o e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Elet id e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
809
810
  end

atafat's avatar
atafat committed
811
  function fresh_from (f:fmla) (s:expr) : ident
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
812

Asma Tafat's avatar
Asma Tafat committed
813

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
814
  (* Need it for monotonicity*)
atafat's avatar
atafat committed
815
  axiom fresh_from_fmla: forall s:expr, f:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
816
817
     fresh_in_fmla (fresh_from f s) f

atafat's avatar
atafat committed
818
819
  axiom fresh_from_expr: forall s:expr, f:fmla.
     fresh_in_expr (fresh_from f s) s
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
820

atafat's avatar
atafat committed
821
  function abstract_effects (s:expr) (f:fmla) : fmla
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
822
823

  axiom abstract_effects_generalize :
atafat's avatar
atafat committed
824
     forall sigma:env, pi:stack, s:expr, f:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
825
826
827
828
        eval_fmla sigma pi (abstract_effects s f) ->
        eval_fmla sigma pi f

  axiom abstract_effects_monotonic :
atafat's avatar
atafat committed
829
     forall s:expr, f:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
830
831
832
        forall sigma:env, pi:stack. eval_fmla sigma pi f ->
        forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f)

atafat's avatar
atafat committed
833
834
835
836
837
838
  function wp (e:expr) (q:fmla) : fmla =
    match e with
    | Evalue v -> Flet result (Tvalue v) q
    | Evar v -> Flet result (Tvar v) q
    | Ederef v -> Flet result (Tderef v) q
    | Eassert f ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
839
840
        (* asymmetric and *)
        Fand f (Fimplies f q)
atafat's avatar
atafat committed
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
    | Eseq e1 e2 -> wp e1 (wp e2 q)
    | Elet id e1 e2 -> wp e1 (Flet id (Tvar result) (wp e2 q))
    | Ebin e1 op e2 ->
       let t1 = fresh_from q e in
       let t2 = fresh_from (Fand (Fterm (Tvar t1)) q) e in
       let q' = Flet result (Tbin (Tvar t1) op (Tvar t2)) q in
       let f = wp e2 (Flet t2 (Tvar result) q') in
       wp e1 (Flet t1 (Tvar result) f)
       (* let wp_op = subst q (Tvar result) (Tbin (Tvar t1) op (Tvar t2)) in *)
       (* let wp2 = (subst (wp e2 wp_op) t2 (Tvar result)) in *)
       (* (subst (wp e1 wp2) t1 (Tvar result)) *)
    | Eassign x e ->
        let id = fresh_from q e in
        let q' = Flet result (Tvalue Vvoid) q in
        wp e (Flet id (Tvar result) (msubst q' x id))
    | Eif e1 e2 e3 ->
        let f =
          Fand (Fimplies (Fterm (Tvar result)) (wp e2 q))
            (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q))
        in
        wp e1 f
    | Ewhile cond inv body ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
863
864
        Fand inv
          (abstract_effects body
atafat's avatar
atafat committed
865
866
867
868
            (wp cond
             (Fand
              (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q))))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
869
870
871
872

    end

  axiom abstract_effects_writes :
atafat's avatar
atafat committed
873
     forall sigma:env, pi:stack, s:expr, q:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
874
875
876
877
878
879
880
881
882
883
        eval_fmla sigma pi (abstract_effects s q) ->
        eval_fmla sigma pi (wp s (abstract_effects s q))


  (* lemma wp_subst: *)
  (*   forall e:expr, q:fmla, id :mident, id':ident. *)
  (*   fresh_in_stmt id e -> *)
  (*     subst (wp e q) id id' = wp e (subst q id id') *)

  lemma monotonicity:
atafat's avatar
atafat committed
884
    forall s:expr, p q:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
885
886
887
888
      valid_fmla (Fimplies p q)
     ->	valid_fmla (Fimplies (wp s p) (wp s q) )

  lemma distrib_conj:
atafat's avatar
atafat committed
889
    forall s:expr, sigma:env, pi:stack, p q:fmla.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
890
891
     (eval_fmla sigma pi (wp s p)) /\
     (eval_fmla sigma pi (wp s q)) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
892
     eval_fmla sigma pi (wp s (Fand p q))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
893
894

  lemma wp_reduction:
atafat's avatar
atafat committed
895
    forall sigma sigma':env, pi pi':stack, s s':expr.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
896
897
898
899
900
    one_step sigma pi s sigma' pi' s' ->
    forall q:fmla.
      eval_fmla sigma pi (wp s q) ->
      eval_fmla sigma' pi' (wp s' q)

atafat's avatar
atafat committed
901
902
903
904
905
906
907
908
909
910
  predicate is_value (e:expr) =
    match e with
    | Evalue _ -> true
    | _ -> false
    end

  lemma decide_value :
    forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v

  lemma bool_value:
Andrei Paskevich's avatar
Andrei Paskevich committed
911
    forall v:value, sigmat: type_env, pit:type_stack.
atafat's avatar
atafat committed
912
913
914
915
      type_expr sigmat pit (Evalue v) TYbool ->
          (v = Vbool False) \/ (v = Vbool True)

  lemma unit_value:
Andrei Paskevich's avatar
Andrei Paskevich committed
916
917
    forall v:value, sigmat: type_env, pit:type_stack.
      type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid
atafat's avatar
atafat committed
918

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
919
  lemma progress:
atafat's avatar
atafat committed
920
    forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
Andrei Paskevich's avatar
Andrei Paskevich committed
921
      type_expr sigmat pit e ty ->
atafat's avatar
atafat committed
922
923
      type_fmla sigmat (Cons(result, ty) pit) q ->
      not is_value e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
924
      eval_fmla sigma pi (wp e q) ->
atafat's avatar
atafat committed
925
926
      exists sigma':env, pi':stack, e':expr.
      one_step sigma pi e sigma' pi' e'
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
927
928
929
930
931
932

end


(***
Local Variables:
atafat's avatar
atafat committed
933
compile-command: "why3ide blocking_semantics4.mlw"
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
934
935
End:
*)