|
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 |
|
|
|
51 |
boogie_vc b_maximum
|
|
|
52 |
unfolding labels
|
|
|
53 |
using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/VCC_b_maximum"]]
|
|
|
54 |
using [[z3_proofs=true]]
|
|
|
55 |
by (smt boogie)
|
|
|
56 |
|
|
|
57 |
boogie_end
|
|
|
58 |
|
|
|
59 |
end |