author | bulwahn |
Thu, 12 Jan 2012 10:19:33 +0100 | |
changeset 46193 | 55a4769d0abe |
parent 41601 | fda8511006f9 |
child 47152 | 446cfc760ccf |
permissions | -rw-r--r-- |
33419 | 1 |
(* Title: HOL/Boogie/Examples/Boogie_Dijkstra.thy |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Boogie example: Dijkstra's algorithm *} |
|
6 |
||
7 |
theory Boogie_Dijkstra |
|
8 |
imports Boogie |
|
40540 | 9 |
uses ("Boogie_Dijkstra.b2i") |
33419 | 10 |
begin |
11 |
||
12 |
text {* |
|
13 |
We prove correct the verification condition generated from the following |
|
14 |
Boogie code: |
|
15 |
||
16 |
\begin{verbatim} |
|
17 |
type Vertex; |
|
18 |
const G: [Vertex, Vertex] int; |
|
19 |
axiom (forall x: Vertex, y: Vertex :: x != y ==> 0 < G[x,y]); |
|
20 |
axiom (forall x: Vertex, y: Vertex :: x == y ==> G[x,y] == 0); |
|
21 |
||
22 |
const Infinity: int; |
|
23 |
axiom 0 < Infinity; |
|
24 |
||
25 |
const Source: Vertex; |
|
26 |
var SP: [Vertex] int; |
|
27 |
||
28 |
procedure Dijkstra(); |
|
29 |
modifies SP; |
|
30 |
ensures (SP[Source] == 0); |
|
31 |
ensures (forall z: Vertex, y: Vertex :: |
|
32 |
SP[y] < Infinity && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]); |
|
33 |
ensures (forall z: Vertex :: z != Source && SP[z] < Infinity ==> |
|
34 |
(exists y: Vertex :: SP[y] < SP[z] && SP[z] == SP[y] + G[y,z])); |
|
35 |
||
36 |
implementation Dijkstra() |
|
37 |
{ |
|
38 |
var v: Vertex; |
|
39 |
var Visited: [Vertex] bool; |
|
40 |
var oldSP: [Vertex] int; |
|
41 |
||
42 |
havoc SP; |
|
43 |
assume (forall x: Vertex :: x == Source ==> SP[x] == 0); |
|
44 |
assume (forall x: Vertex :: x != Source ==> SP[x] == Infinity); |
|
45 |
||
46 |
havoc Visited; |
|
47 |
assume (forall x: Vertex :: !Visited[x]); |
|
48 |
||
49 |
while ((exists x: Vertex :: !Visited[x] && SP[x] < Infinity)) |
|
50 |
invariant (SP[Source] == 0); |
|
51 |
invariant (forall x: Vertex :: SP[x] >= 0); |
|
52 |
invariant (forall y: Vertex, z: Vertex :: |
|
53 |
!Visited[z] && Visited[y] ==> SP[y] <= SP[z]); |
|
54 |
invariant (forall z: Vertex, y: Vertex :: |
|
55 |
Visited[y] && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]); |
|
56 |
invariant (forall z: Vertex :: z != Source && SP[z] < Infinity ==> |
|
57 |
(exists y: Vertex :: SP[y] < SP[z] && Visited[y] && |
|
58 |
SP[z] == SP[y] + G[y,z])); |
|
59 |
{ |
|
60 |
havoc v; |
|
61 |
assume (!Visited[v]); |
|
62 |
assume (SP[v] < Infinity); |
|
63 |
assume (forall x: Vertex :: !Visited[x] ==> SP[v] <= SP[x]); |
|
64 |
||
65 |
Visited[v] := true; |
|
66 |
||
67 |
oldSP := SP; |
|
68 |
havoc SP; |
|
69 |
assume (forall u: Vertex :: |
|
70 |
G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u] ==> |
|
71 |
SP[u] == oldSP[v] + G[v,u]); |
|
72 |
assume (forall u: Vertex :: |
|
73 |
!(G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u]) ==> |
|
74 |
SP[u] == oldSP[u]); |
|
75 |
assert (forall z: Vertex:: SP[z] <= oldSP[z]); |
|
76 |
assert (forall y: Vertex:: Visited[y] ==> SP[y] == oldSP[y]); |
|
77 |
} |
|
78 |
} |
|
79 |
\end{verbatim} |
|
80 |
*} |
|
81 |
||
82 |
||
40580
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40540
diff
changeset
|
83 |
boogie_open "Boogie_Dijkstra.b2i" |
33419 | 84 |
|
40513 | 85 |
declare [[smt_certificates="Boogie_Dijkstra.certs"]] |
36081
70deefb6c093
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
boehmes
parents:
34993
diff
changeset
|
86 |
declare [[smt_fixed=true]] |
41601 | 87 |
declare [[smt_oracle=false]] |
34993
bf3b8462732b
updated examples due to changes in the way SMT certificates are stored
boehmes
parents:
34068
diff
changeset
|
88 |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33419
diff
changeset
|
89 |
boogie_vc Dijkstra |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33445
diff
changeset
|
90 |
by boogie |
33419 | 91 |
|
92 |
boogie_end |
|
93 |
||
94 |
end |