src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
author boehmes
Thu, 05 Nov 2009 14:48:40 +0100
changeset 33445 f0c78a28e18e
parent 33419 8ae45e87b992
child 34068 a78307d72e58
permissions -rw-r--r--
shorter names for variables and verification conditions, auto-fix variables occurring in a verification condition
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Boogie/Examples/Boogie_Dijkstra.thy
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     3
*)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     4
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     5
header {* Boogie example: Dijkstra's algorithm *}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     6
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     7
theory Boogie_Dijkstra
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     8
imports Boogie
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     9
begin
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    10
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    11
text {*
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    12
We prove correct the verification condition generated from the following
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    13
Boogie code:
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    14
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    15
\begin{verbatim}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    16
type Vertex;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    17
const G: [Vertex, Vertex] int;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    18
axiom (forall x: Vertex, y: Vertex ::  x != y ==> 0 < G[x,y]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    19
axiom (forall x: Vertex, y: Vertex ::  x == y ==> G[x,y] == 0);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    20
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    21
const Infinity: int;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    22
axiom 0 < Infinity;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    23
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    24
const Source: Vertex;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    25
var SP: [Vertex] int;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    26
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    27
procedure Dijkstra();
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    28
  modifies SP;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    29
  ensures (SP[Source] == 0);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    30
  ensures (forall z: Vertex, y: Vertex ::
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    31
    SP[y] < Infinity && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    32
  ensures (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    33
    (exists y: Vertex :: SP[y] < SP[z] && SP[z] == SP[y] + G[y,z]));
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    34
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    35
implementation Dijkstra()
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    36
{
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    37
  var v: Vertex;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    38
  var Visited: [Vertex] bool;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    39
  var oldSP: [Vertex] int;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    40
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    41
  havoc SP;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    42
  assume (forall x: Vertex :: x == Source ==> SP[x] == 0);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    43
  assume (forall x: Vertex :: x != Source ==> SP[x] == Infinity);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    44
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    45
  havoc Visited;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    46
  assume (forall x: Vertex :: !Visited[x]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    47
            
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    48
  while ((exists x: Vertex :: !Visited[x] && SP[x] < Infinity))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    49
    invariant (SP[Source] == 0);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    50
    invariant (forall x: Vertex :: SP[x] >= 0);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    51
    invariant (forall y: Vertex, z: Vertex :: 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    52
      !Visited[z] && Visited[y] ==> SP[y] <= SP[z]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    53
    invariant (forall z: Vertex, y: Vertex ::
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    54
      Visited[y] && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    55
    invariant (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    56
      (exists y: Vertex :: SP[y] < SP[z] && Visited[y] && 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    57
        SP[z] == SP[y] + G[y,z]));
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    58
  {
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    59
    havoc v;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    60
    assume (!Visited[v]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    61
    assume (SP[v] < Infinity); 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    62
    assume (forall x: Vertex :: !Visited[x] ==> SP[v] <= SP[x]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    63
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    64
    Visited[v] := true;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    65
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    66
    oldSP := SP;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    67
    havoc SP;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    68
    assume (forall u: Vertex :: 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    69
      G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u] ==> 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    70
        SP[u] == oldSP[v] + G[v,u]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    71
    assume (forall u: Vertex :: 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    72
      !(G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u]) ==> 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    73
        SP[u] == oldSP[u]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    74
    assert (forall z: Vertex:: SP[z] <= oldSP[z]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    75
    assert (forall y: Vertex:: Visited[y] ==> SP[y] == oldSP[y]);
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    76
  }
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    77
}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    78
\end{verbatim}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    79
*}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    80
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    81
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    82
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    83
33445
f0c78a28e18e shorter names for variables and verification conditions,
boehmes
parents: 33419
diff changeset
    84
boogie_vc Dijkstra
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    85
  unfolding labels
33445
f0c78a28e18e shorter names for variables and verification conditions,
boehmes
parents: 33419
diff changeset
    86
  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_Dijkstra"]]
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    87
  using [[z3_proofs=true]]
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    88
  by (smt boogie)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    89
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    90
boogie_end 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    91
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    92
end