examples/WP_revisited/wp2.mlw

   1
   2 (** {1 A certified WP calculus} *)
   3
   4 (** {2 A simple imperative language, syntax and semantics} *)
   5
   6 theory Imp
   7
   8 (** terms and formulas *)
   9
  10 type datatype = Tint | Tbool
  11
  12 type operator = Oplus | Ominus | Omult | Ole
  13
  14 type ident = int
  15
  16 type term =
  17   | Tconst int
  18   | Tvar ident
  19   | Tderef ident
  20   | Tbin term operator term
  21
  22 type fmla =
  23   | Fterm term
  24   | Fand fmla fmla
  25   | Fnot fmla
  26   | Fimplies fmla fmla
  27   | Flet ident term fmla
  28   | Fforall ident datatype fmla
  29
  30 use int.Int
  31 use bool.Bool
  32
  33 type value =
  34   | Vint int
  35   | Vbool bool
  36
  37 use map.Map as IdMap
  38 type env = IdMap.map ident value
  39
  40 (** semantics of formulas *)
  41
  42 function eval_bin (x:value) (op:operator) (y:value) : value =
  43   match x,y with
  44   | Vint x,Vint y ->
  45      match op with
  46      | Oplus -> Vint (x+y)
  47      | Ominus -> Vint (x-y)
  48      | Omult -> Vint (x*y)
  49      | Ole -> Vbool (if x <= y then True else False)
  50      end
  51   | _,_ -> Vbool False
  52   end
  53
  54 function get_env (i:ident) (e:env) : value = IdMap.get e i
  55
  56 function eval_term (sigma:env) (pi:env) (t:term) : value =
  57   match t with
  58   | Tconst n -> Vint n
  59   | Tvar id -> get_env id pi
  60   | Tderef id -> get_env id sigma
  61   | Tbin t1 op t2 ->
  62      eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
  63   end
  64
  65 predicate eval_fmla (sigma:env) (pi:env) (f:fmla) =
  66   match f with
  67   | Fterm t -> eval_term sigma pi t = Vbool True
  68   | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
  69   | Fnot f -> not (eval_fmla sigma pi f)
  70   | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
  71   | Flet x t f ->
  72       eval_fmla sigma (IdMap.set pi x (eval_term sigma pi t)) f
  73   | Fforall x Tint f ->
  74      forall n:int. eval_fmla sigma (IdMap.set pi x (Vint n)) f
  75   | Fforall x Tbool f ->
  76      forall b:bool.
  77         eval_fmla sigma (IdMap.set pi x (Vbool b)) f
  78   end
  79
  80 (** substitution of a reference `r` by a logic variable `v`
  81    warning: proper behavior only guaranted if `v` is fresh *)
  82
  83 let rec function subst_term (e:term) (r:ident) (v:ident) : term =
  84   match e with
  85   | Tconst _ -> e
  86   | Tvar _ -> e
  87   | Tderef x -> if r=x then Tvar v else e
  88   | Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v)
  89   end
  90
  91 predicate fresh_in_term (id:ident) (t:term) =
  92   match t with
  93   | Tconst _ -> true
  94   | Tvar v -> id <> v
  95   | Tderef _ -> true
  96   | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2
  97   end
  98
  99 lemma eval_subst_term:
 100   forall sigma pi:env, e:term, x:ident, v:ident.
 101     fresh_in_term v e ->
 102     eval_term sigma pi (subst_term e x v) =
 103     eval_term (IdMap.set sigma x (IdMap.get pi v)) pi e
 104
 105 lemma eval_term_change_free :
 106   forall t:term, sigma pi:env, id:ident, v:value.
 107     fresh_in_term id t ->
 108     eval_term sigma (IdMap.set pi id v) t = eval_term sigma pi t
 109
 110 predicate fresh_in_fmla (id:ident) (f:fmla) =
 111   match f with
 112   | Fterm e -> fresh_in_term id e
 113   | Fand f1 f2   | Fimplies f1 f2 ->
 114       fresh_in_fmla id f1 /\ fresh_in_fmla id f2
 115   | Fnot f -> fresh_in_fmla id f
 116   | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
 117   | Fforall y _ f -> id <> y /\ fresh_in_fmla id f
 118   end
 119
 120 let rec function subst (f:fmla) (x:ident) (v:ident) : fmla =
 121   match f with
 122   | Fterm e -> Fterm (subst_term e x v)
 123   | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
 124   | Fnot f -> Fnot (subst f x v)
 125   | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v)
 126   | Flet y t f -> Flet y (subst_term t x v) (subst f x v)
 127   | Fforall y ty f -> Fforall y ty (subst f x v)
 128   end
 129
 130
 131 lemma eval_subst:
 132   forall f:fmla, sigma pi:env, x:ident, v:ident.
 133     fresh_in_fmla v f ->
 134     (eval_fmla sigma pi (subst f x v) <->
 135      eval_fmla (IdMap.set sigma x (IdMap.get pi v)) pi f)
 136
 137 lemma eval_swap:
 138   forall f:fmla, sigma pi:env, id1 id2:ident, v1 v2:value.
 139     id1 <> id2 ->
 140     (eval_fmla sigma (IdMap.set (IdMap.set pi id1 v1) id2 v2) f <->
 141     eval_fmla sigma (IdMap.set (IdMap.set pi id2 v2) id1 v1) f)
 142
 143 lemma eval_change_free :
 144   forall f:fmla, sigma pi:env, id:ident, v:value.
 145     fresh_in_fmla id f ->
 146     (eval_fmla sigma (IdMap.set pi id v) f <-> eval_fmla sigma pi f)
 147
 148 (* statements *)
 149
 150 type stmt =
 151   | Sskip
 152   | Sassign ident term
 153   | Sseq stmt stmt
 154   | Sif term stmt stmt
 155   | Sassert fmla
 156   | Swhile term fmla stmt
 157
 158 lemma check_skip:
 159   forall s:stmt. s=Sskip \/s<>Sskip
 160
 161 (** small-steps semantics for statements *)
 162
 163 inductive one_step env env stmt env env stmt =
 164
 165   | one_step_assign:
 166       forall sigma pi:env, x:ident, e:term.
 167         one_step sigma pi (Sassign x e)
 168                  (IdMap.set sigma x (eval_term sigma pi e)) pi
 169                  Sskip
 170
 171   | one_step_seq:
 172       forall sigma pi sigma' pi':env, i1 i1' i2:stmt.
 173         one_step sigma pi i1 sigma' pi' i1' ->
 174           one_step sigma pi (Sseq i1 i2) sigma' pi' (Sseq i1' i2)
 175
 176   | one_step_seq_skip:
 177       forall sigma pi:env, i:stmt.
 178         one_step sigma pi (Sseq Sskip i) sigma pi i
 179
 180   | one_step_if_true:
 181       forall sigma pi:env, e:term, i1 i2:stmt.
 182         eval_term sigma pi e = (Vbool True) ->
 183           one_step sigma pi (Sif e i1 i2) sigma pi i1
 184
 185   | one_step_if_false:
 186       forall sigma pi:env, e:term, i1 i2:stmt.
 187         eval_term sigma pi e = (Vbool False) ->
 188           one_step sigma pi (Sif e i1 i2) sigma pi i2
 189
 190   | one_step_assert:
 191       forall sigma pi:env, f:fmla.
 192         eval_fmla sigma pi f ->
 193           one_step sigma pi (Sassert f) sigma pi Sskip
 194
 195   | one_step_while_true:
 196       forall sigma pi:env, e:term, inv:fmla, i:stmt.
 197         eval_fmla sigma pi inv ->
 198         eval_term sigma pi e = (Vbool True) ->
 199           one_step sigma pi (Swhile e inv i) sigma pi (Sseq i (Swhile e inv i))
 200
 201   | one_step_while_false:
 202       forall sigma pi:env, e:term, inv:fmla, i:stmt.
 203         eval_fmla sigma pi inv ->
 204         eval_term sigma pi e = (Vbool False) ->
 205           one_step sigma pi (Swhile e inv i) sigma pi Sskip
 206
 207 (***
 208
 209   lemma progress:
 210     forall s:state, i:stmt.
 211       i <> Sskip ->
 212       exists s':state, i':stmt. one_step s i s' i'
 213
 214 *)
 215
 216  (** many steps of execution *)
 217
 218  inductive many_steps env env stmt env env stmt int =
 219    | many_steps_refl:
 220      forall sigma pi:env, i:stmt. many_steps sigma pi i sigma pi i 0
 221    | many_steps_trans:
 222      forall sigma1 pi1 sigma2 pi2 sigma3 pi3:env, i1 i2 i3:stmt, n:int.
 223        one_step sigma1 pi1 i1 sigma2 pi2 i2 ->
 224        many_steps sigma2 pi2 i2 sigma3 pi3 i3 n ->
 225        many_steps sigma1 pi1 i1 sigma3 pi3 i3 (n+1)
 226
 227 lemma steps_non_neg:
 228   forall sigma1 pi1 sigma2 pi2:env, i1 i2:stmt, n:int.
 229     many_steps sigma1 pi1 i1 sigma2 pi2 i2 n -> n >= 0
 230
 231 lemma many_steps_seq:
 232   forall sigma1 pi1 sigma3 pi3:env, i1 i2:stmt, n:int.
 233     many_steps sigma1 pi1 (Sseq i1 i2) sigma3 pi3 Sskip n ->
 234     exists sigma2 pi2:env, n1 n2:int.
 235       many_steps sigma1 pi1 i1 sigma2 pi2 Sskip n1 /\
 236       many_steps sigma2 pi2 i2 sigma3 pi3 Sskip n2 /\
 237       n = 1 + n1 + n2
 238
 239
 240
 241 predicate valid_fmla (p:fmla) = forall sigma pi:env. eval_fmla sigma pi p
 242
 243 (** {3 Hoare triples} *)
 244
 245 (** partial correctness *)
 246 predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
 247     forall sigma pi:env. eval_fmla sigma pi p ->
 248       forall sigma' pi':env, n:int. many_steps sigma pi i sigma' pi' Sskip n ->
 249         eval_fmla sigma' pi' q
 250
 251 (*** total correctness *)
 252 (***
 253 predicate total_valid_triple (p:fmla) (i:stmt) (q:fmla) =
 254     forall s:state. eval_fmla s p ->
 255       exists s':state, n:int. many_steps s i s' Sskip n /\
 256         eval_fmla s' q
 257 *)
 258
 259 end
 260
 261
 262 theory TestSemantics
 263
 264 use Imp
 265 use map.Const
 266
 267 function my_sigma : env = Const.const (Vint 0)
 268 function my_pi : env = Const.const (Vint 42)
 269
 270 goal Test13 :
 271   eval_term my_sigma my_pi (Tconst 13) = Vint 13
 272
 273 goal Test42 :
 274   eval_term my_sigma my_pi (Tvar 0) = Vint 42
 275
 276 goal Test0 :
 277   eval_term my_sigma my_pi (Tderef 0) = Vint 0
 278
 279 goal Test55 :
 280   eval_term my_sigma my_pi (Tbin (Tvar 0) Oplus (Tconst 13)) = Vint 55
 281
 282 goal Ass42 :
 283     let x = 0 in
 284     forall sigma' pi':env.
 285       one_step my_sigma my_pi (Sassign x (Tconst 42)) sigma' pi' Sskip ->
 286         IdMap.get sigma' x = Vint 42
 287
 288 goal If42 :
 289     let x = 0 in
 290     forall sigma1 pi1 sigma2 pi2:env, i:stmt.
 291       one_step my_sigma my_pi
 292         (Sif (Tbin (Tderef x) Ole (Tconst 10))
 293              (Sassign x (Tconst 13))
 294              (Sassign x (Tconst 42)))
 295         sigma1 pi1 i ->
 296       one_step sigma1 pi1 i sigma2 pi2 Sskip ->
 297         IdMap.get sigma2 x = Vint 13
 298
 299 end
 300
 301 (** {2 Hoare logic} *)
 302
 303 theory HoareLogic
 304
 305 use Imp
 306
 307
 308 (** Hoare logic rules (partial correctness) *)
 309
 310 lemma consequence_rule:
 311   forall p p' q q':fmla, i:stmt.
 312   valid_fmla (Fimplies p' p) ->
 313   valid_triple p i q ->
 314   valid_fmla (Fimplies q q') ->
 315   valid_triple p' i q'
 316
 317 lemma skip_rule:
 318   forall q:fmla. valid_triple q Sskip q
 319
 320 lemma assign_rule:
 321   forall q:fmla, x id:ident, e:term.
 322   fresh_in_fmla id q ->
 323   valid_triple (Flet id e (subst q x id)) (Sassign x e) q
 324
 325 lemma seq_rule:
 326   forall p q r:fmla, i1 i2:stmt.
 327   valid_triple p i1 r /\ valid_triple r i2 q ->
 328   valid_triple p (Sseq i1 i2) q
 329
 330 lemma if_rule:
 331   forall e:term, p q:fmla, i1 i2:stmt.
 332   valid_triple (Fand p (Fterm e)) i1 q /\
 333   valid_triple (Fand p (Fnot (Fterm e))) i2 q ->
 334   valid_triple p (Sif e i1 i2) q
 335
 336 lemma assert_rule:
 337   forall f p:fmla. valid_fmla (Fimplies p f) ->
 338   valid_triple p (Sassert f) p
 339
 340 lemma assert_rule_ext:
 341   forall f p:fmla.
 342   valid_triple (Fimplies f p) (Sassert f) p
 343
 344 lemma while_rule:
 345   forall e:term, inv:fmla, i:stmt.
 346   valid_triple (Fand (Fterm e) inv) i inv ->
 347   valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)
 348
 349 lemma while_rule_ext:
 350   forall e:term, inv inv':fmla, i:stmt.
 351   valid_fmla (Fimplies inv' inv) ->
 352   valid_triple (Fand (Fterm e) inv') i inv' ->
 353   valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e)) inv')
 354
 355 (*** frame rule ? *)
 356
 357 end
 358
 359 (** {2 WP calculus} *)
 360
 361 module WP
 362
 363 use Imp
 364
 365 use set.Fset as Set
 366 clone set.SetApp as S with type elt = ident, val eq = Int.(=)
 367
 368 predicate assigns (sigma:env) (a:Set.fset ident) (sigma':env) =
 369   forall i:ident. not (Set.mem i a) ->
 370     IdMap.get sigma i = IdMap.get sigma' i
 371
 372 lemma assigns_refl:
 373   forall sigma:env, a:Set.fset ident. assigns sigma a sigma
 374
 375 lemma assigns_trans:
 376   forall sigma1 sigma2 sigma3:env, a:Set.fset ident.
 377     assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
 378     assigns sigma1 a sigma3
 379
 380 lemma assigns_union_left:
 381   forall sigma sigma':env, s1 s2:Set.fset ident.
 382     assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'
 383
 384 lemma assigns_union_right:
 385   forall sigma sigma':env, s1 s2:Set.fset ident.
 386     assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
 387
 388
 389 predicate stmt_writes (i:stmt) (w:Set.fset ident) =
 390   match i with
 391   | Sskip | Sassert _ -> true
 392   | Sassign id _ -> Set.mem id w
 393   | Sseq s1 s2 | Sif _ s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
 394   | Swhile _ _ s -> stmt_writes s w
 395   end
 396
 397
 398   let rec compute_writes (s:stmt) : S.set
 399    ensures {
 400      forall sigma pi sigma' pi':env, n:int.
 401        many_steps sigma pi s sigma' pi' Sskip n ->
 402        assigns sigma result sigma' }
 403    variant { s }
 404   = match s with
 405     | Sskip -> S.empty ()
 406     | Sassign i _ -> S.singleton i
 407     | Sseq s1 s2 -> S.union (compute_writes s1) (compute_writes s2)
 408     | Sif _ s1 s2 -> S.union (compute_writes s1) (compute_writes s2)
 409     | Swhile _ _ s -> compute_writes s
 410     | Sassert _ -> S.empty ()
 411     end
 412
 413   val fresh_from_fmla (q:fmla) : ident
 414     ensures { fresh_in_fmla result q }
 415
 416   val abstract_effects (i:stmt) (f:fmla) : fmla
 417     ensures { forall sigma pi:env. eval_fmla sigma pi result ->
 418         eval_fmla sigma pi f /\
 419 (***
 420         forall sigma':env, w:Set.set ident.
 421         stmt_writes i w /\ assigns sigma w sigma' ->
 422         eval_fmla sigma' pi result
 423 *)
 424         forall sigma' pi':env, n:int.
 425            many_steps sigma pi i sigma' pi' Sskip n ->
 426            eval_fmla sigma' pi' result
 427      }
 428
 429   use HoareLogic
 430
 431   let rec wp (i:stmt) (q:fmla)
 432     ensures { valid_triple result i q }
 433     variant { i }
 434   = match i with
 435     | Sskip -> q
 436     | Sseq i1 i2 -> wp i1 (wp i2 q)
 437     | Sassign x e ->
 438         let id = fresh_from_fmla q in Flet id e (subst q x id)
 439     | Sif e i1 i2 ->
 440         Fand (Fimplies (Fterm e) (wp i1 q))
 441              (Fimplies (Fnot (Fterm e)) (wp i2 q))
 442     | Sassert f ->
 443        Fimplies f q (* liberal wp, no termination required *)
 444        (* Fand f q *) (* strict wp, termination required *)
 445     | Swhile e inv i ->
 446         Fand inv
 447           (abstract_effects i
 448             (Fand
 449                 (Fimplies (Fand (Fterm e) inv) (wp i inv))
 450                 (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
 451
 452     end
 453
 454
 455 end
 456
 457
 458
 459 (***
 460 Local Variables:
 461 compile-command: "why3ide wp2.mlw"
 462 End:
 463 *)