Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
125
Issues
125
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
efecb614
Commit
efecb614
authored
Mar 07, 2019
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fixed 'make bench'
parent
8a7974cf
Changes
5
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
627 additions
and
487 deletions
+627
-487
drivers/pvs-common.gen
drivers/pvs-common.gen
+1
-1
examples/WP_revisited/wp2/why3session.xml
examples/WP_revisited/wp2/why3session.xml
+21
-15
examples/WP_revisited/wp2/why3shapes.gz
examples/WP_revisited/wp2/why3shapes.gz
+0
-0
examples/WP_revisited/wp2/wp2_WP_VC_compute_writes_1.v
examples/WP_revisited/wp2/wp2_WP_VC_compute_writes_1.v
+0
-471
examples/WP_revisited/wp2/wp2_WP_VC_compute_writes_2.v
examples/WP_revisited/wp2/wp2_WP_VC_compute_writes_2.v
+605
-0
No files found.
drivers/pvs-common.gen
View file @
efecb614
...
...
@@ -295,7 +295,7 @@ theory set.Set
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop
mem
_empty
remove prop
is_empty
_empty
syntax function add "add(%1, %2)"
syntax function singleton "singleton(%1)"
...
...
examples/WP_revisited/wp2/why3session.xml
View file @
efecb614
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"
5
"
>
<why3session
shape_version=
"
6
"
>
<prover
id=
"0"
name=
"Coq"
version=
"8.7.1"
timelimit=
"3"
steplimit=
"0"
memlimit=
"0"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.4"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Alt-Ergo"
version=
"2.0.0"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"CVC4"
version=
"1.6"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"8"
name=
"Eprover"
version=
"1.8-001"
timelimit=
"30"
steplimit=
"0"
memlimit=
"4000"
/>
<prover
id=
"10"
name=
"Z3"
version=
"4.5.0"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<file
name=
"../wp2.mlw"
proved=
"true"
>
<file
proved=
"true"
>
<path
name=
".."
/>
<path
name=
"wp2.mlw"
/>
<theory
name=
"Imp"
proved=
"true"
>
<goal
name=
"eval_subst_term"
proved=
"true"
>
<transf
name=
"induction_ty_lex"
proved=
"true"
>
...
...
@@ -34,7 +37,7 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"eval_change_free"
proved=
"true"
>
<proof
prover=
"0"
timelimit=
"5"
edited=
"wp2_Imp_eval_change_free_1.v"
><result
status=
"valid"
time=
"
0.34
"
/></proof>
<proof
prover=
"0"
timelimit=
"5"
edited=
"wp2_Imp_eval_change_free_1.v"
><result
status=
"valid"
time=
"
1.30
"
/></proof>
</goal>
<goal
name=
"check_skip"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"2"
/></proof>
...
...
@@ -50,7 +53,7 @@
</transf>
</goal>
<goal
name=
"many_steps_seq"
proved=
"true"
>
<proof
prover=
"0"
edited=
"wp2_Imp_many_steps_seq_1.v"
><result
status=
"valid"
time=
"
0.41
"
/></proof>
<proof
prover=
"0"
edited=
"wp2_Imp_many_steps_seq_1.v"
><result
status=
"valid"
time=
"
1.22
"
/></proof>
</goal>
</theory>
<theory
name=
"TestSemantics"
proved=
"true"
>
...
...
@@ -120,7 +123,7 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.14"
steps=
"407"
/></proof>
</goal>
<goal
name=
"if_rule"
proved=
"true"
>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_if_rule_1.v"
><result
status=
"valid"
time=
"
0.49
"
/></proof>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_if_rule_1.v"
><result
status=
"valid"
time=
"
1.40
"
/></proof>
</goal>
<goal
name=
"assert_rule"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.22"
steps=
"518"
/></proof>
...
...
@@ -129,13 +132,16 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.17"
steps=
"836"
/></proof>
</goal>
<goal
name=
"while_rule"
proved=
"true"
>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_while_rule_1.v"
><result
status=
"valid"
time=
"
0.48
"
/></proof>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_while_rule_1.v"
><result
status=
"valid"
time=
"
1.36
"
/></proof>
</goal>
<goal
name=
"while_rule_ext"
proved=
"true"
>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_while_rule_ext_1.v"
><result
status=
"valid"
time=
"
0.54
"
/></proof>
<proof
prover=
"0"
edited=
"wp2_HoareLogic_while_rule_ext_1.v"
><result
status=
"valid"
time=
"
1.53
"
/></proof>
</goal>
</theory>
<theory
name=
"WP"
proved=
"true"
>
<goal
name=
"S.VC eq"
expl=
"VC for eq"
proved=
"true"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"assigns_refl"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"3"
/></proof>
</goal>
...
...
@@ -143,10 +149,10 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"9"
/></proof>
</goal>
<goal
name=
"assigns_union_left"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
steps=
"1
2
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
steps=
"1
4
"
/></proof>
</goal>
<goal
name=
"assigns_union_right"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"
18
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"
20
"
/></proof>
</goal>
<goal
name=
"VC compute_writes"
expl=
"VC for compute_writes"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
...
...
@@ -168,22 +174,22 @@
<goal
name=
"VC compute_writes.5"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC compute_writes.5.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"
10"
><result
status=
"valid"
time=
"0.04
"
/></proof>
<proof
prover=
"
2"
timelimit=
"1"
><result
status=
"valid"
time=
"0.13"
steps=
"123
"
/></proof>
</goal>
<goal
name=
"VC compute_writes.5.1"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"
2"
timelimit=
"1"
><result
status=
"valid"
time=
"0.13"
steps=
"3
24"
/></proof>
<proof
prover=
"
10"
><result
status=
"valid"
time=
"0.
24"
/></proof>
</goal>
<goal
name=
"VC compute_writes.5.2"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC compute_writes.5.3"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"2"
timelimit=
"1"
><result
status=
"valid"
time=
"0.07"
steps=
"287
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.09"
steps=
"431
"
/></proof>
</goal>
<goal
name=
"VC compute_writes.5.4"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"0"
timelimit=
"
5"
memlimit=
"1000"
edited=
"wp2_WP_VC_compute_writes_1.v"
><result
status=
"valid"
time=
"0.48
"
/></proof>
<proof
prover=
"0"
timelimit=
"
0"
edited=
"wp2_WP_VC_compute_writes_2.v"
><result
status=
"valid"
time=
"1.22
"
/></proof>
</goal>
<goal
name=
"VC compute_writes.5.5"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
32
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
23
"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -224,7 +230,7 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
</goal>
<goal
name=
"VC wp.5.5"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"0"
timelimit=
"0"
edited=
"wp2_WP_VC_wp_1.v"
><result
status=
"valid"
time=
"
0.5
2"
/></proof>
<proof
prover=
"0"
timelimit=
"0"
edited=
"wp2_WP_VC_wp_1.v"
><result
status=
"valid"
time=
"
1.4
2"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/WP_revisited/wp2/why3shapes.gz
View file @
efecb614
No preview for this file type
examples/WP_revisited/wp2/wp2_WP_VC_compute_writes_1.v
deleted
100644 → 0
View file @
8a7974cf
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
HighOrd
.
Require
int
.
Int
.
Require
map
.
Map
.
Require
bool
.
Bool
.
(
*
Why3
assumption
*
)
Inductive
datatype
:=
|
Tint
:
datatype
|
Tbool
:
datatype
.
Axiom
datatype_WhyType
:
WhyType
datatype
.
Existing
Instance
datatype_WhyType
.
(
*
Why3
assumption
*
)
Inductive
operator
:=
|
Oplus
:
operator
|
Ominus
:
operator
|
Omult
:
operator
|
Ole
:
operator
.
Axiom
operator_WhyType
:
WhyType
operator
.
Existing
Instance
operator_WhyType
.
(
*
Why3
assumption
*
)
Definition
ident
:=
Z
.
(
*
Why3
assumption
*
)
Inductive
term
:=
|
Tconst
:
Z
->
term
|
Tvar
:
Z
->
term
|
Tderef
:
Z
->
term
|
Tbin
:
term
->
operator
->
term
->
term
.
Axiom
term_WhyType
:
WhyType
term
.
Existing
Instance
term_WhyType
.
(
*
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
.
Axiom
fmla_WhyType
:
WhyType
fmla
.
Existing
Instance
fmla_WhyType
.
(
*
Why3
assumption
*
)
Inductive
value
:=
|
Vint
:
Z
->
value
|
Vbool
:
bool
->
value
.
Axiom
value_WhyType
:
WhyType
value
.
Existing
Instance
value_WhyType
.
(
*
Why3
assumption
*
)
Definition
env
:=
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
)))
end
|
(
_
,
_
)
=>
((
eval_bin
x
op
y
)
=
(
Vbool
false
))
end
.
(
*
Why3
assumption
*
)
Fixpoint
eval_term
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
t
:
term
)
{
struct
t
}:
value
:=
match
t
with
|
(
Tconst
n
)
=>
Vint
n
|
(
Tvar
id
)
=>
pi
id
|
(
Tderef
id
)
=>
sigma
id
|
(
Tbin
t1
op
t2
)
=>
eval_bin
(
eval_term
sigma
pi
t1
)
op
(
eval_term
sigma
pi
t2
)
end
.
(
*
Why3
assumption
*
)
Fixpoint
eval_fmla
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
match
f
with
|
(
Fterm
t
)
=>
((
eval_term
sigma
pi
t
)
=
(
Vbool
true
))
|
(
Fand
f1
f2
)
=>
(
eval_fmla
sigma
pi
f1
)
/
\
(
eval_fmla
sigma
pi
f2
)
|
(
Fnot
f1
)
=>
~
(
eval_fmla
sigma
pi
f1
)
|
(
Fimplies
f1
f2
)
=>
(
eval_fmla
sigma
pi
f1
)
->
eval_fmla
sigma
pi
f2
|
(
Flet
x
t
f1
)
=>
eval_fmla
sigma
(
map
.
Map
.
set
pi
x
(
eval_term
sigma
pi
t
))
f1
|
(
Fforall
x
Tint
f1
)
=>
forall
(
n
:
Z
),
eval_fmla
sigma
(
map
.
Map
.
set
pi
x
(
Vint
n
))
f1
|
(
Fforall
x
Tbool
f1
)
=>
forall
(
b
:
bool
),
eval_fmla
sigma
(
map
.
Map
.
set
pi
x
(
Vbool
b
))
f1
end
.
Parameter
subst_term
:
term
->
Z
->
Z
->
term
.
Axiom
subst_term_def
:
forall
(
e
:
term
)
(
r
:
Z
)
(
v
:
Z
),
match
e
with
|
(
Tconst
_
)
=>
((
subst_term
e
r
v
)
=
e
)
|
(
Tvar
_
)
=>
((
subst_term
e
r
v
)
=
e
)
|
(
Tderef
x
)
=>
((
r
=
x
)
->
((
subst_term
e
r
v
)
=
(
Tvar
v
)))
/
\
(
~
(
r
=
x
)
->
((
subst_term
e
r
v
)
=
e
))
|
(
Tbin
e1
op
e2
)
=>
((
subst_term
e
r
v
)
=
(
Tbin
(
subst_term
e1
r
v
)
op
(
subst_term
e2
r
v
)))
end
.
(
*
Why3
assumption
*
)
Fixpoint
fresh_in_term
(
id
:
Z
)
(
t
:
term
)
{
struct
t
}:
Prop
:=
match
t
with
|
(
Tconst
_
)
=>
True
|
(
Tvar
v
)
=>
~
(
id
=
v
)
|
(
Tderef
_
)
=>
True
|
(
Tbin
t1
_
t2
)
=>
(
fresh_in_term
id
t1
)
/
\
(
fresh_in_term
id
t2
)
end
.
Axiom
eval_subst_term
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
e
:
term
)
(
x
:
Z
)
(
v
:
Z
),
(
fresh_in_term
v
e
)
->
((
eval_term
sigma
pi
(
subst_term
e
x
v
))
=
(
eval_term
(
map
.
Map
.
set
sigma
x
(
pi
v
))
pi
e
)).
Axiom
eval_term_change_free
:
forall
(
t
:
term
)
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
id
:
Z
)
(
v
:
value
),
(
fresh_in_term
id
t
)
->
((
eval_term
sigma
(
map
.
Map
.
set
pi
id
v
)
t
)
=
(
eval_term
sigma
pi
t
)).
(
*
Why3
assumption
*
)
Fixpoint
fresh_in_fmla
(
id
:
Z
)
(
f
:
fmla
)
{
struct
f
}:
Prop
:=
match
f
with
|
(
Fterm
e
)
=>
fresh_in_term
id
e
|
((
Fand
f1
f2
)
|
(
Fimplies
f1
f2
))
=>
(
fresh_in_fmla
id
f1
)
/
\
(
fresh_in_fmla
id
f2
)
|
(
Fnot
f1
)
=>
fresh_in_fmla
id
f1
|
(
Flet
y
t
f1
)
=>
~
(
id
=
y
)
/
\
((
fresh_in_term
id
t
)
/
\
(
fresh_in_fmla
id
f1
))
|
(
Fforall
y
_
f1
)
=>
~
(
id
=
y
)
/
\
(
fresh_in_fmla
id
f1
)
end
.
(
*
Why3
assumption
*
)
Fixpoint
subst
(
f
:
fmla
)
(
x
:
Z
)
(
v
:
Z
)
{
struct
f
}:
fmla
:=
match
f
with
|
(
Fterm
e
)
=>
Fterm
(
subst_term
e
x
v
)
|
(
Fand
f1
f2
)
=>
Fand
(
subst
f1
x
v
)
(
subst
f2
x
v
)
|
(
Fnot
f1
)
=>
Fnot
(
subst
f1
x
v
)
|
(
Fimplies
f1
f2
)
=>
Fimplies
(
subst
f1
x
v
)
(
subst
f2
x
v
)
|
(
Flet
y
t
f1
)
=>
Flet
y
(
subst_term
t
x
v
)
(
subst
f1
x
v
)
|
(
Fforall
y
ty
f1
)
=>
Fforall
y
ty
(
subst
f1
x
v
)
end
.
Axiom
eval_subst
:
forall
(
f
:
fmla
)
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
x
:
Z
)
(
v
:
Z
),
(
fresh_in_fmla
v
f
)
->
(
eval_fmla
sigma
pi
(
subst
f
x
v
))
<->
(
eval_fmla
(
map
.
Map
.
set
sigma
x
(
pi
v
))
pi
f
).
Axiom
eval_swap
:
forall
(
f
:
fmla
)
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
id1
:
Z
)
(
id2
:
Z
)
(
v1
:
value
)
(
v2
:
value
),
~
(
id1
=
id2
)
->
(
eval_fmla
sigma
(
map
.
Map
.
set
(
map
.
Map
.
set
pi
id1
v1
)
id2
v2
)
f
)
<->
(
eval_fmla
sigma
(
map
.
Map
.
set
(
map
.
Map
.
set
pi
id2
v2
)
id1
v1
)
f
).
Axiom
eval_change_free
:
forall
(
f
:
fmla
)
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
id
:
Z
)
(
v
:
value
),
(
fresh_in_fmla
id
f
)
->
(
eval_fmla
sigma
(
map
.
Map
.
set
pi
id
v
)
f
)
<->
(
eval_fmla
sigma
pi
f
).
(
*
Why3
assumption
*
)
Inductive
stmt
:=
|
Sskip
:
stmt
|
Sassign
:
Z
->
term
->
stmt
|
Sseq
:
stmt
->
stmt
->
stmt
|
Sif
:
term
->
stmt
->
stmt
->
stmt
|
Sassert
:
fmla
->
stmt
|
Swhile
:
term
->
fmla
->
stmt
->
stmt
.
Axiom
stmt_WhyType
:
WhyType
stmt
.
Existing
Instance
stmt_WhyType
.
Axiom
check_skip
:
forall
(
s
:
stmt
),
(
s
=
Sskip
)
\
/
~
(
s
=
Sskip
).
(
*
Why3
assumption
*
)
Inductive
one_step
:
(
Z
->
value
)
->
(
Z
->
value
)
->
stmt
->
(
Z
->
value
)
->
(
Z
->
value
)
->
stmt
->
Prop
:=
|
one_step_assign
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
x
:
Z
)
(
e
:
term
),
one_step
sigma
pi
(
Sassign
x
e
)
(
map
.
Map
.
set
sigma
x
(
eval_term
sigma
pi
e
))
pi
Sskip
|
one_step_seq
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
sigma
'
:
Z
->
value
)
(
pi
'
:
Z
->
value
)
(
i1
:
stmt
)
(
i1
'
:
stmt
)
(
i2
:
stmt
),
(
one_step
sigma
pi
i1
sigma
'
pi
'
i1
'
)
->
one_step
sigma
pi
(
Sseq
i1
i2
)
sigma
'
pi
'
(
Sseq
i1
'
i2
)
|
one_step_seq_skip
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
i
:
stmt
),
one_step
sigma
pi
(
Sseq
Sskip
i
)
sigma
pi
i
|
one_step_if_true
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
e
:
term
)
(
i1
:
stmt
)
(
i2
:
stmt
),
((
eval_term
sigma
pi
e
)
=
(
Vbool
true
))
->
one_step
sigma
pi
(
Sif
e
i1
i2
)
sigma
pi
i1
|
one_step_if_false
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
e
:
term
)
(
i1
:
stmt
)
(
i2
:
stmt
),
((
eval_term
sigma
pi
e
)
=
(
Vbool
false
))
->
one_step
sigma
pi
(
Sif
e
i1
i2
)
sigma
pi
i2
|
one_step_assert
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
f
:
fmla
),
(
eval_fmla
sigma
pi
f
)
->
one_step
sigma
pi
(
Sassert
f
)
sigma
pi
Sskip
|
one_step_while_true
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
e
:
term
)
(
inv
:
fmla
)
(
i
:
stmt
),
(
eval_fmla
sigma
pi
inv
)
->
((
eval_term
sigma
pi
e
)
=
(
Vbool
true
))
->
one_step
sigma
pi
(
Swhile
e
inv
i
)
sigma
pi
(
Sseq
i
(
Swhile
e
inv
i
))
|
one_step_while_false
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
e
:
term
)
(
inv
:
fmla
)
(
i
:
stmt
),
(
eval_fmla
sigma
pi
inv
)
->
((
eval_term
sigma
pi
e
)
=
(
Vbool
false
))
->
one_step
sigma
pi
(
Swhile
e
inv
i
)
sigma
pi
Sskip
.
(
*
Why3
assumption
*
)
Inductive
many_steps
:
(
Z
->
value
)
->
(
Z
->
value
)
->
stmt
->
(
Z
->
value
)
->
(
Z
->
value
)
->
stmt
->
Z
->
Prop
:=
|
many_steps_refl
:
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
i
:
stmt
),
many_steps
sigma
pi
i
sigma
pi
i
0
%
Z
|
many_steps_trans
:
forall
(
sigma1
:
Z
->
value
)
(
pi1
:
Z
->
value
)
(
sigma2
:
Z
->
value
)
(
pi2
:
Z
->
value
)
(
sigma3
:
Z
->
value
)
(
pi3
:
Z
->
value
)
(
i1
:
stmt
)
(
i2
:
stmt
)
(
i3
:
stmt
)
(
n
:
Z
),
(
one_step
sigma1
pi1
i1
sigma2
pi2
i2
)
->
(
many_steps
sigma2
pi2
i2
sigma3
pi3
i3
n
)
->
many_steps
sigma1
pi1
i1
sigma3
pi3
i3
(
n
+
1
%
Z
)
%
Z
.
Axiom
steps_non_neg
:
forall
(
sigma1
:
Z
->
value
)
(
pi1
:
Z
->
value
)
(
sigma2
:
Z
->
value
)
(
pi2
:
Z
->
value
)
(
i1
:
stmt
)
(
i2
:
stmt
)
(
n
:
Z
),
(
many_steps
sigma1
pi1
i1
sigma2
pi2
i2
n
)
->
(
0
%
Z
<=
n
)
%
Z
.
Axiom
many_steps_seq
:
forall
(
sigma1
:
Z
->
value
)
(
pi1
:
Z
->
value
)
(
sigma3
:
Z
->
value
)
(
pi3
:
Z
->
value
)
(
i1
:
stmt
)
(
i2
:
stmt
)
(
n
:
Z
),
(
many_steps
sigma1
pi1
(
Sseq
i1
i2
)
sigma3
pi3
Sskip
n
)
->
exists
sigma2
:
Z
->
value
,
exists
pi2
:
Z
->
value
,
exists
n1
:
Z
,
exists
n2
:
Z
,
(
many_steps
sigma1
pi1
i1
sigma2
pi2
Sskip
n1
)
/
\
((
many_steps
sigma2
pi2
i2
sigma3
pi3
Sskip
n2
)
/
\
(
n
=
((
1
%
Z
+
n1
)
%
Z
+
n2
)
%
Z
)).
(
*
Why3
assumption
*
)
Definition
valid_fmla
(
p
:
fmla
)
:
Prop
:=
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
),
eval_fmla
sigma
pi
p
.
(
*
Why3
assumption
*
)
Definition
valid_triple
(
p
:
fmla
)
(
i
:
stmt
)
(
q
:
fmla
)
:
Prop
:=
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
),
(
eval_fmla
sigma
pi
p
)
->
forall
(
sigma
'
:
Z
->
value
)
(
pi
'
:
Z
->
value
)
(
n
:
Z
),
(
many_steps
sigma
pi
i
sigma
'
pi
'
Sskip
n
)
->
eval_fmla
sigma
'
pi
'
q
.
Axiom
set
:
forall
(
a
:
Type
),
Type
.
Parameter
set_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
set
a
).
Existing
Instance
set_WhyType
.
Parameter
mem
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
Prop
.
Parameter
infix_eqeq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
Prop
.
Axiom
infix_eqeq_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
(
infix_eqeq
s1
s2
)
<->
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Axiom
extensionality
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
(
infix_eqeq
s1
s2
)
->
(
s1
=
s2
).
Parameter
subset
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
Prop
.
Axiom
subset_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
(
subset
s1
s2
)
<->
forall
(
x
:
a
),
(
mem
x
s1
)
->
mem
x
s2
.
Axiom
subset_refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
subset
s
s
.
Axiom
subset_trans
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
)
(
s3
:
set
a
),
(
subset
s1
s2
)
->
(
subset
s2
s3
)
->
subset
s1
s3
.
Parameter
is_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
Prop
.
Axiom
is_empty_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
(
is_empty
s
)
<->
forall
(
x
:
a
),
~
(
mem
x
s
).
Parameter
empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
set
a
.
Axiom
empty_def
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
is_empty
(
empty
:
set
a
).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
set
a
.
Axiom
add_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
set
a
),
forall
(
y
:
a
),
(
mem
y
(
add
x
s
))
<->
((
y
=
x
)
\
/
(
mem
y
s
)).
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
set
a
.
Axiom
remove_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
set
a
),
forall
(
y
:
a
),
(
mem
y
(
remove
x
s
))
<->
(
~
(
y
=
x
)
/
\
(
mem
y
s
)).
Axiom
add_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
set
a
),
(
mem
x
s
)
->
((
add
x
(
remove
x
s
))
=
s
).
Axiom
remove_add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
set
a
),
((
remove
x
(
add
x
s
))
=
(
remove
x
s
)).
Axiom
subset_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
set
a
),
subset
(
remove
x
s
)
s
.
Parameter
union
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
set
a
.
Axiom
union_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
forall
(
x
:
a
),
(
mem
x
(
union
s1
s2
))
<->
((
mem
x
s1
)
\
/
(
mem
x
s2
)).
Parameter
inter
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
set
a
.
Axiom
inter_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
forall
(
x
:
a
),
(
mem
x
(
inter
s1
s2
))
<->
((
mem
x
s1
)
/
\
(
mem
x
s2
)).
Parameter
diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
set
a
.
Axiom
diff_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
forall
(
x
:
a
),
(
mem
x
(
diff
s1
s2
))
<->
((
mem
x
s1
)
/
\
~
(
mem
x
s2
)).
Axiom
subset_diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
subset
(
diff
s1
s2
)
s1
.
Parameter
choose
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
a
.
Axiom
choose_spec
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
~
(
is_empty
s
)
->
mem
(
choose
s
)
s
.
Parameter
cardinal
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
Z
.
Axiom
cardinal_nonneg
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
(
0
%
Z
<=
(
cardinal
s
))
%
Z
.
Axiom
cardinal_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
((
cardinal
s
)
=
0
%
Z
)
<->
(
is_empty
s
).
Axiom
cardinal_add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
forall
(
s
:
set
a
),
~
(
mem
x
s
)
->
((
cardinal
(
add
x
s
))
=
(
1
%
Z
+
(
cardinal
s
))
%
Z
).
Axiom
cardinal_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
forall
(
s
:
set
a
),
(
mem
x
s
)
->
((
cardinal
s
)
=
(
1
%
Z
+
(
cardinal
(
remove
x
s
)))
%
Z
).
Axiom
cardinal_subset
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
(
subset
s1
s2
)
->
((
cardinal
s1
)
<=
(
cardinal
s2
))
%
Z
.
Axiom
subset_eq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
set
a
)
(
s2
:
set
a
),
(
subset
s1
s2
)
->
((
cardinal
s1
)
=
(
cardinal
s2
))
->
infix_eqeq
s1
s2
.
Axiom
cardinal1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
set
a
),
((
cardinal
s
)
=
1
%
Z
)
->
forall
(
x
:
a
),
(
mem
x
s
)
->
(
x
=
(
choose
s
)).
(
*
Why3
assumption
*
)
Definition
assigns
(
sigma
:
Z
->
value
)
(
a
:
set
Z
)
(
sigma
'
:
Z
->
value
)
:
Prop
:=
forall
(
i
:
Z
),
~
(
mem
i
a
)
->
((
sigma
i
)
=
(
sigma
'
i
)).
Axiom
assigns_refl
:
forall
(
sigma
:
Z
->
value
)
(
a
:
set
Z
),
assigns
sigma
a
sigma
.
Axiom
assigns_trans
:
forall
(
sigma1
:
Z
->
value
)
(
sigma2
:
Z
->
value
)
(
sigma3
:
Z
->
value
)
(
a
:
set
Z
),
((
assigns
sigma1
a
sigma2
)
/
\
(
assigns
sigma2
a
sigma3
))
->
assigns
sigma1
a
sigma3
.
Axiom
assigns_union_left
:
forall
(
sigma
:
Z
->
value
)
(
sigma
'
:
Z
->
value
)
(
s1
:
set
Z
)
(
s2
:
set
Z
),
(
assigns
sigma
s1
sigma
'
)
->
assigns
sigma
(
union
s1
s2
)
sigma
'
.
Axiom
assigns_union_right
:
forall
(
sigma
:
Z
->
value
)
(
sigma
'
:
Z
->
value
)
(
s1
:
set
Z
)
(
s2
:
set
Z
),
(
assigns
sigma
s2
sigma
'
)
->
assigns
sigma
(
union
s1
s2
)
sigma
'
.
(
*
Why3
assumption
*
)
Fixpoint
stmt_writes
(
i
:
stmt
)
(
w
:
set
Z
)
{
struct
i
}:
Prop
:=
match
i
with
|
(
Sskip
|
(
Sassert
_
))
=>
True
|
(
Sassign
id
_
)
=>
mem
id
w
|
((
Sseq
s1
s2
)
|
(
Sif
_
s1
s2
))
=>
(
stmt_writes
s1
w
)
/
\
(
stmt_writes
s2
w
)
|
(
Swhile
_
_
s
)
=>
stmt_writes
s
w
end
.
(
*
Why3
goal
*
)
Theorem
VC_compute_writes
:
forall
(
s
:
stmt
),
forall
(
result
:
set
Z
),
(
exists
x
:
term
,
exists
x1
:
fmla
,
exists
x2
:
stmt
,
(
s
=
(
Swhile
x
x1
x2
))
/
\
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
sigma
'
:
Z
->
value
)
(
pi
'
:
Z
->
value
)
(
n
:
Z
),
(
many_steps
sigma
pi
x2
sigma
'
pi
'
Sskip
n
)
->
assigns
sigma
result
sigma
'
)
->
forall
(
sigma
:
Z
->
value
)
(
pi
:
Z
->
value
)
(
sigma
'
:
Z
->
value
)
(
pi
'
:
Z
->
value
)
(
n
:
Z
),
(
many_steps
sigma
pi
s
sigma
'
pi
'
Sskip
n
)
->
assigns
sigma
result
sigma
'
.
(
*
Why3
intros
s
result
(
x
,(
x1
,(
x2
,(
h1
,
h2
))))
sigma
pi
sigma
'
pi
'
n
h3
.
*
)
intros
s
result
(
x
,(
x1
,(
x2
,(
h1
,
h2
))));
rewrite
h1
in
*
.
intros
.
generalize
sigma
pi
sigma
'
pi
'
H
.
generalize
(
steps_non_neg
_
_
_
_
_
_
_
H
).
clear
sigma
pi
sigma
'
pi
'
H
.
intro
H_n_pos
.