src/HOL/Boogie/Examples/Boogie_Max.thy
 author boehmes Fri Nov 13 15:11:41 2009 +0100 (2009-11-13) changeset 33663 a84fd6385832 parent 33445 f0c78a28e18e child 34068 a78307d72e58 permissions -rw-r--r--
adapted proofs due to changes in HOL-Boogie
     1 (*  Title:      HOL/Boogie/Examples/Boogie_Dijkstra.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 text {*

    42 Approach 1: Discharge the verification condition fully automatically by SMT:

    43 *}

    44 boogie_vc max

    45   unfolding labels

    46   using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_max"]]

    47   using [[z3_proofs=true]]

    48   by (smt boogie)

    49

    50 text {*

    51 Approach 2: Split the verification condition, try to solve the splinters by

    52 a selection of automated proof tools, and show the remaining subgoals by an

    53 explicit proof. This approach is most useful in an interactive debug-and-fix

    54 mode.

    55 *}

    56 boogie_vc max

    57 proof (split_vc (verbose) try: fast simp)

    58   print_cases

    59   case L_14_5c

    60   thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)

    61 next

    62   case L_14_5b

    63   thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)

    64 next

    65   case L_14_5a

    66   note max0 = max0 = array 0

    67   {

    68     fix i :: int

    69     assume "0 \<le> i \<and> i < 1"

    70     hence "i = 0" by simp

    71     with max0 have "array i \<le> max0" by simp

    72   }

    73   thus ?case by simp

    74 qed

    75

    76 boogie_end

    77

    78 end