src/HOL/Boogie/Examples/Boogie_Max.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_Max.thy

     2     Author:     Sascha Boehme, TU Muenchen

     3 *)

     4

     5 header {* Boogie example: get the greatest element of a list *}

     6

     7 theory Boogie_Max

     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 procedure max(array : [int]int, length : int)

    17   returns (max : int);

    18   requires (0 < length);

    19   ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max);

    20   ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max);

    21

    22 implementation max(array : [int]int, length : int) returns (max : int)

    23 {

    24   var p : int, k : int;

    25   max := array[0];

    26   k := 0;

    27   p := 1;

    28   while (p < length)

    29     invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max);

    30     invariant (array[k] == max);

    31   {

    32     if (array[p] > max) { max := array[p]; k := p; }

    33     p := p + 1;

    34   }

    35 }

    36 \end{verbatim}

    37 *}

    38

    39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"

    40

    41 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]

    42 declare [[smt_fixed=true]]

    43

    44 boogie_vc max

    45   using [[z3_proofs=true]]

    46   by boogie

    47

    48 boogie_end

    49

    50 end