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--
Add lessThan_Suc_eq_insert_0
     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