wp3.mlw 13.8 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
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181

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

type ident = int

constant result : ident = (-1)

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
  | Fforall ident datatype fmla

use map.Map as IdMap
type env = IdMap.map ident value

(** 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
  | _,_ -> Vbool False
  end

function get_env (i:ident) (e:env) : value = IdMap.get e i

function eval_term (sigma:env) (pi:env) (t:term) : value =
  match t with
  | Tvalue v -> v
  | Tvar id -> get_env 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:env) (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 (IdMap.set pi x (eval_term sigma pi t)) f
  | Fforall x TYint f ->
     forall n:int. eval_fmla sigma (IdMap.set pi x (Vint n)) f
  | Fforall x TYbool f ->
     forall b:bool.
        eval_fmla sigma (IdMap.set pi x (Vbool b)) f
  | Fforall x TYunit f ->
        eval_fmla sigma (IdMap.set pi x Vvoid) f
  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
  | Tderef x -> if r=x then Tvar v else e
  | Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v)
  end

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 pi:env, 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 (IdMap.get pi v)) pi e

lemma eval_term_change_free :
  forall t:term, sigma pi:env, id:ident, v:value.
    fresh_in_term id t ->
    eval_term sigma (IdMap.set pi id v) 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


lemma eval_subst:
  forall f:fmla, sigma pi:env, x:ident, v:ident.
    fresh_in_fmla v f ->
    (eval_fmla sigma pi (subst f x v) <->
     eval_fmla (IdMap.set sigma x (IdMap.get pi v)) pi f)

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

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

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

constant void : expr = Evalue Vvoid

(*
lemma check_skip:
  forall s:stmt. s=Sskip \/s<>Sskip
*)

(** small-steps semantics for statements *)

inductive one_step env env expr env env expr =

  | one_step_assign_ctxt:
      forall sigma pi sigma' pi':env, 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:
182
      forall sigma pi:env, x:ident, v:value.
MARCHE Claude's avatar
MARCHE Claude committed
183
184
185
186
187
188
189
190
191
        one_step sigma pi (Eassign x (Evalue v))
                 (IdMap.set sigma x v) pi void

  | one_step_seq_ctxt:
      forall sigma pi sigma' pi':env, 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:
MARCHE Claude's avatar
MARCHE Claude committed
192
      forall sigma pi:env, e:expr.
MARCHE Claude's avatar
MARCHE Claude committed
193
194
195
196
197
198
199
200
201
202
203
204
        one_step sigma pi (Eseq void e) sigma pi e

  | one_step_let_ctxt:
      forall sigma pi sigma' pi':env, 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 pi:env, id:ident, v:value, e:expr.
        one_step sigma pi (Elet id (Evalue v) e) sigma (IdMap.set pi id v) e

  | one_step_if_ctxt:
MARCHE Claude's avatar
MARCHE Claude committed
205
      forall sigma pi sigma' pi':env, e1 e1' e2 e3:expr.
MARCHE Claude's avatar
MARCHE Claude committed
206
207
208
209
        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:
MARCHE Claude's avatar
MARCHE Claude committed
210
      forall sigma pi:env, e1 e2:expr.
MARCHE Claude's avatar
MARCHE Claude committed
211
212
213
        one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1

  | one_step_if_false:
MARCHE Claude's avatar
MARCHE Claude committed
214
      forall sigma pi:env, e1 e2:expr.
MARCHE Claude's avatar
MARCHE Claude committed
215
216
217
218
219
220
221
222
223
        one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2

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

  | one_step_while:
      forall sigma pi:env, e:expr, inv:fmla, e':expr.
Andrei Paskevich's avatar
Andrei Paskevich committed
224
        one_step sigma pi (Ewhile e inv e') sigma pi
MARCHE Claude's avatar
MARCHE Claude committed
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
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
292
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
327
328
329
330
331
332
333
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
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
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
        (Eif e (Eseq e' (Ewhile e inv e')) void)

(***

  lemma progress:
    forall s:state, i:expr.
      i <> Sskip ->
      exists s':state, i':expr. one_step s i s' i'

*)

 (** many steps of execution *)

 inductive many_steps env env expr env env expr int =
   | many_steps_refl:
     forall sigma pi:env, i:expr. many_steps sigma pi i sigma pi i 0
   | many_steps_trans:
     forall sigma1 pi1 sigma2 pi2 sigma3 pi3:env, i1 i2 i3:expr, n:int.
       one_step sigma1 pi1 i1 sigma2 pi2 i2 ->
       many_steps sigma2 pi2 i2 sigma3 pi3 i3 n ->
       many_steps sigma1 pi1 i1 sigma3 pi3 i3 (n+1)

lemma steps_non_neg:
  forall sigma1 pi1 sigma2 pi2:env, i1 i2:expr, n:int.
    many_steps sigma1 pi1 i1 sigma2 pi2 i2 n -> n >= 0

lemma many_steps_seq:
  forall sigma1 pi1 sigma3 pi3:env, e1 e2:expr, n:int.
    many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3 void n ->
    exists sigma2 pi2:env, 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 pi1 sigma3 pi3:env, id:ident, e1 e2:expr, v2:value, n:int.
    many_steps sigma1 pi1 (Elet id e1 e2) sigma3 pi3 (Evalue v2) n ->
    exists sigma2 pi2:env, v1:value, n1 n2:int.
      many_steps sigma1 pi1 e1 sigma2 pi2 (Evalue v1) n1 /\
      many_steps sigma2 (IdMap.set pi2 id v1) e2 sigma3 pi3 (Evalue v2) n2 /\
      n = 1 + n1 + n2



predicate valid_fmla (p:fmla) = forall sigma pi:env. eval_fmla sigma pi p

(** {3 Hoare triples} *)

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

(*** total correctness *)
(***
predicate total_valid_triple (p:fmla) (i:expr) (q:fmla) =
    forall s:state. eval_fmla s p ->
      exists s':state, n:int. many_steps s i s' Sskip n /\
        eval_fmla s' q
*)

end


theory TestSemantics

use import ImpExpr

function my_sigma : env = IdMap.const (Vint 0)
function my_pi : env = IdMap.const (Vint 42)

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 :
  eval_term my_sigma my_pi (Tvar 0) = Vint 42

goal Test42expr :
  many_steps my_sigma my_pi (Evar 0) my_sigma my_pi (Evalue (Vint 42)) 1

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

goal Test0expr :
  many_steps my_sigma my_pi (Ederef 0) my_sigma my_pi (Evalue (Vint 0)) 1

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

goal Test55expr :
  many_steps my_sigma my_pi (Ebin (Evar 0) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 3

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

goal If42 :
    let x = 0 in
    forall sigma1 pi1 sigma2 pi2:env, 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.
  fresh_in_fmla result p ->
  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} *)

(*
module WP

use import Imp

use set.Set

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'


predicate expr_writes (i:expr) (w:Set.set ident) =
  match i with
  | Sskip | Sassert _ -> true
  | Sassign id _ -> Set.mem id w
  | Sseq s1 s2 | Sif _ s1 s2 -> expr_writes s1 w /\ expr_writes s2 w
  | Swhile _ _ s -> expr_writes s w
  end


  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 pi sigma' pi':env, 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 pi:env. 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))
Andrei Paskevich's avatar
Andrei Paskevich committed
503
                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
MARCHE Claude's avatar
MARCHE Claude committed
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518

    end
    { valid_triple result i q }


end
*)


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