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

wp with total eval of term

parent 5f6dc23b
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z) -> stmt
-> Z -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i
0%Z)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt) (n:Z), (one_step s1 i1 s2
i2) -> ((many_steps s2 i2 s3 i3 n) -> (many_steps s1 i1 s3 i3
(n + 1%Z)%Z)).
Axiom steps_non_neg : forall (s1:(map ident Z)) (s2:(map ident Z)) (i1:stmt)
(i2:stmt) (n:Z), (many_steps s1 i1 s2 i2 n) -> (0%Z <= n)%Z.
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt) (n:Z), (many_steps s1 (Sseq i1 i2) s3 Sskip n) -> exists s2:(map
ident Z), exists n1:Z, exists n2:Z, (many_steps s1 i1 s2 Sskip n1) /\
((many_steps s2 i2 s3 Sskip n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).
Inductive fmla :=
| Fterm : expr -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla .
Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
| (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
| (Fnot f1) => ~ (eval_fmla s f1)
| (Fimplies f1 f2) => (eval_fmla s f1) -> (eval_fmla s f2)
end.
Unset Implicit Arguments.
Parameter subst_expr: expr -> ident -> expr -> expr.
Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
match e with
| (Econst _) => ((subst_expr e x t) = e)
| (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
((subst_expr e x t) = e))
| (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
(subst_expr e2 x t)))
end.
Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)).
Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: 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 f1) => (Fnot (subst f1 x t))
| (Fimplies f1 f2) => (Fimplies (subst f1 x t) (subst f2 x t))
end.
Unset Implicit Arguments.
Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) <-> (eval_fmla (set s x (eval_expr s t)) f).
Definition valid_fmla(p:fmla): Prop := forall (s:(map ident Z)), (eval_fmla s
p).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)) (n:Z),
(many_steps s i sqt Sskip n) -> (eval_fmla sqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:ident) (e:expr),
(valid_triple (subst q x e) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:expr) (p:fmla) (q:fmla) (i1:stmt) (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).
Axiom 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)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_triple p i q) -> (valid_triple pqt i qqt).
(* YOU MAY EDIT THE PROOF BELOW *)
intros p p' q q' i H.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -4,13 +4,15 @@ theory Imp
(* terms and formulas *)
type datatype = Tint | Tbool
type operator = Oplus | Ominus | Omult | Ole
type ident = int
type term =
| Tconst int
| Tvar int (* de Bruijn index ? *)
| Tvar ident
| Tderef ident
| Tbin term operator term
......@@ -19,27 +21,22 @@ type fmla =
| Fand fmla fmla
| Fnot fmla
| Fimplies fmla fmla
| Flet term fmla
| Fforall fmla
| Flet ident term fmla
| Fforall ident datatype fmla
(* program states: 2 stack env for refs and local vars *)
use import int.Int
use import bool.Bool
type datatype =
| Tint | Tbool
type value =
| Vint int
| Vbool bool
use import list.List
use map.Map as IdMap
type var_env = list value
use map.Map as IdMap
type var_env = IdMap.map ident value
type ref_env = IdMap.map ident value
type state = {| var_env : var_env; ref_env: ref_env |}
(* semantics of formulas *)
......@@ -56,12 +53,14 @@ predicate eval_bin (x:value) (op:operator) (y:value) (res:value) =
| _,_ -> false
end
(*
inductive get_env (i:int) (env:list value) (res:value) =
| Get_first:
| Get_first:
forall x:value, l:list value. get_env 0 (Cons x l) x
| Get_next:
forall i:int, x r:value, l:list value. i > 0 ->
get_env (i-1) l r -> get_env i (Cons x l) x
*)
predicate get_refenv (i:ident) (e:ref_env) (r:value) =
IdMap.get e i = r
......@@ -71,7 +70,7 @@ inductive eval_term state term value =
forall s:state, n:int. eval_term s (Tconst n) (Vint n)
| eval_var :
forall s:state, i:int, res:value.
get_env i (var_env s) res -> eval_term s (Tvar i) res
get_refenv i (var_env s) res -> eval_term s (Tvar i) res
| eval_deref :
forall s:state, i:ident, res:value.
get_refenv i (ref_env s) res -> eval_term s (Tderef i) res
......@@ -81,7 +80,8 @@ inductive eval_term state term value =
eval_bin r1 op r2 r -> eval_term s (Tbin t1 op t2) r
function my_state :state =
{| var_env = Cons (Vint 42) Nil; 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)
......@@ -108,43 +108,50 @@ inductive eval_fmla state fmla bool =
eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
eval_fmla s (Fimplies f1 f2) (implb b1 b2)
| eval_forall_int_true:
forall s:state, f:fmla.
forall s:state, x:ident, f:fmla.
(* problem: qu'est-ce qui garanti que s.var_env a exactement
autant de debruijn que f ? *)
(forall n:int. eval_fmla
{| var_env = Cons (Vint n) s.var_env ; ref_env = s.ref_env |}
{| var_env = IdMap.set s.var_env x (Vint n);
ref_env = s.ref_env |}
f True) ->
eval_fmla s (Fforall f) True
eval_fmla s (Fforall x Tint f) True
(* substitution *)
(*
function subst_expr (e:expr) (x:ident) (t:expr) : expr =
function subst_term (e:term) (x:ident) (t:term) : term =
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)
| Tconst _ -> e
| Tvar _ -> e
| Tderef y -> if x=y then t else e
| Tbin e1 op e2 -> Tbin (subst_term e1 x t) op (subst_term 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
lemma eval_subst_term:
forall s:state, e:term, x:ident, t:term, r v:value.
eval_term s t r ->
eval_term s (subst_term e x t) v <->
eval_term {| var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x r) |}
e v
function subst (f:fmla) (x:ident) (t:expr) : fmla =
function subst (f:fmla) (x:ident) (t:term) : fmla =
match f with
| Fterm e -> Fterm (subst_expr e x t)
| Fterm e -> Fterm (subst_term 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)
| Flet y t' f -> Flet y t' (subst f x t)
| Fforall y ty f -> Fforall y ty (subst f 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
forall s:state, f:fmla, x:ident, t:term, r:value, b:bool.
eval_fmla s (subst f x t) b <->
eval_fmla {| var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x r) |}
f b
*)
(* statements *)
......@@ -251,16 +258,14 @@ lemma many_steps_seq:
n = 1 + n1 + n2
(*
predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p
predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p True
(* Hoare triples *)
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
forall s:state. eval_fmla s p ->
forall s:state. eval_fmla s p True ->
forall s':state, n:int. many_steps s i s' Sskip n ->
eval_fmla s' q
eval_fmla s' q True
(* Hoare logic rules *)
......@@ -268,7 +273,7 @@ lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule:
forall q:fmla, x:ident, e:expr.
forall q:fmla, x:ident, e:term.
valid_triple (subst q x e) (Sassign x e) q
lemma seq_rule:
......@@ -277,15 +282,15 @@ lemma seq_rule:
valid_triple p (Sseq i1 i2) q
lemma if_rule:
forall e:expr, p q:fmla, i1 i2:stmt.
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 while_rule:
forall e:expr, inv:fmla, i:stmt.
forall e:term, inv:fmla, i:stmt.
valid_triple (Fand (Fterm e) inv) i inv ->
valid_triple inv (Swhile e i) (Fand (Fnot (Fterm e)) inv)
valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)
lemma consequence_rule:
forall p p' q q':fmla, i:stmt.
......@@ -296,11 +301,10 @@ lemma consequence_rule:
*)
end
(*
module WP
......@@ -317,7 +321,7 @@ module WP
(Fimplies (Fnot (Fterm e)) (wp i2 q))
| Swhile e inv i ->
Fand inv
(Forall (Fand
((*Fforall*) (Fand
(Fimplies (Fand (Fterm e) inv) (wp i inv))
(Fimplies (Fand (Fnot (Fterm e)) inv) q)))
......@@ -326,7 +330,6 @@ module WP
end
*)
(*
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/hoare_logic/wp/why3session.xml">
name="wp/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -9,7 +9,7 @@
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
......@@ -56,7 +56,7 @@
expanded="true">
<goal
name="Test13"
sum="588a68a35eb40a90e89f2604e6fd3683"
sum="c9030241e89dc006dab8cc9ae47a7718"
proved="true"
expanded="true"
shape="aeval_termamy_stateaTconstc13aVintc13">
......@@ -65,12 +65,12 @@
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="Test42"
sum="ad60784608efee681d7bfb6d4657ce64"
sum="1a9081f642f945dbe5d29567cdab6c3b"
proved="true"
expanded="true"
shape="aeval_termamy_stateaTvarc0aVintc42">
......@@ -79,13 +79,13 @@
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="Test55"
sum="a416d24c7e960e30780c57a6ed5795aa"
proved="true"
sum="c836a48e248b70c8e1b24d72622c0c12"
proved="false"
expanded="true"
shape="aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55">
<proof
......@@ -93,12 +93,26 @@
timelimit="5"
edited="wp_Imp_Test55_2.v"
obsolete="false">
<result status="valid" time="0.50"/>
<result status="unknown" time="0.68"/>
</proof>
</goal>
<goal
name="eval_subst_term"
sum="60bd6222851e94fd66727d7e9a0b1017"
proved="false"
expanded="true"
shape="aeval_termamk stateavar_envV0asetaref_envV0V2V4V1V5qaeval_termV0asubst_termV1V2V3V5Iaeval_termV0V3V4F">
</goal>
<goal
name="eval_subst"
sum="ec744e293a652182334adca9e988063f"
proved="false"
expanded="true"
shape="aeval_fmlaamk stateavar_envV0asetaref_envV0V2V4V1V5qaeval_fmlaV0asubstV1V2V3V5F">
</goal>
<goal
name="check_skip"
sum="2dfd7981c1282e38fe4d32469fa442c3"
sum="4639337ccc2425b532d7ff9875c9c4eb"
proved="true"
expanded="true"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
......@@ -112,7 +126,7 @@
</goal>
<goal
name="Ass42"
sum="8329fde7dbe71ed5445e3fe0fbff0f00"
sum="44dd3d1e51c27ee5e8c2c4314633dbd8"
proved="true"
expanded="true"
shape="Lc0ainfix =agetaref_envV1V0aVintc42Iaone_stepamy_stateaSassignV0aTconstc42V1aSskipF">
......@@ -121,26 +135,26 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.15"/>
</proof>
</goal>
<goal
name="If42"
sum="aff6d2fdcb44ce731b6d88a5e11d731e"
proved="true"
sum="8f67af21dfd6689f3ffe63de07f6800a"
proved="false"
expanded="true"
shape="Lc0ainfix =agetaref_envV2V0aVintc42Iaone_stepV1V3V2aSskipIaone_stepamy_stateaSifaTbinaTvarV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V3F">
<proof
prover="coq"
timelimit="5"
edited="wp_Imp_If42_1.v"
obsolete="false">
<result status="valid" time="0.79"/>
obsolete="true">
<result status="unknown" time="0.71"/>
</proof>
</goal>
<goal
name="steps_non_neg"
sum="eadba762cc1a40c7895345dfdf01917a"
sum="0196a8f3e7819c74e6ad8d12303bf434"
proved="false"
expanded="true"
shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
......@@ -148,27 +162,27 @@
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="6.06"/>
obsolete="true">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="8.57"/>
obsolete="true">
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="9.84"/>
obsolete="true">
<result status="timeout" time="5.10"/>
</proof>
</goal>
<goal
name="many_steps_seq"
sum="1c58617d16ff2ed20d6a49c7ff3990ad"
sum="194261c30065d2a593dacbf80e32ffd6"
proved="false"
expanded="true"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
......@@ -176,24 +190,236 @@
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="6.07"/>
obsolete="true">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="8.57"/>
obsolete="true">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="z3"
timelimit="5"