src/HOL/Boogie/Examples/VCC_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@33419
     1
(*  Title:      HOL/Boogie/Examples/VCC_Max.thy
boehmes@33419
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@33419
     3
*)
boehmes@33419
     4
boehmes@33419
     5
header {* Boogie example from VCC: get the greatest element of a list *}
boehmes@33419
     6
boehmes@33419
     7
theory VCC_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
C code:
boehmes@33419
    14
boehmes@33419
    15
\begin{verbatim}
boehmes@33419
    16
#include "vcc.h"
boehmes@33419
    17
boehmes@33419
    18
typedef unsigned char byte;
boehmes@33419
    19
typedef unsigned long ulong;
boehmes@33419
    20
boehmes@33419
    21
static byte maximum(byte arr[], ulong len)
boehmes@33419
    22
  requires(wrapped(as_array(arr, len)))
boehmes@33419
    23
  requires (0 < len && len < (1UI64 << 40))
boehmes@33419
    24
  ensures (forall(ulong i; i<len ==> arr[i] <= result))
boehmes@33419
    25
  ensures (exists(ulong i; i<len && arr[i] == result))
boehmes@33419
    26
{
boehmes@33419
    27
  byte max = arr[0];
boehmes@33419
    28
  ulong p;
boehmes@33419
    29
  spec(ulong witness = 0;)
boehmes@33419
    30
boehmes@33419
    31
  for (p = 1; p < len; p++)
boehmes@33419
    32
    invariant(p <= len)
boehmes@33419
    33
    invariant(forall(ulong i; i < p ==> arr[i] <= max))
boehmes@33419
    34
    invariant(witness < len && arr[witness] == max)
boehmes@33419
    35
  {
boehmes@33419
    36
    if (arr[p] > max) 
boehmes@33419
    37
    {
boehmes@33419
    38
      max = arr[p];
boehmes@33419
    39
      speconly(witness = p;)
boehmes@33419
    40
    }
boehmes@33419
    41
  }
boehmes@33419
    42
  return max;
boehmes@33419
    43
}
boehmes@33419
    44
\end{verbatim}
boehmes@33419
    45
*}
boehmes@33419
    46
boehmes@33419
    47
boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
boehmes@33419
    48
boehmes@34993
    49
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
boehmes@36081
    50
declare [[smt_fixed=true]]
boehmes@34993
    51
boehmes@33419
    52
boogie_status
boehmes@33419
    53
boehmes@33445
    54
boogie_vc maximum
boehmes@34068
    55
  using [[z3_proofs=true]]
boehmes@34068
    56
  by boogie
boehmes@33419
    57
boehmes@33419
    58
boogie_end
boehmes@33419
    59
boehmes@35153
    60
end