Commit 32393783 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

WP with bound variables

parent 2362bfcd
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/hoare_logic/imp_n/why3session.xml">
name="imp_n/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -28,13 +28,13 @@
expanded="true">
<theory
name="Imp"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
<goal
name="ident_eq_dec"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="8" loccnumb="6" loccnume="18"
sum="ca7c4648761db026ea93d61666f0b79a"
proved="true"
......@@ -50,7 +50,7 @@
</goal>
<goal
name="check_skip"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="32" loccnumb="6" loccnume="16"
sum="a28ed21b2b531fe3e8a3933e02f27497"
proved="true"
......@@ -61,12 +61,12 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test13"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="59" loccnumb="7" loccnume="13"
sum="89034cff3a243960c6fe7b2b2a91966f"
proved="true"
......@@ -82,7 +82,7 @@
</goal>
<goal
name="Test42"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="63" loccnumb="7" loccnume="13"
sum="991bca434c242bd0fc4fcae7860bb583"
proved="true"
......@@ -98,7 +98,7 @@
</goal>
<goal
name="Test55"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="68" loccnumb="7" loccnume="13"
sum="13ad67fe0a83a4e1ece624124c864703"
proved="true"
......@@ -114,7 +114,7 @@
</goal>
<goal
name="Ass42"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="112" loccnumb="7" loccnume="12"
sum="2eae993f753f8826c606f370e5382862"
proved="true"
......@@ -130,7 +130,7 @@
</goal>
<goal
name="If42"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="119" loccnumb="7" loccnume="11"
sum="12b5437a3440e505c69b24e6e91a75b8"
proved="true"
......@@ -141,12 +141,12 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
<result status="valid" time="0.36"/>
</proof>
</goal>
<goal
name="progress"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="131" loccnumb="8" loccnume="16"
sum="1de081684224e7f85881292371e2b0b0"
proved="true"
......@@ -158,12 +158,12 @@
edited="imp_n_Imp_progress_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
name="steps_non_neg"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="148" loccnumb="6" loccnume="19"
sum="9afb86d9042cfb6d235dbe573c99c7af"
proved="true"
......@@ -175,12 +175,12 @@
edited="imp_n_Imp_steps_non_neg_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.49"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
name="many_steps_seq"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="152" loccnumb="6" loccnume="20"
sum="63f9f761456c06e15c3369514675fb0d"
proved="true"
......@@ -192,12 +192,12 @@
edited="imp_n_Imp_many_steps_seq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
<goal
name="eval_subst_expr"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="186" loccnumb="6" loccnume="21"
sum="e63480504ff35c49144c886bd8a62737"
proved="true"
......@@ -209,12 +209,12 @@
edited="imp_n_Imp_eval_subst_expr_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.52"/>
<result status="valid" time="0.54"/>
</proof>
</goal>
<goal
name="eval_subst"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="199" loccnumb="6" loccnume="16"
sum="86264772f72216dbeb4b098411b567fc"
proved="true"
......@@ -226,12 +226,12 @@
edited="imp_n_Imp_eval_subst_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.54"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal
name="skip_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="214" loccnumb="6" loccnume="15"
sum="2ad581756a248899fb392c2d4997c804"
proved="true"
......@@ -242,12 +242,12 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="assign_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="217" loccnumb="6" loccnume="17"
sum="40e9ed93ad1f5b1a561275cf534b59fd"
proved="true"
......@@ -259,12 +259,12 @@
edited="imp_n_Imp_assign_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="seq_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="221" loccnumb="6" loccnume="14"
sum="523e5a3dbd386e78faa32a502c820e04"
proved="true"
......@@ -276,12 +276,12 @@
edited="imp_n_Imp_seq_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="if_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="226" loccnumb="6" loccnume="13"
sum="7328cf68bc5a595e5c87d83b2d1a723e"
proved="true"
......@@ -293,12 +293,12 @@
edited="imp_n_Imp_if_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="while_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="232" loccnumb="6" loccnume="16"
sum="c297af00727ea643f60ade404427e376"
proved="true"
......@@ -310,12 +310,12 @@
edited="imp_n_Imp_while_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.64"/>
</proof>
</goal>
<goal
name="consequence_rule"
locfile="examples/hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="237" loccnumb="6" loccnume="22"
sum="d312e9ab3334578a19d6c531bed904c6"
proved="true"
......@@ -333,7 +333,7 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.27"/>
<result status="valid" time="0.28"/>
</proof>
</goal>
</theory>
......
theory Imp
(* terms and formulas *)
type datatype = Tint | Tbool
type operator = Oplus | Ominus | Omult | Ole
type ident = int
type term =
| Tconst int
| 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 import int.Int
use import bool.Bool
type value =
| Vint int
| Vbool bool
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
| Tconst n -> Vint n
| 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
function my_sigma : env = IdMap.const (Vint 42)
function my_pi : env = IdMap.const (Vint 0)
goal Test13 :
eval_term my_sigma my_pi (Tconst 13) = Vint 13
goal Test42 :
eval_term my_sigma my_pi (Tvar 0) = Vint 42
goal Test0 :
eval_term my_sigma my_pi (Tderef 0) = Vint 0
goal Test55 :
eval_term my_sigma my_pi (Tbin (Tvar 0) Oplus (Tconst 13)) = Vint 55
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 Tint f ->
forall n:int. eval_fmla sigma (IdMap.set pi x (Vint n)) f
| Fforall x Tbool f ->
forall b:bool.
eval_fmla sigma (IdMap.set pi x (Vbool b)) 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
| Tconst _ -> e
| 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
| Tconst _ -> 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 t (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)
(* statements *)
type stmt =
| Sskip
| Sassign ident term
| Sseq stmt stmt
| Sif term stmt stmt
| Sassert fmla
| Swhile term fmla stmt
lemma check_skip:
forall s:stmt. s=Sskip \/s<>Sskip
(* small-steps semantics for statements *)
inductive one_step env env stmt env env stmt =
| one_step_assign:
forall sigma pi:env, x:ident, e:term.
one_step sigma pi (Sassign x e)
(IdMap.set sigma x (eval_term sigma pi e)) pi
Sskip
| one_step_seq:
forall sigma pi sigma' pi':env, i1 i1' i2:stmt.
one_step sigma pi i1 sigma' pi' i1' ->
one_step sigma pi (Sseq i1 i2) sigma' pi' (Sseq i1' i2)
| one_step_seq_skip:
forall sigma pi:env, i:stmt.
one_step sigma pi (Sseq Sskip i) sigma pi i
| one_step_if_true:
forall sigma pi:env, e:term, i1 i2:stmt.
eval_term sigma pi e = (Vbool True) ->
one_step sigma pi (Sif e i1 i2) sigma pi i1
| one_step_if_false:
forall sigma pi:env, e:term, i1 i2:stmt.
eval_term sigma pi e = (Vbool False) ->
one_step sigma pi (Sif e i1 i2) sigma pi i2
| one_step_assert:
forall sigma pi:env, f:fmla.
eval_fmla sigma pi f ->
one_step sigma pi (Sassert f) sigma pi Sskip
| one_step_while_true:
forall sigma pi:env, e:term, inv:fmla, i:stmt.
eval_fmla sigma pi inv ->
eval_term sigma pi e = (Vbool True) ->
one_step sigma pi (Swhile e inv i) sigma pi (Sseq i (Swhile e inv i))
| one_step_while_false:
forall sigma pi:env, e:term, inv:fmla, i:stmt.
eval_fmla sigma pi inv ->
eval_term sigma pi e = (Vbool False) ->
one_step sigma pi (Swhile e inv i) sigma pi Sskip
goal Ass42 :
let x = 0 in
forall sigma' pi':env.
one_step my_sigma my_pi (Sassign x (Tconst 42)) sigma' pi' Sskip ->
IdMap.get sigma' x = Vint 42
goal If42 :
let x = 0 in
forall sigma1 pi1 sigma2 pi2:env, i:stmt.
one_step my_sigma my_pi
(Sif (Tbin (Tderef x) Ole (Tconst 10))
(Sassign x (Tconst 13))
(Sassign x (Tconst 42)))
sigma1 pi1 i ->
one_step sigma1 pi1 i sigma2 pi2 Sskip ->
IdMap.get sigma2 x = Vint 13
(*
lemma progress:
forall s:state, i:stmt.
i <> Sskip ->
exists s':state, i':stmt. one_step s i s' i'
*)
(* many steps of execution *)
inductive many_steps env env stmt env env stmt int =
| many_steps_refl:
forall sigma pi:env, i:stmt. many_steps sigma pi i sigma pi i 0
| many_steps_trans:
forall sigma1 pi1 sigma2 pi2 sigma3 pi3:env, i1 i2 i3:stmt, 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:stmt, n:int.
many_steps sigma1 pi1 i1 sigma2 pi2 i2 n -> n >= 0
lemma many_steps_seq:
forall sigma1 pi1 sigma3 pi3:env, i1 i2:stmt, n:int.
many_steps sigma1 pi1 (Sseq i1 i2) sigma3 pi3 Sskip n ->
exists sigma2 pi2:env, n1 n2:int.
many_steps sigma1 pi1 i1 sigma2 pi2 Sskip n1 /\
many_steps sigma2 pi2 i2 sigma3 pi3 Sskip n2 /\
n = 1 + n1 + n2
predicate valid_fmla (p:fmla) = forall sigma pi:env. eval_fmla sigma pi p
(*** Hoare triples ***)
(* partial correctness *)
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
forall sigma pi:env. eval_fmla sigma pi p ->
forall sigma' pi':env, n:int. many_steps sigma pi i sigma' pi' Sskip n ->
eval_fmla sigma' pi' q
(* total correctness *)
(*
predicate total_valid_triple (p:fmla) (i:stmt) (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
*)
(* Hoare logic rules (partial correctness) *)
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule:
forall q:fmla, x id:ident, e:term.
fresh_in_fmla id q ->
valid_triple (Flet id e (subst q x id)) (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:
forall e:term, p q:fmla, i1 i2:stmt.
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 assert_rule:
forall f p:fmla. valid_fmla (Fimplies p f) ->
valid_triple p (Sassert f) p
lemma assert_rule_ext:
forall f p:fmla.
valid_triple (Fimplies f p) (Sassert f) p
lemma while_rule:
forall e:term, inv:fmla, i:stmt.
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:stmt.
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')
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'
(* frame rule *)
use set.Set
predicate assigns (sigma pi:env) (a:Set.set ident) (sigma' pi':env) =
forall i:ident. not (Set.mem i a) ->
eval_term sigma pi (Tderef i) = eval_term sigma' pi' (Tderef i)
function stmt_writes (s:stmt) : Set.set ident =
match s with
| Sskip -> Set.empty
| Sassign i _ -> Set.singleton i
| Sseq s1 s2 -> Set.union (stmt_writes s1) (stmt_writes s2)
| Sif _ s1 s2 -> Set.union (stmt_writes s1) (stmt_writes s2)
| Swhile _ _ s -> stmt_writes s
| Sassert _ -> Set.empty
end
end
module WP
use import Imp
val fresh_from_fmla (q:fmla) :
{ }
ident
{ fresh_in_fmla result q }
let rec wp (i:stmt) (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
((*Fforall*) (Fand
(Fimplies (Fand (Fterm e) inv) (wp i inv))
(Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end
{ valid_triple result i q }
end
(*
Local Variables:
compile-command: "why3ide -I . wp2.mlw"
End:
*)