src/HOL/Boogie/Examples/VCC_Max.thy
author blanchet
Tue, 27 Mar 2012 16:59:13 +0300
changeset 47152 446cfc760ccf
parent 41601 fda8511006f9
child 48069 e9b2782c4f99
permissions -rw-r--r--
renamed "smt_fixed" to "smt_read_only_certificates"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Boogie/Examples/VCC_Max.thy
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     3
*)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     4
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     5
header {* Boogie example from VCC: get the greatest element of a list *}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     6
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     7
theory VCC_Max
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
     8
imports Boogie
40540
293f9f211be0 formal dependency on b2i files
boehmes
parents: 40514
diff changeset
     9
uses ("VCC_Max.b2i")
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    10
begin
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    11
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    12
text {*
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    13
We prove correct the verification condition generated from the following
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    14
C code:
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    15
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    16
\begin{verbatim}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    17
#include "vcc.h"
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    18
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    19
typedef unsigned char byte;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    20
typedef unsigned long ulong;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    21
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    22
static byte maximum(byte arr[], ulong len)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    23
  requires(wrapped(as_array(arr, len)))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    24
  requires (0 < len && len < (1UI64 << 40))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    25
  ensures (forall(ulong i; i<len ==> arr[i] <= result))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    26
  ensures (exists(ulong i; i<len && arr[i] == result))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    27
{
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    28
  byte max = arr[0];
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    29
  ulong p;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    30
  spec(ulong witness = 0;)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    31
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    32
  for (p = 1; p < len; p++)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    33
    invariant(p <= len)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    34
    invariant(forall(ulong i; i < p ==> arr[i] <= max))
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    35
    invariant(witness < len && arr[witness] == max)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    36
  {
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    37
    if (arr[p] > max) 
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    38
    {
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    39
      max = arr[p];
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    40
      speconly(witness = p;)
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    41
    }
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    42
  }
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    43
  return max;
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    44
}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    45
\end{verbatim}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    46
*}
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    47
40580
0592d3a39c08 require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents: 40540
diff changeset
    48
boogie_open (quiet) "VCC_Max.b2i"
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    49
47152
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 41601
diff changeset
    50
declare [[smt_certificates = "VCC_Max.certs"]]
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 41601
diff changeset
    51
declare [[smt_read_only_certificates = true]]
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 41601
diff changeset
    52
declare [[smt_oracle = false]]
34993
bf3b8462732b updated examples due to changes in the way SMT certificates are stored
boehmes
parents: 34068
diff changeset
    53
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    54
boogie_status
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    55
33445
f0c78a28e18e shorter names for variables and verification conditions,
boehmes
parents: 33419
diff changeset
    56
boogie_vc maximum
34068
a78307d72e58 make assertion labels unique already when loading a verification condition,
boehmes
parents: 33445
diff changeset
    57
  by boogie
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    58
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    59
boogie_end
8ae45e87b992 added HOL-Boogie
boehmes
parents:
diff changeset
    60
35153
5e8935678ee4 include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents: 34993
diff changeset
    61
end