Skip to content
GitLab
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
ea4a727a
Commit
ea4a727a
authored
Mar 19, 2015
by
MARCHE Claude
Browse files
fix session
parent
ada95b4c
Changes
4
Hide whitespace changes
Inline
Side-by-side
drivers/smt-libv2.drv
View file @
ea4a727a
...
...
@@ -6,7 +6,7 @@ printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error:
\
\1"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
valid "^unsat"
...
...
examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v
View file @
ea4a727a
...
...
@@ -203,8 +203,11 @@ Definition inv_succ2 (src:vertex) (s:(set vertex)) (q:(set vertex))
((
map
.
Map
.
get
d
y
)
<=
((
map
.
Map
.
get
d
x
)
+
(
weight
x
y
))
%
Z
)
%
Z
)).
Require
Import
Why3
.
Ltac
ae
:=
why3
"Alt-Ergo,0.99.1,"
timelimit
5.
(
*
Ltac
ae0952
:=
why3
"Alt-Ergo,0.95.2,"
timelimit
3.
Ltac
z3
:=
why3
"z3"
timelimit
3.
*
)
(
*
Why3
goal
*
)
Theorem
WP_parameter_shortest_path_code
:
forall
(
src
:
vertex
)
(
dst
:
vertex
),
...
...
@@ -266,8 +269,8 @@ intros src dst d (h1,h2) q d1 visited ((h3,h4),h5) q1 d2 visited1
((
h24
,(
h25
,(
h26
,(
h27
,(
h28
,(
h29
,(
h30
,(
h31
,
h32
)))))))),
h33
)
result
h34
h35
h36
su1
v1
(
h37
,
h38
)
q4
d4
h39
v2
h40
.
*
)
intuition
;
try
ae
0952
.
(
*
note
Alt
-
Ergo
0.99.1
solves
all
!
*
)
intuition
;
try
ae
.
(
*
destruct
(
why_decidable_eq
v2
v1
)
as
[
case
|
case
].
subst
v2
d4
;
rewrite
Map
.
Select_eq
.
apply
Path_cons
.
...
...
@@ -285,5 +288,6 @@ z3.
ae0952
.
trivial
.
ae0952
.
*
)
Qed
.
examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v
View file @
ea4a727a
(
*
This
file
is
generated
by
Why3
'
s
Coq
8.4
driver
*
)
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
...
...
@@ -8,135 +8,133 @@ Require map.Map.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
Axiom
qtmark
:
Type
.
Parameter
qtmark_WhyType
:
WhyType
qtmark
.
Existing
Instance
qtmark_WhyType
.
(
*
Why3
assumption
*
)
Inductive
ref
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
Inductive
ref
(
a
:
Type
)
:=
|
mk_ref
:
a
->
ref
a
.
Axiom
ref_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
ref
a
).
Existing
Instance
ref_WhyType
.
Implicit
Arguments
mk_ref
[[
a
]
[
a_WT
]
].
Implicit
Arguments
mk_ref
[[
a
]].
(
*
Why3
assumption
*
)
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
@
ref
a
a_WT
))
:
a
:=
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
ref
a
))
:
a
:=
match
v
with
|
(
mk_ref
x
)
=>
x
end
.
Axiom
set
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
Type
.
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
a_WT
)
->
Prop
.
Parameter
mem
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
Prop
.
(
*
Why3
assumption
*
)
Definition
infix_eqeq
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Definition
infix_eqeq
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Axiom
extensionality
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
s2
).
Axiom
extensionality
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
s2
).
(
*
Why3
assumption
*
)
Definition
subset
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
Definition
subset
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
Axiom
subset_refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
@
set
a
a_WT
)),
(
subset
s
s
).
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
(
s3
:
(
@
set
a
a_WT
)),
(
subset
s1
s2
)
->
((
subset
s2
s3
)
->
(
subset
s1
s3
)).
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
empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
@
set
a
a_WT
).
Parameter
empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
).
(
*
Why3
assumption
*
)
Definition
is_empty
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s
:
(
@
set
a
a_WT
))
:
Prop
:=
Definition
is_empty
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
~
(
mem
x
s
).
Axiom
empty_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
is_empty
(
empty
:
(
@
set
a
a_WT
))).
Axiom
empty_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
is_empty
(
empty
:
(
set
a
))).
Axiom
mem_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
~
(
mem
x
(
empty
:
(
@
set
a
a_WT
))).
(
empty
:
(
set
a
))).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
add_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
),
forall
(
s
:
(
@
set
a
a_WT
)),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
forall
(
s
:
(
set
a
)),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
remove_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
)
(
s
:
(
@
set
a
a_WT
)),
(
mem
x
(
remove
y
s
))
<->
((
~
(
x
=
y
))
/
\
(
mem
x
s
)).
(
s
:
(
set
a
)),
(
mem
x
(
remove
y
s
))
<->
((
~
(
x
=
y
))
/
\
(
mem
x
s
)).
Axiom
add_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
@
set
a
a_WT
)),
(
mem
x
s
)
->
((
add
x
(
remove
x
s
))
=
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
a_WT
)),
((
remove
x
(
add
x
s
))
=
(
remove
x
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
a_WT
)),
(
subset
(
remove
x
s
)
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
a_WT
)
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
Parameter
union
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
union_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
(
x
:
a
),
(
mem
x
(
union
s1
s2
))
<->
((
mem
x
s1
)
\
/
(
mem
x
s2
)).
Axiom
union_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
union
s1
s2
))
<->
((
mem
x
s1
)
\
/
(
mem
x
s2
)).
Parameter
inter
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
Parameter
inter
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
inter_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
(
x
:
a
),
(
mem
x
(
inter
s1
s2
))
<->
((
mem
x
s1
)
/
\
(
mem
x
s2
)).
Axiom
inter_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
inter
s1
s2
))
<->
((
mem
x
s1
)
/
\
(
mem
x
s2
)).
Parameter
diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
Parameter
diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
diff_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
@
set
a
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
(
x
:
a
),
(
mem
x
(
diff
s1
s2
))
<->
((
mem
x
s1
)
/
\
~
(
mem
x
s2
)).
Axiom
diff_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
)),
(
subset
(
diff
s1
s2
)
s1
).
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_WT
)
->
a
.
Parameter
choose
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
a
.
Axiom
choose_def
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
@
set
a
a_WT
)),
(
~
(
is_empty
s
))
->
(
mem
(
choose
s
)
s
).
Axiom
choose_def
:
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
a_WT
)
->
Z
.
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
a_WT
)),
(
0
%
Z
<=
(
cardinal
s
))
%
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
a_WT
)),
((
cardinal
s
)
=
0
%
Z
)
<->
(
is_empty
s
).
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
a_WT
)),
(
~
(
mem
x
s
))
->
((
cardinal
(
add
x
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
a_WT
)),
(
mem
x
s
)
->
((
cardinal
s
)
=
(
1
%
Z
+
(
cardinal
(
remove
x
s
)))
%
Z
).
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
)),
(
subset
s1
s2
)
->
((
cardinal
s1
)
<=
(
cardinal
s2
))
%
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
cardinal1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
@
set
a
a_WT
)),
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
)).
Axiom
vertex
:
Type
.
Parameter
vertex_WhyType
:
WhyType
vertex
.
Existing
Instance
vertex_WhyType
.
Parameter
v
:
(
@
set
vertex
vertex_WhyType
).
Parameter
v
:
(
set
vertex
).
Parameter
g_succ
:
vertex
->
(
@
set
vertex
vertex_WhyType
).
Parameter
g_succ
:
vertex
->
(
set
vertex
).
Axiom
G_succ_sound
:
forall
(
x
:
vertex
),
(
subset
(
g_succ
x
)
v
).
...
...
@@ -145,12 +143,12 @@ Parameter weight: vertex -> vertex -> Z.
Axiom
Weight_nonneg
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
(
0
%
Z
<=
(
weight
x
y
))
%
Z
.
(
*
Why3
assumption
*
)
Definition
min
(
m
:
vertex
)
(
q
:
(
@
set
vertex
vertex_WhyType
))
(
d
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
:
Prop
:=
(
mem
m
q
)
/
\
forall
(
x
:
vertex
),
(
mem
x
q
)
->
((
map
.
Map
.
get
d
m
)
<=
(
map
.
Map
.
get
d
x
))
%
Z
.
Definition
min
(
m
:
vertex
)
(
q
:
(
set
vertex
))
(
d
:
(
map
.
Map
.
map
vertex
Z
))
:
Prop
:=
(
mem
m
q
)
/
\
forall
(
x
:
vertex
),
(
mem
x
q
)
->
((
map
.
Map
.
get
d
m
)
<=
(
map
.
Map
.
get
d
x
))
%
Z
.
(
*
Why3
assumption
*
)
Inductive
path
:
vertex
->
vertex
->
Z
->
Prop
:=
Inductive
path
:
vertex
->
vertex
->
Z
->
Prop
:=
|
Path_nil
:
forall
(
x
:
vertex
),
(
path
x
x
0
%
Z
)
|
Path_cons
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
),
forall
(
d
:
Z
),
(
path
x
y
d
)
->
((
mem
z
(
g_succ
y
))
->
(
path
x
z
(
d
+
(
weight
y
z
))
%
Z
)).
...
...
@@ -174,42 +172,38 @@ Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
exists
v
'
:
vertex
,
exists
d
'
:
Z
,
(
shortest_path
src
v
'
d
'
)
/
\
((
mem
v1
(
g_succ
v
'
))
/
\
((
d
'
+
(
weight
v
'
v1
))
%
Z
<
d
)
%
Z
))).
Axiom
Completeness_lemma
:
forall
(
s
:
(
@
set
vertex
vertex_WhyType
)),
(
forall
(
v1
:
vertex
),
(
mem
v1
s
)
->
forall
(
w
:
vertex
),
(
mem
w
(
g_succ
v1
))
->
(
mem
w
s
))
->
forall
(
src
:
vertex
),
(
mem
src
s
)
->
forall
(
dst
:
vertex
),
forall
(
d
:
Z
),
(
path
src
dst
d
)
->
(
mem
dst
s
).
Axiom
Completeness_lemma
:
forall
(
s
:
(
set
vertex
)),
(
forall
(
v1
:
vertex
),
(
mem
v1
s
)
->
forall
(
w
:
vertex
),
(
mem
w
(
g_succ
v1
))
->
(
mem
w
s
))
->
forall
(
src
:
vertex
),
(
mem
src
s
)
->
forall
(
dst
:
vertex
),
forall
(
d
:
Z
),
(
path
src
dst
d
)
->
(
mem
dst
s
).
(
*
Why3
assumption
*
)
Definition
inv_src
(
src
:
vertex
)
(
s
:
(
@
set
vertex
vertex_WhyType
))
(
q
:
(
@
set
vertex
vertex_WhyType
))
:
Prop
:=
(
mem
src
s
)
\
/
(
mem
src
q
).
Definition
inv_src
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
:
Prop
:=
(
mem
src
s
)
\
/
(
mem
src
q
).
(
*
Why3
assumption
*
)
Definition
inv
(
src
:
vertex
)
(
s
:
(
@
set
vertex
vertex_WhyType
))
(
q
:
(
@
set
vertex
vertex_WhyType
))
(
d
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
:
Prop
:=
(
inv_src
src
s
q
)
/
\
(((
map
.
Map
.
get
d
src
)
=
0
%
Z
)
/
\
Definition
inv
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
(
d
:
(
map
.
Map
.
map
vertex
Z
))
:
Prop
:=
(
inv_src
src
s
q
)
/
\
(((
map
.
Map
.
get
d
src
)
=
0
%
Z
)
/
\
((
subset
s
v
)
/
\
((
subset
q
v
)
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
q
)
->
~
(
mem
v1
s
))
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
s
)
->
(
shortest_path
src
v1
(
map
.
Map
.
get
d
v1
)))
/
\
forall
(
v1
:
vertex
),
(
mem
v1
q
)
->
(
path
src
v1
(
map
.
Map
.
get
d
v1
))))))).
(
*
Why3
assumption
*
)
Definition
inv_succ
(
src
:
vertex
)
(
s
:
(
@
set
vertex
vertex_WhyType
))
(
q
:
(
@
set
vertex
vertex_WhyType
))
(
d
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
(((
mem
y
s
)
\
/
(
mem
y
q
))
/
\
((
map
.
Map
.
get
d
y
)
<=
((
map
.
Map
.
get
d
x
)
+
(
weight
x
y
))
%
Z
)
%
Z
).
Definition
inv_succ
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
(
d
:
(
map
.
Map
.
map
vertex
Z
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
(((
mem
y
s
)
\
/
(
mem
y
q
))
/
\
((
map
.
Map
.
get
d
y
)
<=
((
map
.
Map
.
get
d
x
)
+
(
weight
x
y
))
%
Z
)
%
Z
).
(
*
Why3
assumption
*
)
Definition
inv_succ2
(
src
:
vertex
)
(
s
:
(
@
set
vertex
vertex_WhyType
))
(
q
:
(
@
set
vertex
vertex_WhyType
))
(
d
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
(
u
:
vertex
)
(
su
:
(
@
set
vertex
vertex_WhyType
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
(((
~
(
x
=
u
))
\
/
((
x
=
u
)
/
\
~
(
mem
y
su
)))
->
(((
mem
y
s
)
\
/
(
mem
y
q
))
/
\
((
map
.
Map
.
get
d
y
)
<=
((
map
.
Map
.
get
d
x
)
+
(
weight
x
y
))
%
Z
)
%
Z
)).
Definition
inv_succ2
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
(
d
:
(
map
.
Map
.
map
vertex
Z
))
(
u
:
vertex
)
(
su
:
(
set
vertex
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
(((
~
(
x
=
u
))
\
/
((
x
=
u
)
/
\
~
(
mem
y
su
)))
->
(((
mem
y
s
)
\
/
(
mem
y
q
))
/
\
((
map
.
Map
.
get
d
y
)
<=
((
map
.
Map
.
get
d
x
)
+
(
weight
x
y
))
%
Z
)
%
Z
)).
Require
Import
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
timelimit
3.
Ltac
z
:=
why3
"z3"
timelimit
3.
Ltac
ae
:=
why3
"Alt-Ergo,0.99.1,"
timelimit
10.
Require
Import
Classical
.
Lemma
inside_or_exit
:
...
...
@@ -235,27 +229,27 @@ Qed.
(
*
Why3
goal
*
)
Theorem
WP_parameter_shortest_path_code
:
forall
(
src
:
vertex
)
(
dst
:
vertex
),
forall
(
d
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
)),
((
mem
src
v
)
/
\
(
mem
dst
v
))
->
forall
(
q
:
(
@
set
vertex
vertex_WhyType
))
(
d1
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
(
visited
:
(
@
set
vertex
vertex_WhyType
)),
((
is_empty
visited
)
/
\
((
q
=
(
add
src
(
empty
:
(
@
set
vertex
vertex_WhyType
))))
/
\
(
d1
=
(
map
.
Map
.
set
d
src
0
%
Z
))))
->
forall
(
q1
:
(
@
set
vertex
vertex_WhyType
))
(
d2
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
))
(
visited1
:
(
@
set
vertex
vertex_WhyType
)),
((
inv
src
visited1
q1
d2
)
/
\
((
inv_succ
src
visited1
q1
d2
)
/
\
forall
(
m
:
vertex
),
(
min
m
q1
d2
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
forall
(
d
:
(
map
.
Map
.
map
vertex
Z
)),
((
mem
src
v
)
/
\
(
mem
dst
v
))
->
forall
(
q
:
(
set
vertex
))
(
d1
:
(
map
.
Map
.
map
vertex
Z
))
(
visited
:
(
set
vertex
)),
((
is_empty
visited
)
/
\
((
q
=
(
add
src
(
empty
:
(
set
vertex
))))
/
\
(
d1
=
(
map
.
Map
.
set
d
src
0
%
Z
))))
->
forall
(
q1
:
(
set
vertex
))
(
d2
:
(
map
.
Map
.
map
vertex
Z
))
(
visited1
:
(
set
vertex
)),
((
inv
src
visited1
q1
d2
)
/
\
((
inv_succ
src
visited1
q1
d2
)
/
\
forall
(
m
:
vertex
),
(
min
m
q1
d2
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
((
dx
<
(
map
.
Map
.
get
d2
m
))
%
Z
->
(
mem
x
visited1
))))
->
forall
(
o
:
bool
),
((
o
=
true
)
<->
(
is_empty
q1
))
->
((
~
(
o
=
true
))
->
((
~
(
is_empty
q1
))
->
forall
(
q2
:
(
@
set
vertex
vertex_WhyType
)),
forall
(
u
:
vertex
),
((
min
u
q1
d2
)
/
\
(
q2
=
(
remove
u
q1
)))
->
((
shortest_path
src
u
(
map
.
Map
.
get
d2
u
))
->
forall
(
visited2
:
(
@
set
vertex
vertex_WhyType
)),
(
visited2
=
(
add
u
visited1
))
->
forall
(
su
:
(
@
set
vertex
vertex_WhyType
))
(
q3
:
(
@
set
vertex
vertex_WhyType
))
(
d3
:
(
@
map
.
Map
.
map
vertex
vertex_WhyType
Z
_
)),
forall
(
q2
:
(
set
vertex
)),
forall
(
u
:
vertex
),
((
min
u
q1
d2
)
/
\
(
q2
=
(
remove
u
q1
)))
->
((
shortest_path
src
u
(
map
.
Map
.
get
d2
u
))
->
forall
(
visited2
:
(
set
vertex
)),
(
visited2
=
(
add
u
visited1
))
->
forall
(
su
:
(
set
vertex
))
(
q3
:
(
set
vertex
))
(
d3
:
(
map
.
Map
.
map
vertex
Z
)),
((
subset
su
(
g_succ
u
))
/
\
((
inv
src
visited2
q3
d3
)
/
\
(
inv_succ2
src
visited2
q3
d3
u
su
)))
->
forall
(
result
:
bool
),
((
result
=
true
)
<->
~
(
is_empty
su
))
->
((
~
(
result
=
true
))
->
forall
(
m
:
vertex
),
(
min
m
q3
d3
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
((
dx
<
(
map
.
Map
.
get
d3
m
))
%
Z
->
(
mem
x
visited2
)))))).
(
*
Why3
intros
src
dst
d
(
h1
,
h2
)
q
d1
visited
(
h3
,(
h4
,
h5
))
q1
d2
visited1
(
h6
,(
h7
,
h8
))
o
h9
h10
h11
q2
u
(
h12
,
h13
)
h14
visited2
h15
su
q3
d3
(
h16
,(
h17
,
h18
))
result
h19
h20
m
h21
x
dx
h22
h23
.
*
)
intros
src
dst
d
(
h1
,
h2
)
q
d1
visited
(
h3
,(
h4
,
h5
))
q1
d2
visited1
(
h6
,(
h7
,
h8
))
o
h9
h10
h11
q2
u
(
h12
,
h13
)
h14
visited2
h15
su
q3
d3
(
h16
,(
h17
,
h18
))
result
h19
h20
m
h21
x
dx
h22
h23
.
...
...
@@ -263,15 +257,16 @@ intros src dst d (h1,h2) q d1 visited (h3,(h4,h5)) q1 d2 visited1
assert
(
is_empty
su
)
by
ae
.
clear
result
h19
h20
.
assert
(
inv_succ
src
visited2
q3
d3
).
unfold
inv_succ
.
split
;
z
.
unfold
inv_succ
.
split
;
ae
.
assert
(
mem
src
visited2
)
by
ae
.
destruct
(
inside_or_exit
visited2
src
x
dx
);
auto
.
destruct
H2
as
(
y
,
(
z
,
(
dy
,
(
a1
,
(
a2
,
(
a3
,
(
a4
,
a5
))))))).
unfold
min
in
h21
.
assert
(
mem
z
q3
)
by
z
.
assert
(
Map
.
get
d3
z
<=
Map
.
get
d3
y
+
weight
y
z
)
%
Z
by
ae
.
assert
(
dy
=
Map
.
get
d3
y
)
by
z
.
z
.
assert
(
mem
z
q3
)
by
ae
.
assert
(
Map
.
get
d3
z
<=
Map
.
get
d3
y
+
weight
y
z
)
%
Z
by
ae
.
assert
(
dy
=
Map
.
get
d3
y
)
by
ae
.
ae
.
Qed
.
examples/dijkstra/why3session.xml
View file @
ea4a727a
...
...
@@ -152,7 +152,7 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.42"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.12.1.7"
expl=
"7."
>
<proof
prover=
"1"
edited=
"dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"
><result
status=
"valid"
time=
"
11.12
"
/></proof>
<proof
prover=
"1"
edited=
"dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"
><result
status=
"valid"
time=
"
4.74
"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -187,7 +187,7 @@
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.17"
expl=
"17. loop invariant preservation"
>
<proof
prover=
"1"
edited=
"dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"
><result
status=
"valid"
time=
"
2.40
"
/></proof>
<proof
prover=
"1"
edited=
"dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"
><result
status=
"valid"
time=
"
6.55
"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.18"
expl=
"18. loop variant decrease"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.07"
/></proof>
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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