src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 36081 70deefb6c093 child 40163 a462d5207aa6 permissions -rw-r--r--
     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

     9 begin

    10

    11 text {*

    12 We prove correct the verification condition generated from the following

    13 Boogie code:

    14

    15 \begin{verbatim}

    16 type Vertex;

    17 const G: [Vertex, Vertex] int;

    18 axiom (forall x: Vertex, y: Vertex ::  x != y ==> 0 < G[x,y]);

    19 axiom (forall x: Vertex, y: Vertex ::  x == y ==> G[x,y] == 0);

    20

    21 const Infinity: int;

    22 axiom 0 < Infinity;

    23

    24 const Source: Vertex;

    25 var SP: [Vertex] int;

    26

    27 procedure Dijkstra();

    28   modifies SP;

    29   ensures (SP[Source] == 0);

    30   ensures (forall z: Vertex, y: Vertex ::

    31     SP[y] < Infinity && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);

    32   ensures (forall z: Vertex :: z != Source && SP[z] < Infinity ==>

    33     (exists y: Vertex :: SP[y] < SP[z] && SP[z] == SP[y] + G[y,z]));

    34

    35 implementation Dijkstra()

    36 {

    37   var v: Vertex;

    38   var Visited: [Vertex] bool;

    39   var oldSP: [Vertex] int;

    40

    41   havoc SP;

    42   assume (forall x: Vertex :: x == Source ==> SP[x] == 0);

    43   assume (forall x: Vertex :: x != Source ==> SP[x] == Infinity);

    44

    45   havoc Visited;

    46   assume (forall x: Vertex :: !Visited[x]);

    47

    48   while ((exists x: Vertex :: !Visited[x] && SP[x] < Infinity))

    49     invariant (SP[Source] == 0);

    50     invariant (forall x: Vertex :: SP[x] >= 0);

    51     invariant (forall y: Vertex, z: Vertex ::

    52       !Visited[z] && Visited[y] ==> SP[y] <= SP[z]);

    53     invariant (forall z: Vertex, y: Vertex ::

    54       Visited[y] && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);

    55     invariant (forall z: Vertex :: z != Source && SP[z] < Infinity ==>

    56       (exists y: Vertex :: SP[y] < SP[z] && Visited[y] &&

    57         SP[z] == SP[y] + G[y,z]));

    58   {

    59     havoc v;

    60     assume (!Visited[v]);

    61     assume (SP[v] < Infinity);

    62     assume (forall x: Vertex :: !Visited[x] ==> SP[v] <= SP[x]);

    63

    64     Visited[v] := true;

    65

    66     oldSP := SP;

    67     havoc SP;

    68     assume (forall u: Vertex ::

    69       G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u] ==>

    70         SP[u] == oldSP[v] + G[v,u]);

    71     assume (forall u: Vertex ::

    72       !(G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u]) ==>

    73         SP[u] == oldSP[u]);

    74     assert (forall z: Vertex:: SP[z] <= oldSP[z]);

    75     assert (forall y: Vertex:: Visited[y] ==> SP[y] == oldSP[y]);

    76   }

    77 }

    78 \end{verbatim}

    79 *}

    80

    81

    82 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"

    83

    84 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]

    85 declare [[smt_fixed=true]]

    86

    87 boogie_vc Dijkstra

    88   using [[z3_proofs=true]]

    89   by boogie

    90

    91 boogie_end

    92

    93 end