wp.mlw 8.42 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4 5 6

theory Imp

(* terms and formulas *)

MARCHE Claude's avatar
MARCHE Claude committed
7 8
type datatype = Tint | Tbool

MARCHE Claude's avatar
MARCHE Claude committed
9 10 11
type operator = Oplus | Ominus | Omult | Ole

type ident = int
MARCHE Claude's avatar
MARCHE Claude committed
12 13 14

type term =
  | Tconst int
MARCHE Claude's avatar
MARCHE Claude committed
15
  | Tvar ident
MARCHE Claude's avatar
MARCHE Claude committed
16
  | Tderef ident
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21 22 23
  | Tbin term operator term

type fmla =
  | Fterm term
  | Fand fmla fmla
  | Fnot fmla
  | Fimplies fmla fmla
MARCHE Claude's avatar
MARCHE Claude committed
24 25
  | Flet ident term fmla
  | Fforall ident datatype fmla
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29 30 31 32 33 34 35

(* program states: 2 stack env for refs and local vars  *)

use import int.Int
use import bool.Bool

type value =
  | Vint int
  | Vbool bool

MARCHE Claude's avatar
MARCHE Claude committed
36 37
use map.Map as IdMap
type var_env = IdMap.map ident value
MARCHE Claude's avatar
MARCHE Claude committed
38 39 40
type ref_env = IdMap.map ident value

type state = {| var_env : var_env; ref_env: ref_env |}
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43

(* semantics of formulas *)

MARCHE Claude's avatar
MARCHE Claude committed
44
predicate eval_bin (x:value) (op:operator) (y:value) (res:value) =
MARCHE Claude's avatar
MARCHE Claude committed
45
  match x,y with
MARCHE Claude's avatar
MARCHE Claude committed
46
  | Vint x,Vint y ->
MARCHE Claude's avatar
MARCHE Claude committed
47
     match op with
MARCHE Claude's avatar
MARCHE Claude committed
48 49 50
     | Oplus -> res = Vint (x+y)
     | Ominus -> res = Vint (x-y)
     | Omult -> res = Vint (x*y)
MARCHE Claude's avatar
MARCHE Claude committed
51
     | Ole -> res = Vbool (if x <= y then True else False)
MARCHE Claude's avatar
MARCHE Claude committed
52
     end
MARCHE Claude's avatar
MARCHE Claude committed
53
  | _,_ -> false
MARCHE Claude's avatar
MARCHE Claude committed
54 55
  end

MARCHE Claude's avatar
MARCHE Claude committed
56
(*
MARCHE Claude's avatar
MARCHE Claude committed
57
inductive get_env (i:int) (env:list value) (res:value) =
MARCHE Claude's avatar
MARCHE Claude committed
58
  | Get_first:
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62
    forall x:value, l:list value. get_env 0 (Cons x l) x
  | Get_next:
    forall i:int, x r:value, l:list value. i > 0 ->
      get_env (i-1) l r -> get_env i (Cons x l) x
MARCHE Claude's avatar
MARCHE Claude committed
63
*)
MARCHE Claude's avatar
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68
predicate get_refenv (i:ident) (e:ref_env) (r:value) =
    IdMap.get e i = r

inductive eval_term state term value =
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72
  | eval_const :
      forall s:state, n:int. eval_term s (Tconst n) (Vint n)
  | eval_var :
      forall s:state, i:int, res:value.
MARCHE Claude's avatar
MARCHE Claude committed
73
        get_refenv i (var_env s) res -> eval_term s (Tvar i) res
MARCHE Claude's avatar
MARCHE Claude committed
74
  | eval_deref :
MARCHE Claude's avatar
MARCHE Claude committed
75 76
      forall s:state, i:ident, res:value.
        get_refenv i (ref_env s) res -> eval_term s (Tderef i) res
MARCHE Claude's avatar
MARCHE Claude committed
77 78 79 80
  | eval_bin :
      forall s:state, op:operator, t1 t2:term, r1 r2 r:value.
        eval_term s t1 r1 -> eval_term s t2 r2 ->
        eval_bin r1 op r2 r -> eval_term s (Tbin t1 op t2) r
MARCHE Claude's avatar
MARCHE Claude committed
81

MARCHE Claude's avatar
MARCHE Claude committed
82
  function my_state :state =
MARCHE Claude's avatar
MARCHE Claude committed
83 84
    {| var_env = IdMap.const (Vint 42);
       ref_env = IdMap.const (Vint 0) |}
MARCHE Claude's avatar
MARCHE Claude committed
85 86

  goal Test13 :
MARCHE Claude's avatar
MARCHE Claude committed
87
    eval_term my_state (Tconst 13) (Vint 13)
MARCHE Claude's avatar
MARCHE Claude committed
88 89

  goal Test42 :
MARCHE Claude's avatar
MARCHE Claude committed
90
    eval_term my_state (Tvar 0) (Vint 42)
MARCHE Claude's avatar
MARCHE Claude committed
91 92

  goal Test55 :
MARCHE Claude's avatar
MARCHE Claude committed
93
    eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) (Vint 55)
MARCHE Claude's avatar
MARCHE Claude committed
94

MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
inductive eval_fmla state fmla bool =
  | eval_term:
    forall s:state, t:term, b:bool.
      eval_term s t (Vbool b) -> eval_fmla s (Fterm t) b
  | eval_and:
    forall s:state, f1 f2:fmla, b1 b2:bool.
      eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
      eval_fmla s (Fand f1 f2) (andb b1 b2)
  | eval_not:
    forall s:state, f:fmla, b:bool.
      eval_fmla s f b -> eval_fmla s (Fnot f) (notb b)
  | eval_impl:
    forall s:state, f1 f2:fmla, b1 b2:bool.
      eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
      eval_fmla s (Fimplies f1 f2) (implb b1 b2)
  | eval_forall_int_true:
MARCHE Claude's avatar
MARCHE Claude committed
111
      forall s:state, x:ident, f:fmla.
MARCHE Claude's avatar
MARCHE Claude committed
112 113 114
        (* problem: qu'est-ce qui garanti que s.var_env a exactement
           autant de debruijn que f ? *)
        (forall n:int. eval_fmla
MARCHE Claude's avatar
MARCHE Claude committed
115 116
          {| var_env = IdMap.set s.var_env x (Vint n);
             ref_env = s.ref_env |}
MARCHE Claude's avatar
MARCHE Claude committed
117
          f True) ->
MARCHE Claude's avatar
MARCHE Claude committed
118
        eval_fmla s (Fforall x Tint f) True
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121

(* substitution *) 

MARCHE Claude's avatar
MARCHE Claude committed
122
function subst_term (e:term) (x:ident) (t:term) : term =
MARCHE Claude's avatar
MARCHE Claude committed
123
  match e with
MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127
  | Tconst _ -> e
  | Tvar _ -> e
  | Tderef y -> if x=y then t else e
  | Tbin e1 op e2 -> Tbin (subst_term e1 x t) op (subst_term e2 x t)
MARCHE Claude's avatar
MARCHE Claude committed
128 129
  end

MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133 134 135 136
lemma eval_subst_term:
  forall s:state, e:term, x:ident, t:term, r v:value.
    eval_term s t r ->
    eval_term s (subst_term e x t) v <->
      eval_term {| var_env = s.var_env;
                   ref_env = (IdMap.set s.ref_env x r) |}
                 e v
MARCHE Claude's avatar
MARCHE Claude committed
137

MARCHE Claude's avatar
MARCHE Claude committed
138
function subst (f:fmla) (x:ident) (t:term) : fmla =
MARCHE Claude's avatar
MARCHE Claude committed
139
  match f with
MARCHE Claude's avatar
MARCHE Claude committed
140
  | Fterm e -> Fterm (subst_term e x t)
MARCHE Claude's avatar
MARCHE Claude committed
141 142 143
  | Fand f1 f2 -> Fand (subst f1 x t) (subst f2 x t)
  | Fnot f -> Fnot (subst f x t)
  | Fimplies f1 f2 -> Fimplies (subst f1 x t) (subst f2 x t)
MARCHE Claude's avatar
MARCHE Claude committed
144 145
  | Flet y t' f -> Flet y t' (subst f x t)
  | Fforall y ty f -> Fforall y ty (subst f x t)
MARCHE Claude's avatar
MARCHE Claude committed
146 147 148
  end

lemma eval_subst:
MARCHE Claude's avatar
MARCHE Claude committed
149 150 151 152 153
  forall s:state, f:fmla, x:ident, t:term, r:value, b:bool.
    eval_fmla s (subst f x t) b <->
    eval_fmla {| var_env = s.var_env;
                 ref_env = (IdMap.set s.ref_env x r) |}
              f b
MARCHE Claude's avatar
MARCHE Claude committed
154

MARCHE Claude's avatar
MARCHE Claude committed
155 156 157 158 159

(* statements *)

type stmt =
  | Sskip
MARCHE Claude's avatar
MARCHE Claude committed
160
  | Sassign ident term
MARCHE Claude's avatar
MARCHE Claude committed
161 162
  | Sseq stmt stmt
  | Sif term stmt stmt
MARCHE Claude's avatar
MARCHE Claude committed
163
  | Swhile term fmla stmt
MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167 168 169 170 171 172

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

(* small-steps semantics for statements *)

inductive one_step state stmt state stmt =

  | one_step_assign:
MARCHE Claude's avatar
MARCHE Claude committed
173 174
      forall s:state, x:ident, e:term, r:value.
        eval_term s e r ->
MARCHE Claude's avatar
MARCHE Claude committed
175
        one_step s (Sassign x e)
MARCHE Claude's avatar
MARCHE Claude committed
176 177 178
                 {| var_env = s.var_env;
                    ref_env = (IdMap.set s.ref_env x r) |}
                 Sskip
MARCHE Claude's avatar
MARCHE Claude committed
179 180 181 182 183 184 185 186 187 188 189

  | one_step_seq:
      forall s s':state, i1 i1' i2:stmt.
        one_step s i1 s' i1' ->
          one_step s (Sseq i1 i2) s' (Sseq i1' i2)

  | one_step_seq_skip:
      forall s:state, i:stmt.
        one_step s (Sseq Sskip i) s i

  | one_step_if_true:
MARCHE Claude's avatar
MARCHE Claude committed
190 191
      forall s:state, e:term, i1 i2:stmt.
        eval_term s e (Vbool True) ->
MARCHE Claude's avatar
MARCHE Claude committed
192 193 194
          one_step s (Sif e i1 i2) s i1

  | one_step_if_false:
MARCHE Claude's avatar
MARCHE Claude committed
195 196
      forall s:state, e:term, i1 i2:stmt.
        eval_term s e (Vbool False) ->
MARCHE Claude's avatar
MARCHE Claude committed
197 198 199
          one_step s (Sif e i1 i2) s i2

  | one_step_while_true:
MARCHE Claude's avatar
MARCHE Claude committed
200 201 202 203
      forall s:state, e:term, inv:fmla, i:stmt.
        eval_fmla s inv True ->
        eval_term s e (Vbool True) ->
          one_step s (Swhile e inv i) s (Sseq i (Swhile e inv i))
MARCHE Claude's avatar
MARCHE Claude committed
204 205

  | one_step_while_false:
MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209
      forall s:state, e:term, inv:fmla, i:stmt.
        eval_fmla s inv True ->
        eval_term s e (Vbool False) ->
          one_step s (Swhile e inv i) s Sskip
MARCHE Claude's avatar
MARCHE Claude committed
210 211

  goal Ass42 :
MARCHE Claude's avatar
MARCHE Claude committed
212
    let x = 0 in
MARCHE Claude's avatar
MARCHE Claude committed
213
    forall s':state.
MARCHE Claude's avatar
MARCHE Claude committed
214 215
      one_step my_state (Sassign x (Tconst 42)) s' Sskip ->
        IdMap.get s'.ref_env x = Vint 42
MARCHE Claude's avatar
MARCHE Claude committed
216 217

  goal If42 :
MARCHE Claude's avatar
MARCHE Claude committed
218
    let x = 0 in
MARCHE Claude's avatar
MARCHE Claude committed
219
    forall s1 s2:state, i:stmt.
MARCHE Claude's avatar
MARCHE Claude committed
220 221 222 223
      one_step my_state
        (Sif (Tbin (Tvar x) Ole (Tconst 10))
             (Sassign x (Tconst 13))
             (Sassign x (Tconst 42)))
MARCHE Claude's avatar
MARCHE Claude committed
224 225
        s1 i ->
      one_step s1 i s2 Sskip ->
MARCHE Claude's avatar
MARCHE Claude committed
226 227 228
        IdMap.get s2.ref_env x = Vint 42

(*
MARCHE Claude's avatar
MARCHE Claude committed
229 230 231 232 233 234

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

MARCHE Claude's avatar
MARCHE Claude committed
235
*)
MARCHE Claude's avatar
MARCHE Claude committed
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

 (* many steps of execution *)

 inductive many_steps state stmt state stmt int =
   | many_steps_refl:
     forall s:state, i:stmt. many_steps s i s i 0
   | many_steps_trans:
     forall s1 s2 s3:state, i1 i2 i3:stmt, n:int.
       one_step s1 i1 s2 i2 ->
       many_steps s2 i2 s3 i3 n ->
       many_steps s1 i1 s3 i3 (n+1)

lemma steps_non_neg:
  forall s1 s2:state, i1 i2:stmt, n:int.
    many_steps s1 i1 s2 i2 n -> n >= 0

lemma many_steps_seq:
  forall s1 s3:state, i1 i2:stmt, n:int.
    many_steps s1 (Sseq i1 i2) s3 Sskip n ->
    exists s2:state, n1 n2:int.
      many_steps s1 i1 s2 Sskip n1 /\
      many_steps s2 i2 s3 Sskip n2 /\
      n = 1 + n1 + n2


MARCHE Claude's avatar
MARCHE Claude committed
261
predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p True
MARCHE Claude's avatar
MARCHE Claude committed
262 263 264 265

(* Hoare triples *)

predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
MARCHE Claude's avatar
MARCHE Claude committed
266
    forall s:state. eval_fmla s p True ->
MARCHE Claude's avatar
MARCHE Claude committed
267
      forall s':state, n:int. many_steps s i s' Sskip n ->
MARCHE Claude's avatar
MARCHE Claude committed
268
        eval_fmla s' q True
MARCHE Claude's avatar
MARCHE Claude committed
269 270 271 272 273 274 275

(* Hoare logic rules *)

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

lemma assign_rule:
MARCHE Claude's avatar
MARCHE Claude committed
276
  forall q:fmla, x:ident, e:term.
MARCHE Claude's avatar
MARCHE Claude committed
277 278 279 280 281 282 283 284
  valid_triple (subst q x e) (Sassign x e) q

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

lemma if_rule:
MARCHE Claude's avatar
MARCHE Claude committed
285
  forall e:term, p q:fmla, i1 i2:stmt.
MARCHE Claude's avatar
MARCHE Claude committed
286 287 288 289 290
  valid_triple (Fand p (Fterm e)) i1 q /\
  valid_triple (Fand p (Fnot (Fterm e))) i2 q ->
  valid_triple p (Sif e i1 i2) q

lemma while_rule:
MARCHE Claude's avatar
MARCHE Claude committed
291
  forall e:term, inv:fmla, i:stmt.
MARCHE Claude's avatar
MARCHE Claude committed
292
  valid_triple (Fand (Fterm e) inv) i inv ->
MARCHE Claude's avatar
MARCHE Claude committed
293
  valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)
MARCHE Claude's avatar
MARCHE Claude committed
294 295 296 297 298 299 300 301 302 303 304 305

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



end

MARCHE Claude's avatar
MARCHE Claude committed
306 307


MARCHE Claude's avatar
MARCHE Claude committed
308

309 310
module WP

MARCHE Claude's avatar
MARCHE Claude committed
311
  use import Imp
312 313 314 315 316 317 318 319 320 321

  let rec wp (i:stmt) (q:fmla) =
    { true }
    match i with
    | Sskip -> q
    | Sseq i1 i2 -> wp i1 (wp i2 q)
    | Sassign x e -> subst q x e
    | Sif e i1 i2 ->
        Fand (Fimplies (Fterm e) (wp i1 q))
             (Fimplies (Fnot (Fterm e)) (wp i2 q))
MARCHE Claude's avatar
MARCHE Claude committed
322 323
    | Swhile e inv i ->
        Fand inv
MARCHE Claude's avatar
MARCHE Claude committed
324
          ((*Fforall*) (Fand
MARCHE Claude's avatar
MARCHE Claude committed
325 326 327
                     (Fimplies (Fand (Fterm e) inv) (wp i inv))
                     (Fimplies (Fand (Fnot (Fterm e)) inv) q))) 

328 329 330 331 332 333 334 335 336 337 338 339 340
    end
    { valid_triple result i q }

end



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