Commit 7497d447 authored by Andrei Paskevich's avatar Andrei Paskevich

update examples/hoare_logic/

blocking_semantics3.mlw
blocking_semantics4.mlw
wp2.mlw
wp_total.mlw
parent 03d1c7b2
...@@ -28,7 +28,7 @@ lemma mident_decide : ...@@ -28,7 +28,7 @@ lemma mident_decide :
forall m1 m2: mident. m1 = m2 \/ m1 <> m2 forall m1 m2: mident. m1 = m2 \/ m1 <> m2
(** ident for immutable variables *) (** ident for immutable variables *)
type ident = {| ident_index : int |} type ident = { ident_index : int }
lemma ident_decide : lemma ident_decide :
forall m1 m2: ident. m1 = m2 \/ m1 <> m2 forall m1 m2: ident. m1 = m2 \/ m1 <> m2
......
...@@ -29,7 +29,7 @@ axiom mident_decide : ...@@ -29,7 +29,7 @@ axiom mident_decide :
forall m1 m2: mident. m1 = m2 \/ m1 <> m2 forall m1 m2: mident. m1 = m2 \/ m1 <> m2
(** ident for immutable variables *) (** ident for immutable variables *)
type ident = {| ident_index : int |} type ident = { ident_index : int }
constant result : ident constant result : ident
......
...@@ -393,9 +393,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) = ...@@ -393,9 +393,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
end end
let rec compute_writes (s:stmt) : Set.set ident = let rec compute_writes (s:stmt) : Set.set ident
{ } ensures {
match s with forall sigma pi sigma' pi':env, n:int.
many_steps sigma pi s sigma' pi' Sskip n ->
assigns sigma result sigma' }
= match s with
| Sskip -> Set.empty | Sskip -> Set.empty
| Sassign i _ -> Set.singleton i | Sassign i _ -> Set.singleton i
| Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2) | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
...@@ -403,19 +406,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) = ...@@ -403,19 +406,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
| Swhile _ _ s -> compute_writes s | Swhile _ _ s -> compute_writes s
| Sassert _ -> Set.empty | Sassert _ -> Set.empty
end 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) : val fresh_from_fmla (q:fmla) : ident
{ } ensures { fresh_in_fmla result q }
ident
{ fresh_in_fmla result q }
val abstract_effects (i:stmt) (f:fmla) : val abstract_effects (i:stmt) (f:fmla) : fmla
{ } ensures { forall sigma pi:env. eval_fmla sigma pi result ->
fmla
{ forall sigma pi:env. eval_fmla sigma pi result ->
eval_fmla sigma pi f /\ eval_fmla sigma pi f /\
(*** (***
forall sigma':env, w:Set.set ident. forall sigma':env, w:Set.set ident.
...@@ -429,9 +425,9 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) = ...@@ -429,9 +425,9 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
use HoareLogic use HoareLogic
let rec wp (i:stmt) (q:fmla) = let rec wp (i:stmt) (q:fmla)
{ true } ensures { valid_triple result i q }
match i with = match i with
| Sskip -> q | Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q) | Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e -> | Sassign x e ->
...@@ -450,7 +446,6 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) = ...@@ -450,7 +446,6 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
(Fimplies (Fand (Fnot (Fterm e)) inv) q))) (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end end
{ valid_triple result i q }
end end
......
...@@ -38,7 +38,7 @@ type env = IdMap.map ident value ...@@ -38,7 +38,7 @@ type env = IdMap.map ident value
type var_env = env type var_env = env
type ref_env = env type ref_env = env
type state = {| var_env : var_env; ref_env: ref_env |} type state = { var_env : var_env; ref_env: ref_env }
(* semantics of formulas *) (* semantics of formulas *)
...@@ -66,8 +66,8 @@ function eval_term (s:state) (t:term) : value = ...@@ -66,8 +66,8 @@ function eval_term (s:state) (t:term) : value =
end end
function my_state :state = function my_state :state =
{| var_env = IdMap.const (Vint 42); { var_env = IdMap.const (Vint 42);
ref_env = IdMap.const (Vint 0) |} ref_env = IdMap.const (Vint 0) }
goal Test13 : goal Test13 :
eval_term my_state (Tconst 13) = Vint 13 eval_term my_state (Tconst 13) = Vint 13
...@@ -89,20 +89,20 @@ predicate eval_fmla (s:state) (f:fmla) = ...@@ -89,20 +89,20 @@ predicate eval_fmla (s:state) (f:fmla) =
| Fimplies f1 f2 -> eval_fmla s f1 -> eval_fmla s f2 | Fimplies f1 f2 -> eval_fmla s f1 -> eval_fmla s f2
| Flet x t f -> | Flet x t f ->
eval_fmla eval_fmla
{| var_env = IdMap.set s.var_env x (eval_term s t) ; { var_env = IdMap.set s.var_env x (eval_term s t) ;
ref_env = s.ref_env |} ref_env = s.ref_env }
f f
| Fforall x Tint f -> | Fforall x Tint f ->
forall n:int. forall n:int.
eval_fmla eval_fmla
{| var_env = IdMap.set s.var_env x (Vint n); { var_env = IdMap.set s.var_env x (Vint n);
ref_env = s.ref_env |} ref_env = s.ref_env }
f f
| Fforall x Tbool f -> | Fforall x Tbool f ->
forall b:bool. forall b:bool.
eval_fmla eval_fmla
{| var_env = IdMap.set s.var_env x (Vbool b); { var_env = IdMap.set s.var_env x (Vbool b);
ref_env = s.ref_env |} ref_env = s.ref_env }
f f
end end
...@@ -119,8 +119,8 @@ function subst_term (e:term) (x:ident) (t:term) : term = ...@@ -119,8 +119,8 @@ function subst_term (e:term) (x:ident) (t:term) : term =
lemma eval_subst_term: lemma eval_subst_term:
forall s:state, e:term, x:ident, t:term. forall s:state, e:term, x:ident, t:term.
eval_term s (subst_term e x t) = eval_term s (subst_term e x t) =
eval_term {| var_env = s.var_env; eval_term { var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x (eval_term s t)) |} ref_env = (IdMap.set s.ref_env x (eval_term s t)) }
e e
function subst (f:fmla) (x:ident) (t:term) : fmla = function subst (f:fmla) (x:ident) (t:term) : fmla =
...@@ -137,8 +137,8 @@ function subst (f:fmla) (x:ident) (t:term) : fmla = ...@@ -137,8 +137,8 @@ function subst (f:fmla) (x:ident) (t:term) : fmla =
lemma eval_subst: lemma eval_subst:
forall f:fmla, s:state, x:ident, t:term. forall f:fmla, s:state, x:ident, t:term.
eval_fmla s (subst f x t) <-> eval_fmla s (subst f x t) <->
eval_fmla {| var_env = s.var_env; eval_fmla { var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x (eval_term s t)) |} ref_env = (IdMap.set s.ref_env x (eval_term s t)) }
f f
(* statements *) (* statements *)
...@@ -161,8 +161,8 @@ inductive one_step state stmt state stmt = ...@@ -161,8 +161,8 @@ inductive one_step state stmt state stmt =
| one_step_assign: | one_step_assign:
forall s:state, x:ident, e:term. forall s:state, x:ident, e:term.
one_step s (Sassign x e) one_step s (Sassign x e)
{| var_env = s.var_env; { var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x (eval_term s e)) |} ref_env = (IdMap.set s.ref_env x (eval_term s e)) }
Sskip Sskip
| one_step_seq: | one_step_seq:
...@@ -340,9 +340,9 @@ module WP ...@@ -340,9 +340,9 @@ module WP
use import Imp use import Imp
let rec wp (i:stmt) (q:fmla) = let rec wp (i:stmt) (q:fmla)
{ true } ensures { valid_triple result i q }
match i with = match i with
| Sskip -> q | Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q) | Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e -> | Sassign x e ->
...@@ -363,7 +363,6 @@ module WP ...@@ -363,7 +363,6 @@ module WP
(Fimplies (Fand (Fnot (Fterm e)) inv) q))) (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end end
{ valid_triple result i q }
end end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment