Commit 63ca4c96 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Coq printer does not replace "'" by "qt" in identifiers anymore

parent 5b3a5369
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="wp4/why3session.xml">
<prover
......@@ -21,13 +21,17 @@
<prover
id="4"
name="Coq"
version="8.3pl4"/>
version="8.3pl3"/>
<prover
id="5"
name="Coq"
version="8.3pl4"/>
<prover
id="6"
name="Z3"
version="2.19"/>
<prover
id="6"
id="7"
name="Z3"
version="3.2"/>
<file
......@@ -131,7 +135,7 @@
expanded="false"
shape="ainfix =aeval_termV0V1asubst_termV2V3V4aeval_termasetV0V3aget_stackV4V1V1V2Iafresh_in_termV4V2F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_eval_subst_term_1.v"
......@@ -149,7 +153,7 @@
expanded="false"
shape="ainfix =aeval_termV0V1avsubst_termV2V3aTvalueV4aeval_termV0aConsaTuple2V3V4V1V2F">
<proof
prover="4"
prover="5"
timelimit="20"
memlimit="1000"
edited="wp4_ImpExpr_eval_vsubst_term_1.v"
......@@ -167,7 +171,7 @@
expanded="false"
shape="ainfix =aeval_termV1aConsaTuple2V3V4V2V0aeval_termV1V2V0Iafresh_in_termV3V0F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_eval_term_change_free_1.v"
......@@ -185,7 +189,7 @@
expanded="false"
shape="aeval_fmlaasetV1V3aget_stackV4V2V2V0qaeval_fmlaV1V2asubstV0V3V4Iafresh_in_fmlaV4V0F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_eval_subst_1.v"
......@@ -212,7 +216,7 @@
expanded="true"
shape="aeval_fmlaV1aConsaTuple2V4V6aConsaTuple2V3V5V2V0qaeval_fmlaV1aConsaTuple2V3V5aConsaTuple2V4V6V2V0Iainfix =V3V4NF">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_eval_swap_1.v"
......@@ -230,7 +234,7 @@
expanded="false"
shape="aeval_fmlaV1V2V0qaeval_fmlaV1aConsaTuple2V3V4V2V0Iafresh_in_fmlaV3V0F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_eval_change_free_1.v"
......@@ -248,7 +252,7 @@
expanded="false"
shape="ainfix &gt;=V6c0Iamany_stepsV0V2V4V1V3V5V6F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_steps_non_neg_1.v"
......@@ -266,7 +270,7 @@
expanded="false"
shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V1V3avoidV10Aamany_stepsV0V2V4V7V8avoidV9EIamany_stepsV0V2aEseqV4V5V1V3avoidV6F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_many_steps_seq_1.v"
......@@ -284,7 +288,7 @@
expanded="false"
shape="ainfix =V8ainfix +ainfix +c1V12V13Aamany_stepsV9aConsaTuple2V4V11V10V6V1V3aEvalueV7V13Aamany_stepsV0V2V5V9V10aEvalueV11V12EIamany_stepsV0V2aEletV4V5V6V1V3aEvalueV7V8F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
edited="wp4_ImpExpr_many_steps_let_1.v"
......@@ -350,7 +354,7 @@
<result status="valid" time="0.05"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -392,7 +396,7 @@
expanded="false"
shape="amany_stepsamy_sigmaamy_piaEvarc0amy_sigmaamy_piaEvalueaVintc42c1">
<proof
prover="4"
prover="5"
timelimit="20"
memlimit="1000"
edited="wp4_TestSemantics_Test42expr_1.v"
......@@ -451,7 +455,7 @@
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -484,7 +488,7 @@
<result status="timeout" time="2.03"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -517,7 +521,7 @@
<result status="timeout" time="2.11"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -550,7 +554,7 @@
<result status="valid" time="0.28"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -575,7 +579,7 @@
<result status="valid" time="1.70"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -595,65 +599,17 @@
locfile="wp4/../wp4.mlw"
loclnum="400" loccnumb="6" loccnume="22"
sum="afa11be50c2373b8af95b59b3b7f1730"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="5"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="12.09"/>
</proof>
<proof
prover="0"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="20.00"/>
</proof>
<proof
prover="2"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="20.10"/>
</proof>
<proof
prover="3"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="20.10"/>
</proof>
<proof
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="outofmemory" time="9.09"/>
</proof>
<proof
prover="4"
timelimit="20"
memlimit="1000"
edited="wp4_HoareLogic_consequence_rule_1.v"
obsolete="true"
archived="false"><undone/>
</proof>
<proof
prover="1"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="19.94"/>
<result status="valid" time="0.84"/>
</proof>
</goal>
<goal
......@@ -665,7 +621,7 @@
expanded="false"
shape="avalid_tripleavsubstV0aresultaTvalueV1aEvalueV1V0F">
<proof
prover="4"
prover="5"
timelimit="20"
memlimit="1000"
edited="wp4_HoareLogic_value_rule_1.v"
......@@ -683,7 +639,7 @@
expanded="true"
shape="avalid_tripleV0aEassignV2V3V1Iavalid_tripleV0V3asubstV1V2aresultF">
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -715,7 +671,7 @@
<result status="timeout" time="20.13"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -740,12 +696,12 @@
expanded="true"
shape="avalid_tripleV0aEseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="10.17"/>
<result status="failure" time="10.17"/>
</proof>
<proof
prover="2"
......@@ -772,7 +728,7 @@
<result status="outofmemory" time="16.11"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -797,7 +753,7 @@
expanded="false"
shape="avalid_tripleV0aEletV3V4V5V1Iavalid_tripleaFletaresultaTvarV3V2V5V1Aavalid_tripleV0V4V2Iafresh_in_fmlaV3V2Iainfix =V3aresultNF">
<proof
prover="4"
prover="5"
timelimit="3"
memlimit="1000"
edited="wp4_HoareLogic_let_rule_1.v"
......@@ -815,12 +771,12 @@
expanded="true"
shape="avalid_tripleV1aEassertV0V1Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="11.57"/>
<result status="failure" time="11.57"/>
</proof>
<proof
prover="2"
......@@ -847,7 +803,7 @@
</proof>
<proof
prover="6"
prover="7"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -872,7 +828,7 @@
expanded="true"
shape="avalid_tripleaFimpliesV0V1aEassertV0V1F">
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -904,7 +860,7 @@
</proof>
<proof
prover="6"
prover="7"
timelimit="20"
memlimit="1000"
obsolete="false"
......
......@@ -278,35 +278,35 @@ Inductive one_step : (map refident value) -> (list (Z* value)%type) -> expr
| one_step_deref : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (r:refident), (one_step sigma pi (Ederef r) sigma pi
(Evalue (get sigma r)))
| one_step_assign_ctxt : forall (sigma:(map refident value)) (sigmaqt:(map
refident value)) (pi:(list (Z* value)%type)) (piqt:(list (Z*
value)%type)) (x:refident) (e:expr) (eqt:expr), (one_step sigma pi e
sigmaqt piqt eqt) -> (one_step sigma pi (Eassign x e) sigmaqt piqt
(Eassign x eqt))
| one_step_assign_ctxt : forall (sigma:(map refident value)) (sigma':(map
refident value)) (pi:(list (Z* value)%type)) (pi':(list (Z*
value)%type)) (x:refident) (e:expr) (e':expr), (one_step sigma pi e
sigma' pi' e') -> (one_step sigma pi (Eassign x e) sigma' pi'
(Eassign x e'))
| one_step_assign_value : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (x:refident) (v:value), (one_step sigma pi (Eassign x
(Evalue v)) (set sigma x v) pi (Evalue Vvoid))
| one_step_seq_ctxt : forall (sigma:(map refident value)) (sigmaqt:(map
refident value)) (pi:(list (Z* value)%type)) (piqt:(list (Z*
value)%type)) (e1:expr) (e1qt:expr) (e2:expr), (one_step sigma pi e1
sigmaqt piqt e1qt) -> (one_step sigma pi (Eseq e1 e2) sigmaqt piqt
(Eseq e1qt e2))
| one_step_seq_ctxt : forall (sigma:(map refident value)) (sigma':(map
refident value)) (pi:(list (Z* value)%type)) (pi':(list (Z*
value)%type)) (e1:expr) (e1':expr) (e2:expr), (one_step sigma pi e1
sigma' pi' e1') -> (one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1'
e2))
| one_step_seq_value : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e:expr), (one_step sigma pi (Eseq (Evalue Vvoid) e)
sigma pi e)
| one_step_let_ctxt : forall (sigma:(map refident value)) (sigmaqt:(map
refident value)) (pi:(list (Z* value)%type)) (piqt:(list (Z*
value)%type)) (id:Z) (e1:expr) (e1qt:expr) (e2:expr), (one_step sigma
pi e1 sigmaqt piqt e1qt) -> (one_step sigma pi (Elet id e1 e2) sigmaqt
piqt (Elet id e1qt e2))
| one_step_let_ctxt : forall (sigma:(map refident value)) (sigma':(map
refident value)) (pi:(list (Z* value)%type)) (pi':(list (Z*
value)%type)) (id:Z) (e1:expr) (e1':expr) (e2:expr), (one_step sigma pi
e1 sigma' pi' e1') -> (one_step sigma pi (Elet id e1 e2) sigma' pi'
(Elet id e1' e2))
| one_step_let_value : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (id:Z) (v:value) (e:expr), (one_step sigma pi (Elet id
(Evalue v) e) sigma (Cons (id, v) pi) e)
| one_step_if_ctxt : forall (sigma:(map refident value)) (sigmaqt:(map
refident value)) (pi:(list (Z* value)%type)) (piqt:(list (Z*
value)%type)) (e1:expr) (e1qt:expr) (e2:expr) (e3:expr),
(one_step sigma pi e1 sigmaqt piqt e1qt) -> (one_step sigma pi (Eif e1
e2 e3) sigmaqt piqt (Eif e1qt e2 e3))
| one_step_if_ctxt : forall (sigma:(map refident value)) (sigma':(map
refident value)) (pi:(list (Z* value)%type)) (pi':(list (Z*
value)%type)) (e1:expr) (e1':expr) (e2:expr) (e3:expr), (one_step sigma
pi e1 sigma' pi' e1') -> (one_step sigma pi (Eif e1 e2 e3) sigma' pi'
(Eif e1' e2 e3))
| one_step_if_true : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e1:expr) (e2:expr), (one_step sigma pi
(Eif (Evalue (Vbool true)) e1 e2) sigma pi e1)
......@@ -317,8 +317,8 @@ Inductive one_step : (map refident value) -> (list (Z* value)%type) -> expr
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Eassert f) sigma pi (Evalue Vvoid))
| one_step_while : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e:expr) (inv:fmla) (eqt:expr), (one_step sigma pi
(Ewhile e inv eqt) sigma pi (Eif e (Eseq eqt (Ewhile e inv eqt))
value)%type)) (e:expr) (inv:fmla) (e':expr), (one_step sigma pi
(Ewhile e inv e') sigma pi (Eif e (Eseq e' (Ewhile e inv e'))
(Evalue Vvoid))).
(* Why3 assumption *)
......@@ -362,18 +362,24 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map refident value))
(* Why3 assumption *)
Definition valid_triple(p:fmla) (e:expr) (q:fmla): Prop := forall (sigma:(map
refident value)) (pi:(list (Z* value)%type)), (eval_fmla sigma pi p) ->
forall (sigmaqt:(map refident value)) (piqt:(list (Z* value)%type))
(v:value) (n:Z), (many_steps sigma pi e sigmaqt piqt (Evalue v) n) ->
(eval_fmla sigmaqt (Cons ((-1%Z)%Z, v) piqt) q).
forall (sigma':(map refident value)) (pi':(list (Z* value)%type)) (v:value)
(n:Z), (many_steps sigma pi e sigma' pi' (Evalue v) n) -> (eval_fmla sigma'
(Cons ((-1%Z)%Z, v) pi') q).
(* Why3 goal *)
Theorem consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(e:expr), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p e q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt e qqt))).
Theorem consequence_rule : forall (p:fmla) (p':fmla) (q:fmla) (q':fmla)
(e:expr), (valid_fmla (Fimplies p' p)) -> ((valid_triple p e q) ->
((valid_fmla (Fimplies q q')) -> (valid_triple p' e q'))).
intros p p' q q' e h1 h2 h3.
unfold valid_triple, valid_fmla in *.
intros.
simpl in h3.
apply h3.
eapply h2.
simpl in h1.
apply h1.
apply H.
apply H0.
Qed.
......@@ -33,6 +33,16 @@ let black_list =
[ "at"; "cofix"; "exists2"; "fix"; "IF"; "left"; "mod"; "Prop";
"return"; "right"; "Set"; "Type"; "using"; "where"; ]
let char_to_alpha c =
match c with
| '\'' -> String.make 1 c
| _ -> Ident.char_to_alpha c
let char_to_alnumus c =
match c with
| '\'' -> String.make 1 c
| _ -> Ident.char_to_alnumus c
let fresh_printer () =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer black_list ~sanitizer:isanitize
......
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