Commit 7f923798 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

restored former behavior: replaying with time = 2 * time if valid result

parent 34f89899
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="hoare_logic/imp_n/why3session.xml">
name="imp_n/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -28,33 +28,33 @@
expanded="false">
<theory
name="Imp"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
expanded="false">
<goal
name="ident_eq_dec"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="8" loccnumb="6" loccnume="18"
sum="1d2fa1307a90cfa4436e58ca8c4baa8b"
sum="ca7c4648761db026ea93d61666f0b79a"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0V1NOainfix =V0V1F">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="check_skip"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="32" loccnumb="6" loccnume="16"
sum="f37d9a038124492ded7dcc13c243bca4"
sum="a28ed21b2b531fe3e8a3933e02f27497"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
<proof
prover="0"
......@@ -66,27 +66,27 @@
</goal>
<goal
name="Test13"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="59" loccnumb="7" loccnume="13"
sum="79514e82972fcb9fb181a42bdd168a5d"
sum="89034cff3a243960c6fe7b2b2a91966f"
proved="true"
expanded="true"
expanded="false"
shape="Laconstc0ainfix =aeval_exprV0aEconstc13c13">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test42"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="63" loccnumb="7" loccnume="13"
sum="2233d910dd871f7629fbd14fe21880a0"
sum="991bca434c242bd0fc4fcae7860bb583"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42">
<proof
prover="0"
......@@ -98,11 +98,11 @@
</goal>
<goal
name="Test55"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="68" loccnumb="7" loccnume="13"
sum="81f3d89dbb17dd5616d61c746363e319"
sum="13ad67fe0a83a4e1ece624124c864703"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55">
<proof
prover="0"
......@@ -114,43 +114,43 @@
</goal>
<goal
name="Ass42"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="112" loccnumb="7" loccnume="12"
sum="d79dafb4b123bd6d405249e2aeae999f"
sum="2eae993f753f8826c606f370e5382862"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="If42"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="119" loccnumb="7" loccnume="11"
sum="2cf4b33a87e77dc3113cb2270027977a"
sum="12b5437a3440e505c69b24e6e91a75b8"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F">
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.35"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
<goal
name="progress"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="131" loccnumb="8" loccnume="16"
sum="e135ae75103f2c596782b1e202f4ddb9"
sum="1de081684224e7f85881292371e2b0b0"
proved="true"
expanded="true"
expanded="false"
shape="aone_stepV0V1V2V3EIainfix =V1aSskipNF">
<proof
prover="3"
......@@ -158,16 +158,16 @@
edited="imp_n_Imp_progress_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.88"/>
</proof>
</goal>
<goal
name="steps_non_neg"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="148" loccnumb="6" loccnume="19"
sum="c06d3e0c5d7dd6ec160f133b26638127"
sum="9afb86d9042cfb6d235dbe573c99c7af"
proved="true"
expanded="true"
expanded="false"
shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
<proof
prover="3"
......@@ -175,16 +175,16 @@
edited="imp_n_Imp_steps_non_neg_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.50"/>
<result status="valid" time="0.90"/>
</proof>
</goal>
<goal
name="many_steps_seq"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="152" loccnumb="6" loccnume="20"
sum="7b3774594f3da38d257567c4311cf3aa"
sum="63f9f761456c06e15c3369514675fb0d"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
<proof
prover="3"
......@@ -192,16 +192,16 @@
edited="imp_n_Imp_many_steps_seq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="1.06"/>
</proof>
</goal>
<goal
name="eval_subst_expr"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="186" loccnumb="6" loccnume="21"
sum="643838e1957c5f3d1b4fe5d360576662"
sum="e63480504ff35c49144c886bd8a62737"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
<proof
prover="3"
......@@ -209,16 +209,16 @@
edited="imp_n_Imp_eval_subst_expr_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.92"/>
</proof>
</goal>
<goal
name="eval_subst"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="199" loccnumb="6" loccnume="16"
sum="6a0bb6fbede50890f0b19fabc5fe5dfb"
sum="86264772f72216dbeb4b098411b567fc"
proved="true"
expanded="true"
expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
<proof
prover="3"
......@@ -226,32 +226,32 @@
edited="imp_n_Imp_eval_subst_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.93"/>
</proof>
</goal>
<goal
name="skip_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="214" loccnumb="6" loccnume="15"
sum="c57fa5e1d70d2b2e34d5c14c461d1073"
sum="2ad581756a248899fb392c2d4997c804"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.91"/>
</proof>
</goal>
<goal
name="assign_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="217" loccnumb="6" loccnume="17"
sum="ab8509c30c82a4d0b3394529d359ab2c"
sum="40e9ed93ad1f5b1a561275cf534b59fd"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
<proof
prover="3"
......@@ -259,16 +259,16 @@
edited="imp_n_Imp_assign_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.99"/>
</proof>
</goal>
<goal
name="seq_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="221" loccnumb="6" loccnume="14"
sum="e22e0675c7a8b77cffdce31c4036ef71"
sum="523e5a3dbd386e78faa32a502c820e04"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="3"
......@@ -276,16 +276,16 @@
edited="imp_n_Imp_seq_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.53"/>
<result status="valid" time="0.90"/>
</proof>
</goal>
<goal
name="if_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="226" loccnumb="6" loccnume="13"
sum="7f59f316f054a9d9326c1ad96557a6b0"
sum="7328cf68bc5a595e5c87d83b2d1a723e"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
<proof
prover="3"
......@@ -293,16 +293,16 @@
edited="imp_n_Imp_if_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.98"/>
</proof>
</goal>
<goal
name="while_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="232" loccnumb="6" loccnume="16"
sum="b2a2c978a4a7bc44c05a5b1b92c1ad45"
sum="c297af00727ea643f60ade404427e376"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="3"
......@@ -310,30 +310,30 @@
edited="imp_n_Imp_while_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="1.05"/>
</proof>
</goal>
<goal
name="consequence_rule"
locfile="hoare_logic/imp_n/../imp_n.why"
locfile="imp_n/../imp_n.why"
loclnum="237" loccnumb="6" loccnume="22"
sum="d85a7b0c64c9a333ac5f627b5d3411c8"
sum="d312e9ab3334578a19d6c531bed904c6"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="4"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.30"/>
<result status="valid" time="0.47"/>
</proof>
</goal>
</theory>
......
......@@ -59,21 +59,6 @@ function eval_term (sigma:env) (pi:env) (t:term) : value =
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
......@@ -216,23 +201,6 @@ inductive one_step env env stmt env env stmt =
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:
......@@ -266,6 +234,7 @@ lemma many_steps_seq:
n = 1 + n1 + n2
predicate valid_fmla (p:fmla) = forall sigma pi:env. eval_fmla sigma pi p
(*** Hoare triples ***)
......@@ -284,8 +253,61 @@ predicate total_valid_triple (p:fmla) (i:stmt) (q:fmla) =
eval_fmla s' q
*)
end
theory TestSemantics
use import Imp
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
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
end
theory HoareLogic
use import Imp
(* Hoare logic rules (partial correctness) *)
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'
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
......@@ -324,14 +346,14 @@ lemma while_rule_ext:
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 ? *)
(* frame rule *)
end
module WP
use import Imp
use set.Set
......@@ -364,14 +386,6 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
| Swhile _ _ s -> stmt_writes s w
end
end
module WP
use import Imp
use set.Set
let rec compute_writes (s:stmt) : Set.set ident =
{ }
......@@ -401,6 +415,8 @@ module WP
eval_fmla sigma' pi' result
}
use HoareLogic
let rec wp (i:stmt) (q:fmla) =
{ true }
match i with
......
This diff is collapsed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
(* Why3 assumption *)
Inductive datatype :=
| Tint : datatype
| Tbool : datatype .
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
(* Why3 assumption *)
Definition ident := Z.
(* Why3 assumption *)
Inductive term :=
| Tconst : Z -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tbin : term -> operator -> term -> term .
(* Why3 assumption *)
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : Z -> term -> fmla -> fmla
| Fforall : Z -> datatype -> fmla -> fmla .
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
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).
(* Why3 assumption *)
Definition env := (map Z value).
Parameter eval_bin: value -> operator -> value -> value.
Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
y) with
| ((Vint x1), (Vint y1)) =>
match op with
| Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
| Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
| Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
| Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))