author | boehmes |
Thu, 05 Nov 2009 14:48:40 +0100 | |
changeset 33445 | f0c78a28e18e |
parent 33419 | 8ae45e87b992 |
child 34068 | a78307d72e58 |
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 |
||
49 |
boogie_status |
|
50 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33419
diff
changeset
|
51 |
boogie_vc maximum |
33419 | 52 |
unfolding labels |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33419
diff
changeset
|
53 |
using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/VCC_maximum"]] |
33419 | 54 |
using [[z3_proofs=true]] |
55 |
by (smt boogie) |
|
56 |
||
57 |
boogie_end |
|
58 |
||
59 |
end |