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--
Add lessThan_Suc_eq_insert_0
     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