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
8fe82db2
Commit
8fe82db2
authored
Oct 13, 2017
by
MARCHE Claude
Browse files
simplified proofs in example dijkstra shortest path
parent
eedb7053
Changes
2
Hide whitespace changes
Inline
Side-by-side
examples/dijkstra/why3session.xml
View file @
8fe82db2
...
...
@@ -26,23 +26,12 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"9"
/></proof>
</goal>
<goal
name=
"Path_shortest_path"
proved=
"true"
>
<transf
name=
"
assert
"
proved=
"true"
arg1=
"
(forall sn. forall d. 0 <= d < sn -> forall v. path src v d -> exists d':int. shortest_path src v d' /\ d' <= d)
"
>
<transf
name=
"
induction
"
proved=
"true"
arg1=
"
d
"
>
<goal
name=
"Path_shortest_path.0"
proved=
"true"
>
<transf
name=
"induction"
proved=
"true"
arg1=
"sn"
>
<goal
name=
"Path_shortest_path.0.0"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Path_shortest_path.0.1"
proved=
"true"
>
<transf
name=
"instantiate"
proved=
"true"
arg1=
"Hrec"
arg2=
"sn"
>
<goal
name=
"Path_shortest_path.0.1.0"
proved=
"true"
>
<proof
prover=
"4"
timelimit=
"5"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
</transf>
</goal>
</transf>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Path_shortest_path.1"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
6
"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -166,24 +155,20 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
steps=
"291"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.16"
expl=
"loop invariant preservation"
proved=
"true"
>
<transf
name=
"
introduce_premises"
proved=
"true"
>
<transf
name=
"
cut"
proved=
"true"
arg1=
"(is_empty su)"
>
<goal
name=
"WP_parameter shortest_path_code.16.0"
expl=
"loop invariant preservation"
proved=
"true"
>
<transf
name=
"cut"
proved=
"true"
arg1=
"(i
s_empty su
)"
>
<transf
name=
"cut"
proved=
"true"
arg1=
"(i
nv_succ src visited q d
)"
>
<goal
name=
"WP_parameter shortest_path_code.16.0.0"
expl=
"loop invariant preservation"
proved=
"true"
>
<transf
name=
"cut"
proved=
"true"
arg1=
"(inv_succ src visited q d)"
>
<goal
name=
"WP_parameter shortest_path_code.16.0.0.0"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.39"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.16.0.0.1"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
</transf>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.35"
/></proof>
</goal>
<goal
name=
"WP_parameter shortest_path_code.16.0.1"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.
02
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.
13
"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter shortest_path_code.16.1"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter shortest_path_code.17"
expl=
"loop variant decrease"
proved=
"true"
>
...
...
examples/dijkstra/why3shapes.gz
View file @
8fe82db2
No preview for this file type
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