src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
author boehmes
Fri Dec 11 15:35:29 2009 +0100 (2009-12-11)
changeset 34068 a78307d72e58
parent 33445 f0c78a28e18e
child 34993 bf3b8462732b
permissions -rw-r--r--
make assertion labels unique already when loading a verification condition,
keep abstract view on verification conditions and provide various splitting operations on verification conditions,
allow to discharge only parts of a verification condition,
extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths,
added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions),
added tactics "boogie", "boogie_all" and "boogie_cases",
dropped tactic "split_vc",
split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands),
dropped (mostly unused) abbreviations
boehmes@33419
     1
(*  Title:      HOL/Boogie/Examples/Boogie_Dijkstra.thy
boehmes@33419
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@33419
     3
*)
boehmes@33419
     4
boehmes@33419
     5
header {* Boogie example: Dijkstra's algorithm *}
boehmes@33419
     6
boehmes@33419
     7
theory Boogie_Dijkstra
boehmes@33419
     8
imports Boogie
boehmes@33419
     9
begin
boehmes@33419
    10
boehmes@33419
    11
text {*
boehmes@33419
    12
We prove correct the verification condition generated from the following
boehmes@33419
    13
Boogie code:
boehmes@33419
    14
boehmes@33419
    15
\begin{verbatim}
boehmes@33419
    16
type Vertex;
boehmes@33419
    17
const G: [Vertex, Vertex] int;
boehmes@33419
    18
axiom (forall x: Vertex, y: Vertex ::  x != y ==> 0 < G[x,y]);
boehmes@33419
    19
axiom (forall x: Vertex, y: Vertex ::  x == y ==> G[x,y] == 0);
boehmes@33419
    20
boehmes@33419
    21
const Infinity: int;
boehmes@33419
    22
axiom 0 < Infinity;
boehmes@33419
    23
boehmes@33419
    24
const Source: Vertex;
boehmes@33419
    25
var SP: [Vertex] int;
boehmes@33419
    26
boehmes@33419
    27
procedure Dijkstra();
boehmes@33419
    28
  modifies SP;
boehmes@33419
    29
  ensures (SP[Source] == 0);
boehmes@33419
    30
  ensures (forall z: Vertex, y: Vertex ::
boehmes@33419
    31
    SP[y] < Infinity && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
boehmes@33419
    32
  ensures (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
boehmes@33419
    33
    (exists y: Vertex :: SP[y] < SP[z] && SP[z] == SP[y] + G[y,z]));
boehmes@33419
    34
boehmes@33419
    35
implementation Dijkstra()
boehmes@33419
    36
{
boehmes@33419
    37
  var v: Vertex;
boehmes@33419
    38
  var Visited: [Vertex] bool;
boehmes@33419
    39
  var oldSP: [Vertex] int;
boehmes@33419
    40
boehmes@33419
    41
  havoc SP;
boehmes@33419
    42
  assume (forall x: Vertex :: x == Source ==> SP[x] == 0);
boehmes@33419
    43
  assume (forall x: Vertex :: x != Source ==> SP[x] == Infinity);
boehmes@33419
    44
boehmes@33419
    45
  havoc Visited;
boehmes@33419
    46
  assume (forall x: Vertex :: !Visited[x]);
boehmes@33419
    47
            
boehmes@33419
    48
  while ((exists x: Vertex :: !Visited[x] && SP[x] < Infinity))
boehmes@33419
    49
    invariant (SP[Source] == 0);
boehmes@33419
    50
    invariant (forall x: Vertex :: SP[x] >= 0);
boehmes@33419
    51
    invariant (forall y: Vertex, z: Vertex :: 
boehmes@33419
    52
      !Visited[z] && Visited[y] ==> SP[y] <= SP[z]);
boehmes@33419
    53
    invariant (forall z: Vertex, y: Vertex ::
boehmes@33419
    54
      Visited[y] && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
boehmes@33419
    55
    invariant (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
boehmes@33419
    56
      (exists y: Vertex :: SP[y] < SP[z] && Visited[y] && 
boehmes@33419
    57
        SP[z] == SP[y] + G[y,z]));
boehmes@33419
    58
  {
boehmes@33419
    59
    havoc v;
boehmes@33419
    60
    assume (!Visited[v]);
boehmes@33419
    61
    assume (SP[v] < Infinity); 
boehmes@33419
    62
    assume (forall x: Vertex :: !Visited[x] ==> SP[v] <= SP[x]);
boehmes@33419
    63
boehmes@33419
    64
    Visited[v] := true;
boehmes@33419
    65
boehmes@33419
    66
    oldSP := SP;
boehmes@33419
    67
    havoc SP;
boehmes@33419
    68
    assume (forall u: Vertex :: 
boehmes@33419
    69
      G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u] ==> 
boehmes@33419
    70
        SP[u] == oldSP[v] + G[v,u]);
boehmes@33419
    71
    assume (forall u: Vertex :: 
boehmes@33419
    72
      !(G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u]) ==> 
boehmes@33419
    73
        SP[u] == oldSP[u]);
boehmes@33419
    74
    assert (forall z: Vertex:: SP[z] <= oldSP[z]);
boehmes@33419
    75
    assert (forall y: Vertex:: Visited[y] ==> SP[y] == oldSP[y]);
boehmes@33419
    76
  }
boehmes@33419
    77
}
boehmes@33419
    78
\end{verbatim}
boehmes@33419
    79
*}
boehmes@33419
    80
boehmes@33419
    81
boehmes@33419
    82
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
boehmes@33419
    83
boehmes@33445
    84
boogie_vc Dijkstra
boehmes@34068
    85
  using [[z3_proofs=true]]
boehmes@33445
    86
  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_Dijkstra"]]
boehmes@34068
    87
  by boogie
boehmes@33419
    88
boehmes@33419
    89
boogie_end 
boehmes@33419
    90
boehmes@33419
    91
end