diff --git a/examples/hoare_logic/blocking_semantics3.mlw b/examples/hoare_logic/blocking_semantics3.mlw
index 74e464349abbb45fd8ccd26bcc1da6a768517381..2941fd43488e56a76011ae342f7beb2ee995aedb 100644
--- a/examples/hoare_logic/blocking_semantics3.mlw
+++ b/examples/hoare_logic/blocking_semantics3.mlw
@@ -28,7 +28,7 @@ lemma mident_decide :
forall m1 m2: mident. m1 = m2 \/ m1 <> m2
(** ident for immutable variables *)
-type ident = {| ident_index : int |}
+type ident = { ident_index : int }
lemma ident_decide :
forall m1 m2: ident. m1 = m2 \/ m1 <> m2
diff --git a/examples/hoare_logic/blocking_semantics4.mlw b/examples/hoare_logic/blocking_semantics4.mlw
index 84b280204f4d56b468f09fd9b644c724e9ec9a64..26922c7b403a63664e0133bf5070b1afb3935ad7 100644
--- a/examples/hoare_logic/blocking_semantics4.mlw
+++ b/examples/hoare_logic/blocking_semantics4.mlw
@@ -29,7 +29,7 @@ axiom mident_decide :
forall m1 m2: mident. m1 = m2 \/ m1 <> m2
(** ident for immutable variables *)
-type ident = {| ident_index : int |}
+type ident = { ident_index : int }
constant result : ident
diff --git a/examples/hoare_logic/wp2.mlw b/examples/hoare_logic/wp2.mlw
index ea4fddfd9457e67b7e50fb793d48a816d924f0db..597dde9d682c2c9cc798209fea35ac7313fa97a9 100644
--- a/examples/hoare_logic/wp2.mlw
+++ b/examples/hoare_logic/wp2.mlw
@@ -393,9 +393,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
end
- let rec compute_writes (s:stmt) : Set.set ident =
- { }
- match s with
+ let rec compute_writes (s:stmt) : Set.set ident
+ ensures {
+ 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
| Sassign i _ -> Set.singleton i
| Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
@@ -403,19 +406,12 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
| 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 fresh_from_fmla (q:fmla) : ident
+ ensures { fresh_in_fmla result q }
- val abstract_effects (i:stmt) (f:fmla) :
- { }
- fmla
- { forall sigma pi:env. eval_fmla sigma pi result ->
+ val abstract_effects (i:stmt) (f:fmla) : fmla
+ ensures { forall sigma pi:env. eval_fmla sigma pi result ->
eval_fmla sigma pi f /\
(***
forall sigma':env, w:Set.set ident.
@@ -429,9 +425,9 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
use HoareLogic
- let rec wp (i:stmt) (q:fmla) =
- { true }
- match i with
+ let rec wp (i:stmt) (q:fmla)
+ ensures { valid_triple result i q }
+ = match i with
| Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e ->
@@ -450,7 +446,6 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
(Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end
- { valid_triple result i q }
end
diff --git a/examples/hoare_logic/wp_total.mlw b/examples/hoare_logic/wp_total.mlw
index 33214d4d5e165488cec00d14328d24cf1474ccbd..6e27a435554c9c6b4d8cff5a2c4380eb2025d8d6 100644
--- a/examples/hoare_logic/wp_total.mlw
+++ b/examples/hoare_logic/wp_total.mlw
@@ -38,7 +38,7 @@ type env = IdMap.map ident value
type var_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 *)
@@ -66,8 +66,8 @@ function eval_term (s:state) (t:term) : value =
end
function my_state :state =
- {| var_env = IdMap.const (Vint 42);
- ref_env = IdMap.const (Vint 0) |}
+ { var_env = IdMap.const (Vint 42);
+ ref_env = IdMap.const (Vint 0) }
goal Test13 :
eval_term my_state (Tconst 13) = Vint 13
@@ -89,20 +89,20 @@ predicate eval_fmla (s:state) (f:fmla) =
| Fimplies f1 f2 -> eval_fmla s f1 -> eval_fmla s f2
| Flet x t f ->
eval_fmla
- {| var_env = IdMap.set s.var_env x (eval_term s t) ;
- ref_env = s.ref_env |}
+ { var_env = IdMap.set s.var_env x (eval_term s t) ;
+ ref_env = s.ref_env }
f
| Fforall x Tint f ->
forall n:int.
eval_fmla
- {| var_env = IdMap.set s.var_env x (Vint n);
- ref_env = s.ref_env |}
+ { var_env = IdMap.set s.var_env x (Vint n);
+ ref_env = s.ref_env }
f
| Fforall x Tbool f ->
forall b:bool.
eval_fmla
- {| var_env = IdMap.set s.var_env x (Vbool b);
- ref_env = s.ref_env |}
+ { var_env = IdMap.set s.var_env x (Vbool b);
+ ref_env = s.ref_env }
f
end
@@ -119,8 +119,8 @@ function subst_term (e:term) (x:ident) (t:term) : term =
lemma eval_subst_term:
forall s:state, e:term, x:ident, t:term.
eval_term s (subst_term e x t) =
- eval_term {| var_env = s.var_env;
- ref_env = (IdMap.set s.ref_env x (eval_term s t)) |}
+ eval_term { var_env = s.var_env;
+ ref_env = (IdMap.set s.ref_env x (eval_term s t)) }
e
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:
forall f:fmla, s:state, x:ident, t:term.
eval_fmla s (subst f x t) <->
- eval_fmla {| var_env = s.var_env;
- ref_env = (IdMap.set s.ref_env x (eval_term s t)) |}
+ eval_fmla { var_env = s.var_env;
+ ref_env = (IdMap.set s.ref_env x (eval_term s t)) }
f
(* statements *)
@@ -161,8 +161,8 @@ inductive one_step state stmt state stmt =
| one_step_assign:
forall s:state, x:ident, e:term.
one_step s (Sassign x e)
- {| var_env = s.var_env;
- ref_env = (IdMap.set s.ref_env x (eval_term s e)) |}
+ { var_env = s.var_env;
+ ref_env = (IdMap.set s.ref_env x (eval_term s e)) }
Sskip
| one_step_seq:
@@ -340,9 +340,9 @@ module WP
use import Imp
- let rec wp (i:stmt) (q:fmla) =
- { true }
- match i with
+ let rec wp (i:stmt) (q:fmla)
+ ensures { valid_triple result i q }
+ = match i with
| Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e ->
@@ -363,7 +363,6 @@ module WP
(Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end
- { valid_triple result i q }
end