src/HOL/Boogie/Examples/Boogie_Max.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 36081 70deefb6c093
child 40163 a462d5207aa6
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
boehmes@34068
     1
(*  Title:      HOL/Boogie/Examples/Boogie_Max.thy
boehmes@33419
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@33419
     3
*)
boehmes@33419
     4
boehmes@33419
     5
header {* Boogie example: get the greatest element of a list *}
boehmes@33419
     6
boehmes@33419
     7
theory Boogie_Max
boehmes@33419
     8
imports Boogie
boehmes@33419
     9
begin
boehmes@33419
    10
boehmes@33419
    11
text {*
boehmes@33419
    12
We prove correct the verification condition generated from the following
boehmes@33419
    13
Boogie code:
boehmes@33419
    14
boehmes@33419
    15
\begin{verbatim}
boehmes@33419
    16
procedure max(array : [int]int, length : int)
boehmes@33419
    17
  returns (max : int);
boehmes@33419
    18
  requires (0 < length);
boehmes@33419
    19
  ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max);
boehmes@33419
    20
  ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max);
boehmes@33419
    21
boehmes@33419
    22
implementation max(array : [int]int, length : int) returns (max : int)
boehmes@33419
    23
{
boehmes@33419
    24
  var p : int, k : int;
boehmes@33419
    25
  max := array[0];
boehmes@33419
    26
  k := 0;
boehmes@33419
    27
  p := 1;
boehmes@33419
    28
  while (p < length)
boehmes@33419
    29
    invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max);
boehmes@33419
    30
    invariant (array[k] == max);
boehmes@33419
    31
  {
boehmes@33419
    32
    if (array[p] > max) { max := array[p]; k := p; }
boehmes@33419
    33
    p := p + 1;
boehmes@33419
    34
  }
boehmes@33419
    35
}
boehmes@33419
    36
\end{verbatim}
boehmes@33419
    37
*}
boehmes@33419
    38
boehmes@33419
    39
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
boehmes@33419
    40
boehmes@34993
    41
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
boehmes@36081
    42
declare [[smt_fixed=true]]
boehmes@34993
    43
boehmes@33445
    44
boogie_vc max
boehmes@33419
    45
  using [[z3_proofs=true]]
boehmes@34068
    46
  by boogie
boehmes@33424
    47
boehmes@33419
    48
boogie_end
boehmes@33419
    49
boehmes@33419
    50
end