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
boehmes@34068
     1
(*  Title:      HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
boehmes@34068
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@34068
     3
*)
boehmes@34068
     4
boehmes@34068
     5
header {* Boogie example: get the greatest element of a list *}
boehmes@34068
     6
boehmes@34068
     7
theory Boogie_Max_Stepwise
boehmes@34068
     8
imports Boogie
boehmes@34068
     9
begin
boehmes@34068
    10
boehmes@34068
    11
text {*
boehmes@34068
    12
We prove correct the verification condition generated from the following
boehmes@34068
    13
Boogie code:
boehmes@34068
    14
boehmes@34068
    15
\begin{verbatim}
boehmes@34068
    16
procedure max(array : [int]int, length : int)
boehmes@34068
    17
  returns (max : int);
boehmes@34068
    18
  requires (0 < length);
boehmes@34068
    19
  ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max);
boehmes@34068
    20
  ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max);
boehmes@34068
    21
boehmes@34068
    22
implementation max(array : [int]int, length : int) returns (max : int)
boehmes@34068
    23
{
boehmes@34068
    24
  var p : int, k : int;
boehmes@34068
    25
  max := array[0];
boehmes@34068
    26
  k := 0;
boehmes@34068
    27
  p := 1;
boehmes@34068
    28
  while (p < length)
boehmes@34068
    29
    invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max);
boehmes@34068
    30
    invariant (array[k] == max);
boehmes@34068
    31
  {
boehmes@34068
    32
    if (array[p] > max) { max := array[p]; k := p; }
boehmes@34068
    33
    p := p + 1;
boehmes@34068
    34
  }
boehmes@34068
    35
}
boehmes@34068
    36
\end{verbatim}
boehmes@34068
    37
*}
boehmes@34068
    38
boehmes@34068
    39
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
boehmes@34068
    40
boehmes@34068
    41
boogie_status -- {* gives an overview of all verification conditions *}
boehmes@34068
    42
boehmes@34068
    43
boogie_status max -- {* shows the names of all unproved assertions
boehmes@34068
    44
  of the verification condition @{text max} *}
boehmes@34068
    45
boehmes@34068
    46
boogie_status (full) max -- {* shows the state of all assertions
boehmes@34068
    47
  of the verification condition @{text max} *}
boehmes@34068
    48
boehmes@34182
    49
boogie_status (paths) max -- {* shows the names of all unproved assertions,
boehmes@34182
    50
  grouped by program paths, of the verification condition @{text max} *}
boehmes@34182
    51
boehmes@34182
    52
boogie_status (full paths) max -- {* shows the state of all assertions
boehmes@34182
    53
  of the verification condition @{text max}, grouped by program paths,
boehmes@34182
    54
  with already proved or irrelevant assertions written in parentheses *}
boehmes@34182
    55
boehmes@34068
    56
boehmes@34068
    57
text {* Let's find out which assertions of @{text max} are hard to prove: *}
boehmes@34068
    58
boehmes@35323
    59
boogie_status (narrow step_timeout: 4 final_timeout: 15) max
boehmes@34182
    60
  (simp add: labels, (fast | metis)?)
boehmes@35323
    61
  -- {* The argument @{text step_timeout} is optional, restricting the runtime
boehmes@35323
    62
        of each intermediate narrowing step by the given number of seconds. *}
boehmes@35323
    63
  -- {* The argument @{text final_timeout} is optional, restricting the
boehmes@35323
    64
        runtime of the final narrowing steps by the given number of seconds. *}
boehmes@34182
    65
  -- {* The last argument should be a method to be applied at each narrowing
boehmes@34068
    66
        step. Note that different methods may be composed to one method by
boehmes@34068
    67
        a language similar to regular expressions. *}
boehmes@34068
    68
boehmes@34182
    69
boogie_status (scan timeout: 4) max
boehmes@34182
    70
  (simp add: labels, (fast | metis)?)
boehmes@34182
    71
  -- {* finds the first hard assertion wrt. to the given method *}
boehmes@34182
    72
boehmes@34068
    73
boehmes@34068
    74
text {* Now, let's prove the three hard assertions of @{text max}: *}
boehmes@34068
    75
boehmes@34182
    76
boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) 
boehmes@34068
    77
proof boogie_cases
boehmes@34068
    78
  case L_14_5c
boehmes@34068
    79
  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
boehmes@34068
    80
next
boehmes@34068
    81
  case L_14_5b
boehmes@34068
    82
  thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)
boehmes@34068
    83
next
boehmes@34068
    84
  case L_14_5a
boehmes@34068
    85
  note max0 = `max0 = array 0`
boehmes@34068
    86
  {
boehmes@34068
    87
    fix i :: int
boehmes@34068
    88
    assume "0 \<le> i \<and> i < 1"
boehmes@34068
    89
    hence "i = 0" by simp
boehmes@34068
    90
    with max0 have "array i \<le> max0" by simp
boehmes@34068
    91
  }
boehmes@34068
    92
  thus ?case by simp
boehmes@34068
    93
qed
boehmes@34068
    94
boehmes@34068
    95
boehmes@34068
    96
boogie_status max -- {* the above proved assertions are not shown anymore *}
boehmes@34068
    97
boehmes@34068
    98
boogie_status (full) max -- {* states the above proved assertions as proved
boehmes@34068
    99
  and all other assertions as not proved *}
boehmes@34068
   100
boehmes@34182
   101
boogie_status (paths) max
boehmes@34182
   102
boehmes@34182
   103
boogie_status (full paths) max
boehmes@34182
   104
boehmes@34068
   105
boehmes@34068
   106
text {* Now we prove the remaining assertions all at once: *}
boehmes@34068
   107
boehmes@34068
   108
boogie_vc max by (auto simp add: labels)
boehmes@34068
   109
boehmes@34068
   110
boehmes@34068
   111
boogie_status -- {* @{text max} has been completely proved *}
boehmes@34068
   112
boehmes@34068
   113
boogie_end
boehmes@34068
   114
boehmes@34068
   115
end