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