Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
62214cba
Commit
62214cba
authored
Oct 25, 2011
by
MARCHE Claude
Browse files
hoare: adding implies connective
parent
80dc916e
Changes
6
Hide whitespace changes
Inline
Side-by-side
examples/hoare_logic/imp_n.why
View file @
62214cba
...
...
@@ -30,7 +30,7 @@ type stmt =
| Swhile expr stmt
lemma check_skip:
forall s:stmt. s=Sskip \/s<>Sskip
forall s:stmt. s=Sskip \/
s<>Sskip
(* program states *)
...
...
examples/hoare_logic/imp_n/imp_n_Imp_assign_rule_1.v
View file @
62214cba
...
...
@@ -118,7 +118,8 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
Inductive
fmla
:=
|
Fterm
:
expr
->
fmla
|
Fand
:
fmla
->
fmla
->
fmla
|
Fnot
:
fmla
->
fmla
.
|
Fnot
:
fmla
->
fmla
|
Fimplies
:
fmla
->
fmla
->
fmla
.
Set
Implicit
Arguments
.
Fixpoint
eval_fmla
(
s
:
(
map
ident
Z
))
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
...
...
@@ -126,6 +127,7 @@ Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
|
(
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
.
...
...
@@ -151,12 +153,16 @@ Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
|
(
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
).
...
...
examples/hoare_logic/imp_n/imp_n_Imp_if_rule_1.v
View file @
62214cba
...
...
@@ -118,7 +118,8 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
Inductive
fmla
:=
|
Fterm
:
expr
->
fmla
|
Fand
:
fmla
->
fmla
->
fmla
|
Fnot
:
fmla
->
fmla
.
|
Fnot
:
fmla
->
fmla
|
Fimplies
:
fmla
->
fmla
->
fmla
.
Set
Implicit
Arguments
.
Fixpoint
eval_fmla
(
s
:
(
map
ident
Z
))
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
...
...
@@ -126,6 +127,7 @@ Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
|
(
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
.
...
...
@@ -151,12 +153,16 @@ Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
|
(
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
).
...
...
examples/hoare_logic/imp_n/imp_n_Imp_seq_rule_1.v
View file @
62214cba
...
...
@@ -118,7 +118,8 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
Inductive
fmla
:=
|
Fterm
:
expr
->
fmla
|
Fand
:
fmla
->
fmla
->
fmla
|
Fnot
:
fmla
->
fmla
.
|
Fnot
:
fmla
->
fmla
|
Fimplies
:
fmla
->
fmla
->
fmla
.
Set
Implicit
Arguments
.
Fixpoint
eval_fmla
(
s
:
(
map
ident
Z
))
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
...
...
@@ -126,6 +127,7 @@ Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
|
(
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
.
...
...
@@ -151,12 +153,16 @@ Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
|
(
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
).
...
...
@@ -178,7 +184,7 @@ intros p q r i1 i2 (H1,H2).
unfold
valid_triple
in
*
.
intros
s
Hp
s
'
n
Hsteps
.
generalize
(
many_steps_seq
_
_
_
_
_
Hsteps
).
intros
(
s2
,(
n1
,(
n2
,(
H3
,(
H4
,
H5
)
))))
.
intros
(
s2
&
n1
&
n2
&
H3
&
H4
&
H5
).
eapply
H2
;
eauto
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
...
...
examples/hoare_logic/imp_n/imp_n_Imp_while_rule_1.v
View file @
62214cba
...
...
@@ -118,7 +118,8 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
Inductive
fmla
:=
|
Fterm
:
expr
->
fmla
|
Fand
:
fmla
->
fmla
->
fmla
|
Fnot
:
fmla
->
fmla
.
|
Fnot
:
fmla
->
fmla
|
Fimplies
:
fmla
->
fmla
->
fmla
.
Set
Implicit
Arguments
.
Fixpoint
eval_fmla
(
s
:
(
map
ident
Z
))
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
...
...
@@ -126,6 +127,7 @@ Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
|
(
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
.
...
...
@@ -151,12 +153,16 @@ Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
|
(
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
).
...
...
@@ -200,7 +206,7 @@ inversion H1; subst; clear H1.
inversion
H2
;
subst
;
clear
H2
.
(
*
case
cond
true
*
)
generalize
(
many_steps_seq
_
_
_
_
_
H3
).
intros
(
s3
,(
n1
,(
n2
,(
h1
,(
h2
,
h3
)
))))
.
intros
(
s3
&
n1
&
n2
&
h1
&
h2
&
h3
).
apply
H
with
(
y
:=
n2
)
(
s
:=
s3
);
auto
.
generalize
(
steps_non_neg
_
_
_
_
_
h1
).
generalize
(
steps_non_neg
_
_
_
_
_
h2
).
...
...
examples/hoare_logic/imp_n/why3session.xml
View file @
62214cba
...
...
@@ -48,17 +48,17 @@
version=
"2.19"
/>
<file
name=
"../imp_n.why"
verified=
"
tru
e"
verified=
"
fals
e"
expanded=
"true"
>
<theory
name=
"Imp"
verified=
"
tru
e"
verified=
"
fals
e"
expanded=
"true"
>
<goal
name=
"ident_eq_dec"
sum=
"ca7c4648761db026ea93d61666f0b79a"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =V0V1NOainfix =V0V1F"
>
<proof
prover=
"alt-ergo"
...
...
@@ -72,7 +72,7 @@
name=
"check_skip"
sum=
"a28ed21b2b531fe3e8a3933e02f27497"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =V0aSskipNOainfix =V0aSskipF"
>
<proof
prover=
"alt-ergo"
...
...
@@ -86,7 +86,7 @@
name=
"Test13"
sum=
"bc53c41524b84304eb79b4e36fef8af8"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"Laconstc0ainfix =aeval_exprV0aEconstc13c13"
>
<proof
prover=
"alt-ergo"
...
...
@@ -100,7 +100,7 @@
name=
"Test42"
sum=
"78671d09729d8ffd84136c2dcf7eb74b"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42"
>
<proof
prover=
"alt-ergo"
...
...
@@ -114,7 +114,7 @@
name=
"Test55"
sum=
"9f1ffc89f69ccb03e44edbf6adfebb8d"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55"
>
<proof
prover=
"alt-ergo"
...
...
@@ -128,7 +128,7 @@
name=
"Ass42"
sum=
"456c846b124e10fccdeb72291a3819b0"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF"
>
<proof
prover=
"alt-ergo"
...
...
@@ -142,7 +142,7 @@
name=
"If42"
sum=
"9c97951c8cf8d86219396907bf0260eb"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F"
>
<proof
prover=
"alt-ergo"
...
...
@@ -156,41 +156,62 @@
name=
"progress"
sum=
"3e029691d2ae6f6e5afe69a1860de120"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"aone_stepV0V1V2V3EIainfix =V1aSskipNF"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_progress_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.45"
/>
<result
status=
"valid"
time=
"0.54"
/>
</proof>
<proof
prover=
"eprover"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"10.01"
/>
</proof>
<proof
prover=
"vampire"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"6.55"
/>
</proof>
<proof
prover=
"spass"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"9.51"
/>
</proof>
</goal>
<goal
name=
"steps_non_neg"
sum=
"7fe79f6298fbe9fbaa31741ffa430e03"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix >=V4c0Iamany_stepsV0V2V1V3V4F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_steps_non_neg_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.46"
/>
</proof>
</goal>
<goal
name=
"many_steps_seq"
sum=
"c4867410343f6c684f9ca00c1536720a"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_many_steps_seq_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.54"
/>
</proof>
</goal>
...
...
@@ -198,7 +219,7 @@
name=
"eval_subst_expr"
sum=
"9528a4415f2f99046bde6107851e9279"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F"
>
<proof
prover=
"coq"
...
...
@@ -212,7 +233,7 @@
name=
"eval_subst"
sum=
"f9958c4b6b55b1609f43dd2ad3432473"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F"
>
<proof
prover=
"coq"
...
...
@@ -226,7 +247,7 @@
name=
"skip_rule"
sum=
"dfc9be1a6c7c1951f0739b5eb00818fa"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleV0aSskipV0F"
>
<proof
prover=
"alt-ergo"
...
...
@@ -239,56 +260,56 @@
<goal
name=
"assign_rule"
sum=
"2ce35dd2e431c206c4ef4d4353dd9c47"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleasubstV0V1V2aSassignV1V2V0F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_assign_rule_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.72"
/>
</proof>
</goal>
<goal
name=
"seq_rule"
sum=
"3da8614c2f6127af09be97a426dc327e"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_seq_rule_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.52"
/>
</proof>
</goal>
<goal
name=
"if_rule"
sum=
"5e738541b92efb7be1706db09a761442"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_if_rule_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.68"
/>
</proof>
</goal>
<goal
name=
"while_rule"
sum=
"17f0b6240f5cfd179c6cea9bfc294a9d"
proved=
"
tru
e"
expanded=
"
fals
e"
proved=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F"
>
<proof
prover=
"coq"
timelimit=
"3"
edited=
"imp_n_Imp_while_rule_1.v"
obsolete=
"
fals
e"
>
obsolete=
"
tru
e"
>
<result
status=
"valid"
time=
"0.57"
/>
</proof>
</goal>
...
...
@@ -296,7 +317,7 @@
name=
"consequence_rule"
sum=
"c6ee564de35ed1dc6ad77dbe593817ba"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F"
>
<proof
prover=
"cvc3"
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment