author | boehmes |
Fri, 12 Nov 2010 15:56:08 +0100 | |
changeset 40514 | db5f14910dce |
parent 40513 | 1204d268464f |
child 40540 | 293f9f211be0 |
permissions | -rw-r--r-- |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33663
diff
changeset
|
1 |
(* Title: HOL/Boogie/Examples/Boogie_Max.thy |
33419 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Boogie example: get the greatest element of a list *} |
|
6 |
||
7 |
theory Boogie_Max |
|
8 |
imports Boogie |
|
9 |
begin |
|
10 |
||
11 |
text {* |
|
12 |
We prove correct the verification condition generated from the following |
|
13 |
Boogie code: |
|
14 |
||
15 |
\begin{verbatim} |
|
16 |
procedure max(array : [int]int, length : int) |
|
17 |
returns (max : int); |
|
18 |
requires (0 < length); |
|
19 |
ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max); |
|
20 |
ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max); |
|
21 |
||
22 |
implementation max(array : [int]int, length : int) returns (max : int) |
|
23 |
{ |
|
24 |
var p : int, k : int; |
|
25 |
max := array[0]; |
|
26 |
k := 0; |
|
27 |
p := 1; |
|
28 |
while (p < length) |
|
29 |
invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max); |
|
30 |
invariant (array[k] == max); |
|
31 |
{ |
|
32 |
if (array[p] > max) { max := array[p]; k := p; } |
|
33 |
p := p + 1; |
|
34 |
} |
|
35 |
} |
|
36 |
\end{verbatim} |
|
37 |
*} |
|
38 |
||
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
40513
diff
changeset
|
39 |
boogie_open "Boogie_Max" |
33419 | 40 |
|
40513 | 41 |
declare [[smt_certificates="Boogie_Max.certs"]] |
36081
70deefb6c093
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
boehmes
parents:
34993
diff
changeset
|
42 |
declare [[smt_fixed=true]] |
40163
a462d5207aa6
changed SMT configuration options; updated SMT certificates
boehmes
parents:
36081
diff
changeset
|
43 |
declare [[smt_oracle=false]] |
34993
bf3b8462732b
updated examples due to changes in the way SMT certificates are stored
boehmes
parents:
34068
diff
changeset
|
44 |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
45 |
boogie_vc max |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33663
diff
changeset
|
46 |
by boogie |
33424
a3b002e2cd55
proper and unique case names for the split_vc method,
boehmes
parents:
33419
diff
changeset
|
47 |
|
33419 | 48 |
boogie_end |
49 |
||
50 |
end |