blocking_semantics5.mlw 20.7 KB
Newer Older
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

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

(** {2 Formalisation d’un langage impératif jouet} *)

(** {3 Syntaxe} *)

theory Syntax

use export bool.Bool
use export int.Int

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

lemma mident_decide :
  forall m1 m2: mident. m1 = m2 \/ m1 <> m2

(** ident for immutable variables *)
Claude Marche's avatar
Claude Marche committed
29
30
type ident

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
lemma ident_decide :
  forall m1 m2: ident. m1 = m2 \/ m1 <> m2

(** Terms *)
type term =
  | Tvalue value
  | Tvar ident
  | Tderef mident
  | Tbin term operator term


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

(** Statements *)
type stmt =
  | Sskip
  | Sassign mident term
  | Sseq stmt stmt
  | Sif term stmt stmt
  | Sassert fmla
  | Swhile term fmla stmt  (* while cond invariant inv body *)

lemma decide_is_skip:
  forall s:stmt. s = Sskip \/ s <> Sskip

end






(** {3 Semantique Operationnelle} *)


theory SemOp

use export Syntax
use map.Map as IdMap
use export list.List

(** 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
  | Tvalue v -> v
Claude Marche's avatar
Claude Marche committed
115
116
117
  | Tvar id  -> get_stack id pi
  | Tderef id  -> get_env id sigma
  | Tbin t1 op t2  ->
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
     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
  | 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


(** [valid_fmla f] is true when [f] is valid in any environment *)
Claude Marche's avatar
Claude Marche committed
139
predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
140
141
142
143
144
145
146
147




(** small-steps semantics for statements *)

inductive one_step env stack stmt env stack stmt =

Claude Marche's avatar
Claude Marche committed
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
  | one_step_assign : forall sigma sigma':env, pi:stack, x:mident, t:term.
      sigma' = IdMap.set sigma x (eval_term sigma pi t) ->
      one_step sigma pi (Sassign x t) sigma' pi Sskip

  | one_step_seq_noskip: forall sigma sigma':env, pi pi':stack, s1 s1' s2:stmt.
      one_step sigma pi s1 sigma' pi' s1' ->
      one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1' s2)

  | one_step_seq_skip: forall sigma:env, pi:stack, s:stmt.
      one_step sigma pi (Sseq Sskip s) sigma pi s

  | one_step_if_true: forall sigma:env, pi:stack, t:term, s1 s2:stmt.
      eval_term sigma pi t = Vbool True ->
      one_step sigma pi (Sif t s1 s2) sigma pi s1

  | one_step_if_false: forall sigma:env, pi:stack, t:term, s1 s2:stmt.
      eval_term sigma pi t = Vbool False ->
      one_step sigma pi (Sif t s1 s2) sigma pi s2

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

  | one_step_while_true: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
      eval_fmla sigma pi inv /\       (** blocking semantics *)
      eval_term sigma pi cond = Vbool True ->
      one_step sigma pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))

  | one_step_while_false: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
        eval_fmla sigma pi inv /\     (** blocking semantics *)
178
179
180
181
182
        eval_term sigma pi cond = Vbool False ->
        one_step sigma pi (Swhile cond inv body) sigma pi Sskip

 (** many steps of execution *)

Claude Marche's avatar
Claude Marche committed
183
inductive many_steps env stack stmt env stack stmt int =
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | many_steps_refl: forall sigma:env, pi:stack, s:stmt.
Claude Marche's avatar
Claude Marche committed
185
186
187
188
189
      many_steps sigma pi s sigma pi s 0
  | many_steps_trans: forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:stmt, n:int.
      one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
      many_steps sigma2 pi2 s2 sigma3 pi3 s3 n ->
      many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n+1)
190

Claude Marche's avatar
Claude Marche committed
191
192
lemma steps_non_neg: forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:stmt, n:int.
  many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0
193
194


Claude Marche's avatar
Claude Marche committed
195
196
predicate reductible (sigma:env) (pi:stack) (s:stmt) =
  exists sigma':env, pi':stack, s':stmt. one_step sigma pi s sigma' pi' s'
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259

end



theory TestSemantics

use import SemOp

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 (Tvalue (Vint 13)) = Vint 13

goal Test42 :
  eval_term my_sigma my_pi (Tvar x) = Vint 42

goal Test0 :
  eval_term my_sigma my_pi (Tderef y) = Vint 0

goal Test55 :
  eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55

goal Ass42 :
  forall sigma':env, pi':stack.
    one_step my_sigma my_pi (Sassign y (Tvalue (Vint 42))) sigma' pi' Sskip ->
      IdMap.get sigma' y = Vint 42

goal If42 :
    forall sigma1 sigma2:env, pi1 pi2:stack, s:stmt.
      one_step my_sigma my_pi
        (Sif (Tbin (Tderef y) Ole (Tvalue (Vint 10)))
             (Sassign y (Tvalue (Vint 13)))
             (Sassign y (Tvalue (Vint 42))))
        sigma1 pi1 s ->
      one_step sigma1 pi1 s sigma2 pi2 Sskip ->
        IdMap.get sigma2 y = Vint 13

end




(** {3 Typage} *)

theory Typing

use export Syntax
use map.Map as IdMap
use export list.List

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) =
Claude Marche's avatar
Claude Marche committed
260
261
262
263
  | 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
264
265
266
267
268
269
270
271
272
273
274
275
276

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


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 =
Claude Marche's avatar
Claude Marche committed
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291

  | Type_value : forall sigma: type_env, pi:type_stack, v:value.
      type_term sigma pi  (Tvalue v) (type_value v)

  | Type_var : forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
      (get_vartype v pi = ty) ->
      type_term sigma pi (Tvar v) ty

  | Type_deref : forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
      (get_reftype v sigma = ty) ->
      type_term sigma pi (Tderef v) ty

  | Type_bin : forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator, ty1 ty2 ty:datatype.
      type_term sigma pi t1 ty1 /\ type_term sigma pi t2 ty2 /\ type_operator op ty1 ty2 ty ->
      type_term sigma pi (Tbin t1 op t2) ty
292
293

inductive type_fmla type_env type_stack fmla =
Claude Marche's avatar
Claude Marche committed
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308

  | 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 ->
309
310
311
312
        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.
Claude Marche's avatar
Claude Marche committed
313
        type_term sigma pi t ty ->
314
315
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Flet x t f)
MARCHE Claude's avatar
MARCHE Claude committed
316
317
318
319
  | Type_forall :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla, ty:datatype.
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Fforall x ty f)
320
321
322
323

inductive type_stmt type_env type_stack stmt =
  | Type_skip :
      forall sigma: type_env, pi:type_stack.
Claude Marche's avatar
Claude Marche committed
324
        type_stmt sigma pi Sskip
325
326
327
  | Type_seq :
      forall sigma: type_env, pi:type_stack, s1 s2:stmt.
        type_stmt sigma pi s1 ->
Claude Marche's avatar
Claude Marche committed
328
329
        type_stmt sigma pi s2 ->
        type_stmt sigma pi (Sseq s1 s2)
330
331
  | Type_assigns :
      forall sigma: type_env, pi:type_stack, x:mident, t:term, ty:datatype.
Claude Marche's avatar
Claude Marche committed
332
        (get_reftype x sigma = ty) ->
333
334
335
336
        type_term sigma pi t ty ->
        type_stmt sigma pi (Sassign x t)
  | Type_if :
      forall sigma: type_env, pi:type_stack, t:term, s1 s2:stmt.
Claude Marche's avatar
Claude Marche committed
337
338
339
340
        type_term sigma pi t TYbool ->
        type_stmt sigma pi s1 ->
        type_stmt sigma pi s2 ->
        type_stmt sigma pi (Sif t s1 s2)
341
342
  | Type_assert :
      forall sigma: type_env, pi:type_stack, p:fmla.
Claude Marche's avatar
Claude Marche committed
343
344
        type_fmla sigma pi p ->
        type_stmt sigma pi (Sassert p)
345
  | Type_while :
MARCHE Claude's avatar
MARCHE Claude committed
346
      forall sigma: type_env, pi:type_stack, cond:term, body:stmt, inv:fmla.
Claude Marche's avatar
Claude Marche committed
347
        type_fmla sigma pi inv ->
MARCHE Claude's avatar
MARCHE Claude committed
348
        type_term sigma pi cond TYbool ->
349
        type_stmt sigma pi body ->
MARCHE Claude's avatar
MARCHE Claude committed
350
        type_stmt sigma pi (Swhile cond inv body)
351
352
353
354
355
356
357
358
359
360
361
362


end


(** {3 Relations entre typage et semantique operationnelle} *)

theory TypingAndSemantics

use import SemOp
use import Typing

MARCHE Claude's avatar
MARCHE Claude committed
363
(*
364
inductive compatible datatype value =
Claude Marche's avatar
Claude Marche committed
365
366
367
368
369
370
    | Compatible_bool :
        forall b: bool. compatible TYbool (Vbool b)
    | Compatible_int :
        forall n: int. compatible TYint (Vint n)
    | Compatible_void :
        compatible TYunit Vvoid
371

MARCHE Claude's avatar
MARCHE Claude committed
372
373
*)

MARCHE Claude's avatar
MARCHE Claude committed
374
predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
MARCHE Claude's avatar
MARCHE Claude committed
375
  (forall id: mident. type_value (get_env id sigma) = get_reftype id sigmat) /\
MARCHE Claude's avatar
MARCHE Claude committed
376
377
  (forall id: ident. type_value (get_stack id pi) = get_vartype id pit)

378
lemma type_inversion : forall v "induction":value.
MARCHE Claude's avatar
MARCHE Claude committed
379
   match (type_value v) with
380
381
382
    | TYbool -> exists b: bool. v = Vbool b
    | TYint -> exists n: int. v = Vint n
    | TYunit -> v = Vvoid
MARCHE Claude's avatar
MARCHE Claude committed
383
  end
384
385
386
387

lemma eval_type_term:
  forall t:term, sigma:env, pi:stack, sigmat:type_env, pit:type_stack, ty:datatype.
    compatible_env sigma sigmat pi pit ->
MARCHE Claude's avatar
MARCHE Claude committed
388
    type_term sigmat pit t ty -> type_value (eval_term sigma pi t) = ty
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410

lemma type_preservation :
  forall s1 s2:stmt, sigma1 sigma2:env, pi1 pi2:stack,
         sigmat:type_env, pit:type_stack.
     type_stmt sigmat pit s1 /\
     compatible_env sigma1 sigmat pi1 pit /\
     one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
     type_stmt sigmat pit s2 /\
     compatible_env sigma2 sigmat pi2 pit

end



(** {2 Problématique des variables fraîches} *)


theory FreshVariables

use import SemOp
use import list.Append

411
412
413
414
415
416
lemma Cons_append: forall a: 'a, l1 l2: list 'a.
  Cons a (l1 ++ l2) = (Cons a l1) ++ l2

lemma Append_nil_l:
  forall l: list 'a. Nil ++ l = l

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

420
function msubst_term (t:term) (x:mident) (v:ident) : term =
421
422
  match t with
  | Tvalue _ | Tvar _  -> t
423
  | Tderef y -> if x = y then Tvar v else t
424
  | Tbin t1 op t2  ->
425
      Tbin (msubst_term t1 x v) op (msubst_term t2 x v)
426
427
428
429
430
431
432
433
434
435
436
437
438
  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


MARCHE Claude's avatar
MARCHE Claude committed
439
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
Claude Marche's avatar
Claude Marche committed
440
predicate fresh_in_term (id:ident) (t:term) =
MARCHE Claude's avatar
MARCHE Claude committed
441
  match t with
MARCHE Claude's avatar
MARCHE Claude committed
442
  | Tvalue _ | Tderef _  -> true
Claude Marche's avatar
Claude Marche committed
443
444
  | Tvar i  -> id <> i
  | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2
MARCHE Claude's avatar
MARCHE Claude committed
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
  end


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



460
(* Needed for monotonicity and wp_reduction *)
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
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

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_swap_term:
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)

MARCHE Claude's avatar
MARCHE Claude committed
479
lemma eval_swap_gen:
480
481
482
483
484
  forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
    eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)

MARCHE Claude's avatar
MARCHE Claude committed
485
486
487
488
489
490
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)

491
492
493
494
495
496
497
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

 (* Need it for monotonicity*)
lemma eval_change_free :
MARCHE Claude's avatar
MARCHE Claude committed
498
  forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
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
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
    fresh_in_fmla id f ->
    (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)



end


(** {2 Hoare logic} *)

theory HoareLogic

use import Syntax
use import SemOp
use import FreshVariables

(* Used by Hoare_logic/seq_rule*)
  lemma many_steps_seq:
    forall sigma1 sigma3:env, pi1 pi3:stack, s1 s2:stmt, n:int.
      many_steps sigma1 pi1 (Sseq s1 s2) sigma3 pi3 Sskip n ->
      exists sigma2:env, pi2:stack, n1 n2:int.
        many_steps sigma1 pi1 s1 sigma2 pi2 Sskip n1 /\
        many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2 /\
        n = 1 + n1 + n2



(** partial correctness *)
predicate valid_triple (p:fmla) (s:stmt) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      forall sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n ->
          eval_fmla sigma' pi' q

(*** total correctness *)
predicate total_valid_triple (p:fmla) (s:stmt) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      exists sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n /\
        eval_fmla sigma' pi' q






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

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

lemma skip_rule:
  forall q:fmla. valid_triple q Sskip q

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)) (Sassign x t) p

lemma seq_rule:
  forall p q r:fmla, s1 s2:stmt.
  valid_triple p s1 r /\ valid_triple r s2 q ->
  valid_triple p (Sseq s1 s2) q

lemma if_rule:
  forall t:term, p q:fmla, s1 s2:stmt.
  valid_triple (Fand p (Fterm t)) s1 q /\
  valid_triple (Fand p (Fnot (Fterm t))) s2 q ->
  valid_triple p (Sif t s1 s2) q

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

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

lemma while_rule:
  forall e:term, inv:fmla, i:stmt.
  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 SemOp
use import Typing
use import TypingAndSemantics
use import FreshVariables


602
function fresh_from (f:fmla) : ident
603
604

  (* Need it for monotonicity*)
605
606
axiom fresh_from_fmla: forall f:fmla.
fresh_in_fmla (fresh_from f) f
607

608
609
610
611
  (* intention:
       abstract_effects s f = "forall w. f"
     avec w = writes(s)
  *)
612
613
  function abstract_effects (s:stmt) (f:fmla) : fmla

614
615
616
617
618
  (* hypothese 1: si
       sigma, pi |= forall w. f
     alors
       sigma, pi |= f
  *)
619
  axiom abstract_effects_specialize :
620
621
622
623
     forall sigma:env, pi:stack, s:stmt, f:fmla.
        eval_fmla sigma pi (abstract_effects s f) ->
        eval_fmla sigma pi f

624
  (* hypothese 2: si
MARCHE Claude's avatar
MARCHE Claude committed
625
626
627
628
629
630
631
632
633
634
635
       sigma, pi |= (forall w, p) /\ (forall w, q)
     alors
       sigma, pi |= forall w, (f /\ q)
  *)
  axiom abstract_effects_distrib_conj :
     forall s:stmt, p q:fmla, sigma:env, pi:stack.
       eval_fmla sigma pi (abstract_effects s p) /\
       eval_fmla sigma pi (abstract_effects s q) ->
         eval_fmla sigma pi (abstract_effects s (Fand p q))

  (* hypothese 3: si
636
637
638
639
640
641
642
643
644
       |= p -> q
     alors
       |= (forall w, p) -> (forall w, q)

     remarque : il est essentiel de parler de validité dans tous les etats:
     on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (forall w, p) -> (forall w, q)
645

646
647
648
649
650
651
652
653
654
655
656
657
658
     contre-exemple: sigma(x) = 42 alors true -> x=42
        mais on n'a
             (forall x, true) -> (forall  x, x=42)
  *)

  axiom abstract_effects_monotonic :
     forall s:stmt, p q:fmla.
        valid_fmla (Fimplies p q) ->
        forall sigma:env, pi:stack.
           eval_fmla sigma pi (abstract_effects s p) ->
           eval_fmla sigma pi (abstract_effects s q)

function wp (s:stmt) (q:fmla) : fmla =
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
    match s with
    | Sskip -> q
    | Sassert f ->
        (* asymmetric and *)
        Fand f (Fimplies f q)
    | Sseq s1 s2 -> wp s1 (wp s2 q)
    | Sassign x t ->
        let id = fresh_from q in
        Flet id t (msubst q x id)
    | Sif t s1 s2 ->
        Fand (Fimplies (Fterm t) (wp s1 q))
             (Fimplies (Fnot (Fterm t)) (wp s2 q))
    | Swhile cond inv body ->
        Fand inv
          (abstract_effects body
            (Fand
              (Fimplies (Fand (Fterm cond) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm cond)) inv) q)))

    end

  axiom abstract_effects_writes :
     forall sigma:env, pi:stack, s:stmt, q:fmla.
        eval_fmla sigma pi (abstract_effects s q) ->
        eval_fmla sigma pi (wp s (abstract_effects s q))

  lemma monotonicity:
    forall s:stmt, p q:fmla.
      valid_fmla (Fimplies p q)
Claude Marche's avatar
Claude Marche committed
688
     -> valid_fmla (Fimplies (wp s p) (wp s q) )
689

690
691
692
693
694
695
 (* remarque l'ordre des quantifications est essentiel, on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (wp s p) -> (wp s q)

     meme contre-exemple: sigma(x) = 42 alors true -> x=42
Claude Marche's avatar
Claude Marche committed
696
        mais
697
698
699
700
          wp (x := 7) true = true
          wp (x := 7) x=42 = 7=42
  *)

701
702
703
704
  lemma distrib_conj:
    forall s:stmt, sigma:env, pi:stack, p q:fmla.
     (eval_fmla sigma pi (wp s p)) /\
     (eval_fmla sigma pi (wp s q)) ->
Claude Marche's avatar
Claude Marche committed
705
     eval_fmla sigma pi (wp s (Fand p q))
706

MARCHE Claude's avatar
MARCHE Claude committed
707
  lemma wp_preserved_by_reduction:
708
709
710
711
712
713
714
715
716
717
718
719
    forall sigma sigma':env, pi pi':stack, s s':stmt.
    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)

  lemma progress:
    forall s:stmt, sigma:env, pi:stack,
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      eval_fmla sigma pi (wp s q) ->
720
      s <> Sskip -> reductible sigma pi s
721
722
723
724

  (** {3 main soundness result} *)

  lemma wp_soundness:
725
    forall n:int, sigma sigma':env, pi pi':stack, s s':stmt,
726
727
728
729
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      many_steps sigma pi s sigma' pi' s' n /\
730
      not (reductible sigma' pi' s') /\
731
732
733
734
735
736
737
738
739
740
741
      eval_fmla sigma pi (wp s q) ->
      s' = Sskip /\ eval_fmla sigma' pi' q

end


(***
Local Variables:
compile-command: "why3ide blocking_semantics5.mlw"
End:
*)