Commit 7c496b1b authored by MARCHE Claude's avatar MARCHE Claude

hoare logic: wp

parent 699d9f9d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="formula/why3session.xml">
name="hoare_logic/formula/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -61,7 +61,7 @@
expanded="true">
<goal
name="Test1"
sum="6bcc11f84daf50293f0fb99637a8f70a"
sum="ad0268b5331a68e8313850369f12a695"
proved="true"
expanded="true"
shape="Lamk_identc0LasetaconstaFalseV0aTrueainfix =aevalaForaFnotaFatomV0aFfalseV1aFalse">
......@@ -70,21 +70,21 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.24"/>
</proof>
</goal>
</theory>
......
theory Imp
(* terms and formulas *)
type operator = Oplus | Ominus | Omult
type term =
| Tconst int
| Tvar int (* de Bruijn index *)
| Tderef int (* de Bruijn index *)
| Tbin term operator term
type fmla =
| Fterm term
| Fand fmla fmla
| Fnot fmla
| Fimplies fmla fmla
| Flet term fmla
| Fforall fmla
(* program states: 2 stack env for refs and local vars *)
use import int.Int
use import bool.Bool
type value =
| Verror
| Vint int
| Vbool bool
use import list.List
type state = {| var_env : list value; ref_env: list 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)
end
| _,_ -> Verror
end
use import list.Nth
function get_env (i:int) (env:list value) : value =
match nth i env with
| None -> Verror
| Some v -> v
end
function eval_term (s:state) (t:term) : value =
match t with
| Tconst n -> Vint n
| Tvar i -> get_env i (var_env s)
| Tderef i -> get_env i (ref_env s)
| Tbin t1 op t2 ->
eval_bin (eval_term s t1) op (eval_term s t2)
end
function my_state :state =
{| var_env = Cons (Vint 42) Nil; ref_env = Nil |}
goal Test13 :
eval_term my_state (Tconst 13) = Vint 13
goal Test42 :
eval_term my_state (Tvar 0) = Vint 42
goal Test55 :
eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) = Vint 55
(* statements *)
type stmt =
| Sskip
| Sassign int term
| Sseq stmt stmt
| Sif term stmt stmt
| Swhile term stmt
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:
forall s:state, x:ident, e:expr.
one_step s (Sassign x e)
(IdMap.set s x (eval_expr s e)) Sskip
| 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:
forall s:state, e:expr, i1 i2:stmt.
eval_expr s e <> 0 ->
one_step s (Sif e i1 i2) s i1
| one_step_if_false:
forall s:state, e:expr, i1 i2:stmt.
eval_expr s e = 0 ->
one_step s (Sif e i1 i2) s i2
| one_step_while_true:
forall s:state, e:expr, i:stmt.
eval_expr s e <> 0 ->
one_step s (Swhile e i) s (Sseq i (Swhile e i))
| one_step_while_false:
forall s:state, e:expr, i:stmt.
eval_expr s e = 0 ->
one_step s (Swhile e i) s Sskip
goal Ass42 :
let x = mk_ident 0 in
let s = IdMap.const 0 in
forall s':state.
one_step s (Sassign x (Econst 42)) s' Sskip ->
IdMap.get s' x = 42
goal If42 :
let x = mk_ident 0 in
let s = IdMap.const 0 in
forall s1 s2:state, i:stmt.
one_step s
(Sif (Evar x)
(Sassign x (Econst 13))
(Sassign x (Econst 42)))
s1 i ->
one_step s1 i s2 Sskip ->
IdMap.get s2 x = 42
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 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
(* formulas *)
predicate eval_fmla (s:state) (f:fmla) =
match f with
| Fterm e -> eval_expr s e <> 0
| Fand f1 f2 -> eval_fmla s f1 /\ eval_fmla s f2
| Fnot f -> not (eval_fmla s f)
| Fimplies f1 f2 -> eval_fmla s f1 -> eval_fmla s f2
end
(* substitution *)
function subst_expr (e:expr) (x:ident) (t:expr) : expr =
match e with
| Econst _ -> e
| Evar y -> if x=y then t else e
| Ebin e1 op e2 -> Ebin (subst_expr e1 x t) op (subst_expr e2 x t)
end
lemma eval_subst_expr:
forall s:state, e:expr, x:ident, t:expr.
eval_expr s (subst_expr e x t) =
eval_expr (IdMap.set s x (eval_expr s t)) e
function subst (f:fmla) (x:ident) (t:expr) : fmla =
match f with
| Fterm e -> Fterm (subst_expr e x t)
| 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)
end
lemma eval_subst:
forall s:state, f:fmla, x:ident, t:expr.
eval_fmla s (subst f x t) <-> eval_fmla (IdMap.set s x (eval_expr s t)) f
predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p
(* Hoare triples *)
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
forall s:state. eval_fmla s p ->
forall s':state, n:int. many_steps s i s' Sskip n ->
eval_fmla s' q
(* Hoare logic rules *)
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule:
forall q:fmla, x:ident, e:expr.
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:
forall e:expr, 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 while_rule:
forall e:expr, inv:fmla, i:stmt.
valid_triple (Fand (Fterm e) inv) i inv ->
valid_triple inv (Swhile e 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'
*)
end
(*
module WP
use import imp_n.Imp
use import Imp
let rec wp (i:stmt) (q:fmla) =
{ true }
......@@ -18,6 +283,7 @@ module WP
end
*)
(*
......
......@@ -51,159 +51,64 @@
verified="true"
expanded="true">
<theory
name="WP WP"
name="Imp"
verified="true"
expanded="true">
<goal
name="WP_parameter wp"
expl="parameter wp"
sum="5bd057f848f72a63b4c3917e9392e870"
name="Test13"
sum="10a7fb7a54721cc5d2e8fe0ccc0a06dd"
proved="true"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSwhilewwavalid_tripleaFtermaEconstc0V0V1FF">
shape="ainfix =aeval_termamy_stateaTconstc13aVintc13">
<proof
prover="z3"
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="Test42"
sum="8062e7b817a81543a8e958c35e86e92f"
proved="true"
expanded="true"
shape="ainfix =aeval_termamy_stateaTvarc0aVintc42">
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="Test55"
sum="2890146a1089020f995c0962244237b7"
proved="true"
expanded="true"
shape="ainfix =aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55">
<proof
prover="coq"
timelimit="3"
edited="wp_Imp_Test55_1.v"
obsolete="false">
<result status="valid" time="0.47"/>
</proof>
</goal>
<goal
name="check_skip"
sum="7df7f8c1ae36c58d46923adb24d820f3"
proved="true"
expanded="true"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter wp.1"
expl="parameter wp"
sum="bb82b4da28a75725ff508bb872eb9300"
proved="true"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSwhilewwtFF">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter wp.2"
expl="parameter wp"
sum="9617ec74c86f83cccb6ec913990f6686"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSwhilewwtFF">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter wp.3"
expl="parameter wp"
sum="f8a917b7a30a9efc9190b33726d130f7"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSwhilewwtFF">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter wp.4"
expl="parameter wp"
sum="fb617d6a26606c752274200a34871307"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V9aFimpliesaFnotaFtermV6V10V0V1Iavalid_tripleV10V8V1FIavalid_tripleV9V7V1FaSwhilewwtFF">
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.17"/>
</proof>
</goal>
<goal
name="WP_parameter wp.5"
expl="parameter wp"
sum="47f03e3a1f44c5b72c589d56d1baa1b2"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSwhilewwavalid_tripleaFtermaEconstc0V0V1FF">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.18"/>
</proof>
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive term :=
| Tconst : Z -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tbin : term -> operator -> term -> term .
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : term -> fmla -> fmla
| Fforall : fmla -> fmla .
Inductive value :=
| Verror : value
| Vint : Z -> value
| Vbool : bool -> value .
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Inductive state :=
| mk_state : (list value) -> (list value) -> state .
Definition ref_env(u:state): (list value) :=
match u with
| (mk_state _ ref_env1) => ref_env1
end.
Definition var_env(u:state): (list value) :=
match u with
| (mk_state var_env1 _) => var_env1
end.
Definition eval_bin(x:value) (op:operator) (y:value): value := match (x,
y) with
| ((Vint x1), (Vint y1)) =>
match op with
| Oplus => (Vint (x1 + y1)%Z)
| Ominus => (Vint (x1 - y1)%Z)
| Omult => (Vint (x1 * y1)%Z)
end
| (_, _) => Verror
end.
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Set Contextual Implicit.
Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
Implicit Arguments nth.
Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None:(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
Definition get_env(i:Z) (env:(list value)): value := match (nth i
env) with
| None => Verror
| (Some v) => v
end.
Set Implicit Arguments.
Fixpoint eval_term(s:state) (t:term) {struct t}: value :=
match t with
| (Tconst n) => (Vint n)
| (Tvar i) => (get_env i (var_env s))
| (Tderef i) => (get_env i (ref_env s))
| (Tbin t1 op t2) => (eval_bin (eval_term s t1) op (eval_term s t2))
end.
Unset Implicit Arguments.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Test55 : ((eval_term (mk_state (Cons (Vint 42%Z) (Nil:(list value)))
(Nil:(list value))) (Tbin (Tvar 0%Z) Oplus (Tconst 13%Z))) = (Vint 55%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
simpl.
unfold eval_bin; simpl.
unfold get_env; simpl.
generalize (nth_def _ 0 (Cons (Vint 42) Nil)).
intros (H,_).
rewrite H; auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -62,6 +62,7 @@ echo ""
echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
run_dir hoare_logic "-I hoare_logic"
echo ""
echo "=== Check Builtin translation ==="
......
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