author | boehmes |
Tue, 26 Oct 2010 11:46:19 +0200 | |
changeset 40163 | a462d5207aa6 |
parent 36081 | 70deefb6c093 |
child 40513 | 1204d268464f |
permissions | -rw-r--r-- |
33419 | 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 |
||
34993
bf3b8462732b
updated examples due to changes in the way SMT certificates are stored
boehmes
parents:
34068
diff
changeset
|
49 |
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]] |
36081
70deefb6c093
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
boehmes
parents:
35153
diff
changeset
|
50 |
declare [[smt_fixed=true]] |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
36081
diff
changeset
|
51 |
declare [[smt_oracle=false]] |
34993
bf3b8462732b
updated examples due to changes in the way SMT certificates are stored
boehmes
parents:
34068
diff
changeset
|
52 |
|
33419 | 53 |
boogie_status |
54 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33419
diff
changeset
|
55 |
boogie_vc maximum |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33445
diff
changeset
|
56 |
by boogie |
33419 | 57 |
|
58 |
boogie_end |
|
59 |
||
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
|
60 |
end |