blocking_semantics.mlw 26.3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

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

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

theory ImpExpr

use import int.Int
use import bool.Bool

(** types and values *)

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

(** terms and formulas *)

type operator = Oplus | Ominus | Omult | Ole

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
20
(** ident for imutable variable*)
Andrei Paskevich's avatar
Andrei Paskevich committed
21
type ident
MARCHE Claude's avatar
MARCHE Claude committed
22

Andrei Paskevich's avatar
Andrei Paskevich committed
23
constant result : ident
MARCHE Claude's avatar
MARCHE Claude committed
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

type term =
  | Tvalue value
  | Tvar ident
  | Tderef ident
  | Tbin term operator term

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 *)

use map.Map as IdMap
type env = IdMap.map ident value  (* map global mutable variables to their value *)
function get_env (i:ident) (e:env) : value = IdMap.get e i

use export list.List
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
  | Tvalue v -> v
  | Tvar id -> get_stack id pi
  | Tderef id -> get_env id sigma
  | Tbin t1 op t2 ->
     eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
  end

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
Andrei Paskevich's avatar
Andrei Paskevich committed
89
  | Flet x t f ->
MARCHE Claude's avatar
MARCHE Claude committed
90
      eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
Andrei Paskevich's avatar
Andrei Paskevich committed
91
  | Fforall x TYint f ->
MARCHE Claude's avatar
MARCHE Claude committed
92
93
94
     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
Andrei Paskevich's avatar
Andrei Paskevich committed
95
  | Fforall x TYunit f ->  eval_fmla sigma (Cons (x,Vvoid) pi) f
MARCHE Claude's avatar
MARCHE Claude committed
96
97
98
99
100
101
102
103
  end

(** substitution of a reference [r] by a logic variable [v]
   warning: proper behavior only guaranted if [v] is fresh *)

function subst_term (e:term) (r:ident) (v:ident) : term =
  match e with
  | Tvalue _ | Tvar _ -> e
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
104
  | Tderef x -> if r = x then Tvar v else e
MARCHE Claude's avatar
MARCHE Claude committed
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
  | Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v)
  end

(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (id:ident) (t:term) =
  match t with
  | Tvalue _ -> true
  | Tvar v -> id <> v
  | Tderef _ -> true
  | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2
  end

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 (IdMap.set sigma x (get_stack v pi)) pi e

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
148
149
150
151
152
153
154
lemma subst_fresh :
  forall f:fmla, x v:ident.
   fresh_in_fmla x f -> subst f x v = f

lemma let_subst:
    forall t:term, f:fmla, x id id':ident.
    subst (Flet x t f) id id' = Flet x (subst_term t id id') (subst f id id')
MARCHE Claude's avatar
MARCHE Claude committed
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172

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 (IdMap.set sigma x (get_stack v pi)) pi f)

lemma eval_swap:
  forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
    eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)

lemma eval_change_free :
  forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
    fresh_in_fmla id f ->
    (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)

MARCHE Claude's avatar
MARCHE Claude committed
173
174
175
176
177
178
179
180
181
182

  (** [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

lemma let_equiv :
  forall id id':ident, t:term, f:fmla.
    forall sigma:env, pi:stack.
      eval_fmla sigma pi (Flet id' t (subst f id id'))
      -> eval_fmla sigma pi (Flet id t f)

MARCHE Claude's avatar
MARCHE Claude committed
183
184
185
186
187
188
189
190
191
192
193
194
195
196
(* expressions *)

type expr =
  | Evalue value
  | Ebin expr operator expr
  | Evar ident
  | Ederef ident
  | Eassign ident expr
  | Eseq expr expr
  | Elet ident expr expr
  | Eif expr expr expr
  | Eassert fmla
  | Ewhile expr fmla expr  (* while cond invariant inv body *)

MARCHE Claude's avatar
MARCHE Claude committed
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
predicate fresh_in_expr (id:ident) (e:expr) =
  match e with
  | Evalue _ -> true
  | Eseq e1 e2
  | Ebin e1 _ e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
  | Evar v -> id <> v
  | Ederef _ -> true
  | Eassign _ e -> fresh_in_expr id e
  | 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
  end


MARCHE Claude's avatar
MARCHE Claude committed
212
213
214
215
216
217
constant void : expr = Evalue Vvoid

(** small-steps semantics for expressions *)

inductive one_step env stack expr env stack expr =

MARCHE Claude's avatar
MARCHE Claude committed
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
  | 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:ident.
        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')

  | one_step_bin_value:
      forall sigma sigma':env, pi 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))

MARCHE Claude's avatar
MARCHE Claude committed
241
242
243
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
280
281
282
283
284
285
286
287
288
289
290
291
  | one_step_assign_ctxt:
      forall sigma sigma':env, pi pi':stack, x:ident, e e':expr.
        one_step sigma pi e sigma' pi' e' ->
        one_step sigma pi (Eassign x e)
                 sigma' pi' (Eassign x e')

  | one_step_assign_value:
      forall sigma:env, pi:stack, x:ident, v:value, e:term.
        one_step sigma pi (Eassign x (Evalue v))
                 (IdMap.set sigma x v) 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, id:ident, 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, id:ident, 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)

  | one_step_if_true:
      forall sigma:env, pi:stack, e:term, e1 e2:expr.
        one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1

  | one_step_if_false:
      forall sigma:env, pi:stack, e:term, e1 e2:expr.
        one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2

  | one_step_assert:
      forall sigma:env, pi:stack, f:fmla.
        (* blocking semantics *)
        eval_fmla sigma pi f ->
          one_step sigma pi (Eassert f) sigma pi void

  | one_step_while:
      forall sigma:env, pi:stack, cond:expr, inv:fmla, body:expr.
        (* blocking semantics *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
292
        eval_fmla sigma pi inv ->
MARCHE Claude's avatar
MARCHE Claude committed
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
        one_step sigma pi (Ewhile cond inv body) sigma pi
        (Eif cond (Eseq body (Ewhile cond inv body)) void)

 (** many steps of execution *)

 inductive many_steps env stack expr env stack expr int =
   | many_steps_refl:
     forall sigma:env, pi:stack, e:expr. many_steps sigma pi e sigma pi e 0
   | many_steps_trans:
     forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, e1 e2 e3:expr, n:int.
       one_step sigma1 pi1 e1 sigma2 pi2 e2 ->
       many_steps sigma2 pi2 e2 sigma3 pi3 e3 n ->
       many_steps sigma1 pi1 e1 sigma3 pi3 e3 (n+1)

  lemma steps_non_neg:
    forall sigma1 sigma2:env, pi1 pi2:stack, e1 e2:expr, n:int.
      many_steps sigma1 pi1 e1 sigma2 pi2 e2 n -> n >= 0

  lemma many_steps_seq:
    forall sigma1 sigma3:env, pi1 pi3:stack, e1 e2:expr, n:int.
      many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3 void n ->
      exists sigma2:env, pi2:stack, n1 n2:int.
        many_steps sigma1 pi1 e1 sigma2 pi2 void n1 /\
        many_steps sigma2 pi2 e2 sigma3 pi3 void n2 /\
        n = 1 + n1 + n2

  lemma many_steps_let:
    forall sigma1 sigma3:env, pi1 pi3:stack, id:ident, e1 e2:expr, v2:value, n:int.
      many_steps sigma1 pi1 (Elet id e1 e2) sigma3 pi3 (Evalue v2) n ->
      exists sigma2:env, pi2:stack, v1:value, n1 n2:int.
        many_steps sigma1 pi1 e1 sigma2 pi2 (Evalue v1) n1 /\
        many_steps sigma2 (Cons (id,v1) pi2) e2 sigma3 pi3 (Evalue v2) n2 /\
        n = 1 + n1 + n2

MARCHE Claude's avatar
MARCHE Claude committed
327
328
329
330
331
332
333
 lemma one_step_change_free :
  forall e e':expr, sigma sigma':env, pi pi':stack, id:ident, v:value.
    fresh_in_expr id e ->
    one_step sigma (Cons (id,v) pi) e sigma' pi' e' ->
    one_step sigma pi e sigma' pi' e'


MARCHE Claude's avatar
MARCHE Claude committed
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358

(** {3 Hoare triples} *)

(** partial correctness *)
predicate valid_triple (p:fmla) (e:expr) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      forall sigma':env, pi':stack, v:value, n:int.
        many_steps sigma pi e sigma' pi' (Evalue v) n ->
          eval_fmla sigma' (Cons (result,v) pi') q

(*** total correctness *)
predicate total_valid_triple (p:fmla) (e:expr) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      exists sigma':env, pi':stack, v:value, n:int.
        many_steps sigma pi e sigma' pi' (Evalue v) n /\
        eval_fmla sigma' (Cons (result,v) pi') q

end


theory TestSemantics

use import ImpExpr

function my_sigma : env = IdMap.const (Vint 0)
MARCHE Claude's avatar
MARCHE Claude committed
359
360
constant x : ident
function my_pi : stack = Cons (x, Vint 42) Nil
MARCHE Claude's avatar
MARCHE Claude committed
361
362
363
364
365
366
367
368

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

goal Test13expr :
  many_steps my_sigma my_pi (Evalue (Vint 13)) my_sigma my_pi (Evalue (Vint 13)) 0

goal Test42 :
MARCHE Claude's avatar
MARCHE Claude committed
369
  eval_term my_sigma my_pi (Tvar x) = Vint 42
MARCHE Claude's avatar
MARCHE Claude committed
370
371

goal Test42expr :
MARCHE Claude's avatar
MARCHE Claude committed
372
  many_steps my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42)) 1
MARCHE Claude's avatar
MARCHE Claude committed
373
374

goal Test0 :
MARCHE Claude's avatar
MARCHE Claude committed
375
  eval_term my_sigma my_pi (Tderef x) = Vint 0
MARCHE Claude's avatar
MARCHE Claude committed
376
377

goal Test0expr :
MARCHE Claude's avatar
MARCHE Claude committed
378
  many_steps my_sigma my_pi (Ederef x) my_sigma my_pi (Evalue (Vint 0)) 1
MARCHE Claude's avatar
MARCHE Claude committed
379
380

goal Test55 :
MARCHE Claude's avatar
MARCHE Claude committed
381
  eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55
MARCHE Claude's avatar
MARCHE Claude committed
382
383

goal Test55expr :
MARCHE Claude's avatar
MARCHE Claude committed
384
  many_steps my_sigma my_pi (Ebin (Evar x) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 2
MARCHE Claude's avatar
MARCHE Claude committed
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
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

goal Ass42 :
  forall sigma':env, pi':stack.
    one_step my_sigma my_pi (Eassign x (Evalue (Vint 42))) sigma' pi' void ->
      IdMap.get sigma' x = Vint 42

goal If42 :
    forall sigma1 sigma2:env, pi1 pi2:stack, e:expr.
      one_step my_sigma my_pi
        (Eif (Ebin (Ederef x) Ole (Evalue (Vint 10)))
             (Eassign x (Evalue (Vint 13)))
             (Eassign x (Evalue (Vint 42))))
        sigma1 pi1 e ->
      one_step sigma1 pi1 e sigma2 pi2 void ->
        IdMap.get sigma2 x = Vint 13

end

(** {2 Hoare logic} *)

theory HoareLogic

use import ImpExpr


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

lemma consequence_rule:
  forall p p' q q':fmla, e:expr.
  valid_fmla (Fimplies p' p) ->
  valid_triple p e q ->
  valid_fmla (Fimplies q q') ->
  valid_triple p' e q'

lemma value_rule:
  forall q:fmla, v:value. fresh_in_fmla result q ->
  valid_triple q (Evalue v) q

lemma assign_rule:
  forall p q:fmla, x:ident, e:expr.
  valid_triple p e (subst q x result) ->
  valid_triple p (Eassign x e) q

lemma seq_rule:
  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

lemma let_rule:
  forall p q r:fmla, id:ident, e1 e2:expr.
  id <> result -> fresh_in_fmla id r ->
  valid_triple p e1 r /\ valid_triple (Flet result (Tvar id) r) e2 q ->
  valid_triple p (Elet id e1 e2) q

(*
lemma if_rule:
  forall e:expr, p q:fmla, i1 i2:expr.
  valid_triple (Fand p (Fterm e)) i1 q /\
  valid_triple (Fand p (Fnot (Fterm e))) i2 q ->
  valid_triple p (Eif e e1 e2) q
*)

lemma assert_rule:
  forall f p:fmla. valid_fmla (Fimplies p f) ->
  valid_triple p (Eassert f) p

lemma assert_rule_ext:
  forall f p:fmla.
  valid_triple (Fimplies f p) (Eassert f) p

(*
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')
*)

(*** frame rule ? *)

end

(** {2 WP calculus} *)

theory WP

use import ImpExpr

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 ident) (sigma':env) =
  forall i:ident. not (Set.mem i a) ->
    IdMap.get sigma i = IdMap.get sigma' i

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

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

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

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

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
503
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
MARCHE Claude's avatar
MARCHE Claude committed
504
505
506
507
508
509
510
511
512
513
514
predicate expr_writes (e:expr) (w:Set.set ident) =
  match e with
  | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
  | Ebin e1 _ e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Eassign id _ -> Set.mem id w
  | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Elet id 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
  end

MARCHE Claude's avatar
MARCHE Claude committed
515
516
517
518
519
520
521
  function fresh_from (f:fmla) (e:expr) : ident

  axiom fresh_from_fmla: forall e:expr, f:fmla.
     fresh_in_fmla (fresh_from f e) f

  axiom fresh_from_expr: forall e:expr, f:fmla.
     fresh_in_expr (fresh_from f e) e
MARCHE Claude's avatar
MARCHE Claude committed
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537

  function abstract_effects (e:expr) (f:fmla) : fmla

  function wp (e:expr) (q:fmla) : fmla =
    match e with
    | Evalue v ->
        (* let result = v in q *)
        Flet result (Tvalue v) q
    | Evar v -> Flet result (Tvar v) q
    | Ederef x -> Flet result (Tderef x) q
    | Eassert f ->
        (* asymmetric and *)
        Fand f (Fimplies f q)
    | 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 ->
MARCHE Claude's avatar
MARCHE Claude committed
538
539
       let t1 = fresh_from q e in
       let t2 = fresh_from (Fand (Fterm (Tvar t1)) q) e in
MARCHE Claude's avatar
MARCHE Claude committed
540
541
542
543
       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)
    | Eassign x e ->
MARCHE Claude's avatar
MARCHE Claude committed
544
        let id = fresh_from q e in
MARCHE Claude's avatar
MARCHE Claude committed
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
        let q' = Flet result (Tvalue Vvoid) q in
        wp e (Flet id (Tvar result) (subst 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 ->
        Fand inv
          (abstract_effects body
            (wp cond
             (Fand
              (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q))))

    end

MARCHE Claude's avatar
MARCHE Claude committed
563
564
565
566
  lemma wp_subst:
    forall e:expr, q:fmla, id id':ident.
    fresh_in_expr id e ->
      subst (wp e q) id id' = wp e (subst q id id')
MARCHE Claude's avatar
MARCHE Claude committed
567

MARCHE Claude's avatar
MARCHE Claude committed
568
569
570
571
572
573
574
575
  lemma wp_implies:
    forall p q:fmla.
     (forall sigma:env, pi:stack.
        eval_fmla sigma pi p -> eval_fmla sigma pi q)
     ->
     forall sigma:env, pi:stack, e:expr.
       eval_fmla sigma pi (wp e p) ->
       eval_fmla sigma pi (wp e q)
MARCHE Claude's avatar
MARCHE Claude committed
576
577
578
579
580
581
582
583
584

  lemma wp_conj:
    forall sigma:env, pi:stack, e:expr, p q:fmla.
     eval_fmla sigma pi (wp e (Fand p q)) <->
       (eval_fmla sigma pi (wp e p)) /\
       (eval_fmla sigma pi (wp e q))


  lemma wp_reduction:
MARCHE Claude's avatar
MARCHE Claude committed
585
586
587
588
589
    forall sigma sigma':env, pi pi':stack, e e':expr.
    one_step sigma pi e sigma' pi' e' ->
    forall q:fmla.
      eval_fmla sigma pi (wp e q) ->
      eval_fmla sigma' pi' (wp e' q)
MARCHE Claude's avatar
MARCHE Claude committed
590
591
592
593
594
595
596

  predicate not_a_value (e:expr) =
    match e with
    | Evalue _ -> false
    | _ -> true
    end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
597
  lemma decide_value:
MARCHE Claude's avatar
MARCHE Claude committed
598
599
    forall e:expr. not_a_value e \/ exists v:value. e = Evalue v

MARCHE Claude's avatar
MARCHE Claude committed
600
  lemma progress:
MARCHE Claude's avatar
MARCHE Claude committed
601
    forall e:expr, sigma:env, pi:stack, q:fmla.
MARCHE Claude's avatar
MARCHE Claude committed
602
603
604
605
    eval_fmla sigma pi (wp e q) /\ not_a_value e ->
    exists sigma':env, pi':stack, e':expr.
      one_step sigma pi e sigma' pi' e'

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

MARCHE Claude's avatar
MARCHE Claude committed
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
(*
  let rec compute_writes (s:expr) : Set.set ident =
   { }
    match s with
    | Sskip -> Set.empty
    | Sassign i _ -> Set.singleton i
    | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Swhile _ _ s -> compute_writes s
    | Sassert _ -> Set.empty
    end
   { forall sigma sigma':env, pi pi':stack, n:int.
       many_steps sigma pi s sigma' pi' Sskip n ->
       assigns sigma result sigma' }

  val fresh_from_fmla (q:fmla) :
     { }
     ident
     { fresh_in_fmla result q }

  val abstract_effects (i:expr) (f:fmla) :
    { }
    fmla
    { forall sigma:env, pi:stack. eval_fmla sigma pi result ->
        eval_fmla sigma pi f /\
(***
        forall sigma':env, w:Set.set ident.
        expr_writes i w /\ assigns sigma w sigma' ->
        eval_fmla sigma' pi result
*)
        forall sigma' pi':env, n:int.
           many_steps sigma pi i sigma' pi' Sskip n ->
           eval_fmla sigma' pi' result
     }

  use HoareLogic

  let rec wp (i:expr) (q:fmla) =
    { true }
    match i with
    | Sskip -> q
    | Sseq i1 i2 -> wp i1 (wp i2 q)
    | Sassign x e ->
        let id = fresh_from_fmla q in Flet id e (subst q x id)
    | Sif e i1 i2 ->
        Fand (Fimplies (Fterm e) (wp i1 q))
             (Fimplies (Fnot (Fterm e)) (wp i2 q))
    | Sassert f ->
       Fimplies f q (* liberal wp, no termination required *)
       (* Fand f q *) (* strict wp, termination required *)
    | Swhile e inv i ->
        Fand inv
          (abstract_effects i
            (Fand
                (Fimplies (Fand (Fterm e) inv) (wp i inv))
                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))

    end
    { valid_triple result i q }

*)

end

MARCHE Claude's avatar
MARCHE Claude committed
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
(* pas concluant

(** {2 WP calculus, variant} *)

theory WP2

use import ImpExpr

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 ident) (sigma':env) =
  forall i:ident. not (Set.mem i a) ->
    IdMap.get sigma i = IdMap.get sigma' i

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

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

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

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

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
704
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
MARCHE Claude's avatar
MARCHE Claude committed
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
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
predicate expr_writes (e:expr) (w:Set.set ident) =
  match e with
  | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
  | Ebin e1 _ e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Eassign id _ -> Set.mem id w
  | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
  | Elet id 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
  end

  function fresh_from (f:fmla) (e:expr) : ident

  axiom fresh_from_fmla: forall e:expr, f:fmla.
     fresh_in_fmla (fresh_from f e) f

  axiom fresh_from_expr: forall e:expr, f:fmla.
     fresh_in_expr (fresh_from f e) e

  function abstract_effects (e:expr) (f:fmla) : fmla

  predicate is_pure (e:expr) =
    match e with
    | Evalue _ | Evar _ | Ederef _ -> true
    | Eassert _ -> false (* true *)
    | Eseq e1 e2 -> false (* is_pure e1 /\ is_pure e2 *)
    | Elet id e1 e2 -> false (* is_pure e1 /\ is_pure e2 *)
    | Ebin e1 op e2 -> false (* is_pure e1 /\ is_pure e2 *)
    | Eassign x e -> false
    | Eif e1 e2 e3 -> false (* is_pure e1 /\ is_pure e2 /\ is_pure e3 *)
    | Ewhile cond inv body -> false
    end

  function purify (e:expr) : term =
    match e with
    | Evalue v -> Tvalue v
    | Evar id -> Tvar id
    | Ederef id -> Tderef id
    | _ -> Tvalue Vvoid
   end

  function wp (e:expr) (q:fmla) : fmla =
    match e with
    | Evalue v ->
        (* let result = e in q *)
        Flet result (Tvalue v) q
    | Evar v -> Flet result (Tvar v) q
    | Ederef x -> Flet result (Tderef x) q
    | Eassert f ->
        (* asymmetric and *)
        Fand f (Fimplies f q)
    | 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 ->
       if is_pure e1 then
          if is_pure e2 then
             Flet result (Tbin (purify e1) op (purify e2)) q
          else
             let id = fresh_from q e in
             wp (Elet id e2 (Ebin e1 op (Evar id))) q
       else
          let id = fresh_from q e in
          wp (Elet id e1 (Ebin (Evar id) op e2)) q
    | Eassign x e ->
        if is_pure e then
          let q' = Flet result (Tvalue Vvoid) q in
          let id = fresh_from q' e in
          Flet id (purify e) (subst q' x id)
        else
          let id = fresh_from q e in
          wp (Elet id e (Eassign x (Evar id))) q
    | 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 ->
        Fand inv
          (abstract_effects body
            (wp cond
             (Fand
              (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q))))

    end

MARCHE Claude's avatar
MARCHE Claude committed
792

MARCHE Claude's avatar
MARCHE Claude committed
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
  lemma wp_conj:
    forall sigma:env, pi:stack, e:expr, p q:fmla.
     eval_fmla sigma pi (wp e (Fand p q)) <->
       (eval_fmla sigma pi (wp e p)) /\
       (eval_fmla sigma pi (wp e q))


  lemma wp_reduction:
    forall sigma sigma':env, pi pi':stack, e e':expr.
    one_step sigma pi e sigma' pi' e' ->
    forall q:fmla.
      eval_fmla sigma pi (wp e q) ->
      eval_fmla sigma' pi' (wp e' q)

  predicate not_a_value (e:expr) =
    match e with
    | Evalue _ -> false
    | _ -> true
    end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
813
  lemma decide_value:
MARCHE Claude's avatar
MARCHE Claude committed
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
    forall e:expr. not_a_value e \/ exists v:value. e = Evalue v

  lemma progress:
    forall e:expr, sigma:env, pi:stack, q:fmla.
    eval_fmla sigma pi (wp e q) /\ not_a_value e ->
    exists sigma':env, pi':stack, e':expr.
      one_step sigma pi e sigma' pi' e'

(*
  let rec compute_writes (s:expr) : Set.set ident =
   { }
    match s with
    | Sskip -> Set.empty
    | Sassign i _ -> Set.singleton i
    | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Swhile _ _ s -> compute_writes s
    | Sassert _ -> Set.empty
    end
   { forall sigma sigma':env, pi pi':stack, n:int.
       many_steps sigma pi s sigma' pi' Sskip n ->
       assigns sigma result sigma' }

  val fresh_from_fmla (q:fmla) :
     { }
     ident
     { fresh_in_fmla result q }

  val abstract_effects (i:expr) (f:fmla) :
    { }
    fmla
    { forall sigma:env, pi:stack. eval_fmla sigma pi result ->
        eval_fmla sigma pi f /\
(***
        forall sigma':env, w:Set.set ident.
        expr_writes i w /\ assigns sigma w sigma' ->
        eval_fmla sigma' pi result
*)
        forall sigma' pi':env, n:int.
           many_steps sigma pi i sigma' pi' Sskip n ->
           eval_fmla sigma' pi' result
     }

  use HoareLogic

  let rec wp (i:expr) (q:fmla) =
    { true }
    match i with
    | Sskip -> q
    | Sseq i1 i2 -> wp i1 (wp i2 q)
    | Sassign x e ->
        let id = fresh_from_fmla q in Flet id e (subst q x id)
    | Sif e i1 i2 ->
        Fand (Fimplies (Fterm e) (wp i1 q))
             (Fimplies (Fnot (Fterm e)) (wp i2 q))
    | Sassert f ->
       Fimplies f q (* liberal wp, no termination required *)
       (* Fand f q *) (* strict wp, termination required *)
    | Swhile e inv i ->
        Fand inv
          (abstract_effects i
            (Fand
                (Fimplies (Fand (Fterm e) inv) (wp i inv))
                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))

    end
    { valid_triple result i q }

*)

end

*)
MARCHE Claude's avatar
MARCHE Claude committed
887
888
889

(***
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
890
compile-command: "why3ide blocking_semantics.mlw"
MARCHE Claude's avatar
MARCHE Claude committed
891
892
893
End:
*)