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