src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 35323 259931828ecc child 40514 db5f14910dce permissions -rw-r--r--
     1 (*  Title:      HOL/Boogie/Examples/Boogie_Max_Stepwise.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_Stepwise

     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 boogie_status -- {* gives an overview of all verification conditions *}

    42

    43 boogie_status max -- {* shows the names of all unproved assertions

    44   of the verification condition @{text max} *}

    45

    46 boogie_status (full) max -- {* shows the state of all assertions

    47   of the verification condition @{text max} *}

    48

    49 boogie_status (paths) max -- {* shows the names of all unproved assertions,

    50   grouped by program paths, of the verification condition @{text max} *}

    51

    52 boogie_status (full paths) max -- {* shows the state of all assertions

    53   of the verification condition @{text max}, grouped by program paths,

    54   with already proved or irrelevant assertions written in parentheses *}

    55

    56

    57 text {* Let's find out which assertions of @{text max} are hard to prove: *}

    58

    59 boogie_status (narrow step_timeout: 4 final_timeout: 15) max

    60   (simp add: labels, (fast | metis)?)

    61   -- {* The argument @{text step_timeout} is optional, restricting the runtime

    62         of each intermediate narrowing step by the given number of seconds. *}

    63   -- {* The argument @{text final_timeout} is optional, restricting the

    64         runtime of the final narrowing steps by the given number of seconds. *}

    65   -- {* The last argument should be a method to be applied at each narrowing

    66         step. Note that different methods may be composed to one method by

    67         a language similar to regular expressions. *}

    68

    69 boogie_status (scan timeout: 4) max

    70   (simp add: labels, (fast | metis)?)

    71   -- {* finds the first hard assertion wrt. to the given method *}

    72

    73

    74 text {* Now, let's prove the three hard assertions of @{text max}: *}

    75

    76 boogie_vc max (examine: L_14_5c L_14_5b L_14_5a)

    77 proof boogie_cases

    78   case L_14_5c

    79   thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)

    80 next

    81   case L_14_5b

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

    83 next

    84   case L_14_5a

    85   note max0 = max0 = array 0

    86   {

    87     fix i :: int

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

    89     hence "i = 0" by simp

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

    91   }

    92   thus ?case by simp

    93 qed

    94

    95

    96 boogie_status max -- {* the above proved assertions are not shown anymore *}

    97

    98 boogie_status (full) max -- {* states the above proved assertions as proved

    99   and all other assertions as not proved *}

   100

   101 boogie_status (paths) max

   102

   103 boogie_status (full paths) max

   104

   105

   106 text {* Now we prove the remaining assertions all at once: *}

   107

   108 boogie_vc max by (auto simp add: labels)

   109

   110

   111 boogie_status -- {* @{text max} has been completely proved *}

   112

   113 boogie_end

   114

   115 end