author | boehmes |
Mon, 15 Nov 2010 00:20:36 +0100 | |
changeset 40540 | 293f9f211be0 |
parent 40514 | db5f14910dce |
child 40580 | 0592d3a39c08 |
permissions | -rw-r--r-- |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Boogie/Examples/Boogie_Max_Stepwise.thy |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
3 |
*) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
4 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
5 |
header {* Boogie example: get the greatest element of a list *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
6 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
7 |
theory Boogie_Max_Stepwise |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
8 |
imports Boogie |
40540 | 9 |
uses ("Boogie_Max.b2i") |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
10 |
begin |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
11 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
12 |
text {* |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
13 |
We prove correct the verification condition generated from the following |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
14 |
Boogie code: |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
15 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
16 |
\begin{verbatim} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
17 |
procedure max(array : [int]int, length : int) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
18 |
returns (max : int); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
19 |
requires (0 < length); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
20 |
ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
21 |
ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
22 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
23 |
implementation max(array : [int]int, length : int) returns (max : int) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
24 |
{ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
25 |
var p : int, k : int; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
26 |
max := array[0]; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
27 |
k := 0; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
28 |
p := 1; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
29 |
while (p < length) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
30 |
invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
31 |
invariant (array[k] == max); |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
32 |
{ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
33 |
if (array[p] > max) { max := array[p]; k := p; } |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
34 |
p := p + 1; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
35 |
} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
36 |
} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
37 |
\end{verbatim} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
38 |
*} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
39 |
|
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
35323
diff
changeset
|
40 |
boogie_open "Boogie_Max" |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
41 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
42 |
boogie_status -- {* gives an overview of all verification conditions *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
43 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
44 |
boogie_status max -- {* shows the names of all unproved assertions |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
45 |
of the verification condition @{text max} *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
46 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
47 |
boogie_status (full) max -- {* shows the state of all assertions |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
48 |
of the verification condition @{text max} *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
49 |
|
34182 | 50 |
boogie_status (paths) max -- {* shows the names of all unproved assertions, |
51 |
grouped by program paths, of the verification condition @{text max} *} |
|
52 |
||
53 |
boogie_status (full paths) max -- {* shows the state of all assertions |
|
54 |
of the verification condition @{text max}, grouped by program paths, |
|
55 |
with already proved or irrelevant assertions written in parentheses *} |
|
56 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
57 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
58 |
text {* Let's find out which assertions of @{text max} are hard to prove: *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
59 |
|
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
34182
diff
changeset
|
60 |
boogie_status (narrow step_timeout: 4 final_timeout: 15) max |
34182 | 61 |
(simp add: labels, (fast | metis)?) |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
34182
diff
changeset
|
62 |
-- {* The argument @{text step_timeout} is optional, restricting the runtime |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
34182
diff
changeset
|
63 |
of each intermediate narrowing step by the given number of seconds. *} |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
34182
diff
changeset
|
64 |
-- {* The argument @{text final_timeout} is optional, restricting the |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
34182
diff
changeset
|
65 |
runtime of the final narrowing steps by the given number of seconds. *} |
34182 | 66 |
-- {* The last argument should be a method to be applied at each narrowing |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
67 |
step. Note that different methods may be composed to one method by |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
68 |
a language similar to regular expressions. *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
69 |
|
34182 | 70 |
boogie_status (scan timeout: 4) max |
71 |
(simp add: labels, (fast | metis)?) |
|
72 |
-- {* finds the first hard assertion wrt. to the given method *} |
|
73 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
74 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
75 |
text {* Now, let's prove the three hard assertions of @{text max}: *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
76 |
|
34182 | 77 |
boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
78 |
proof boogie_cases |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
79 |
case L_14_5c |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
80 |
thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
81 |
next |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
82 |
case L_14_5b |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
83 |
thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
84 |
next |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
85 |
case L_14_5a |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
86 |
note max0 = `max0 = array 0` |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
87 |
{ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
88 |
fix i :: int |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
89 |
assume "0 \<le> i \<and> i < 1" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
90 |
hence "i = 0" by simp |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
91 |
with max0 have "array i \<le> max0" by simp |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
92 |
} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
93 |
thus ?case by simp |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
94 |
qed |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
95 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
96 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
97 |
boogie_status max -- {* the above proved assertions are not shown anymore *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
98 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
99 |
boogie_status (full) max -- {* states the above proved assertions as proved |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
100 |
and all other assertions as not proved *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
101 |
|
34182 | 102 |
boogie_status (paths) max |
103 |
||
104 |
boogie_status (full paths) max |
|
105 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
106 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
107 |
text {* Now we prove the remaining assertions all at once: *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
108 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
109 |
boogie_vc max by (auto simp add: labels) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
110 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
111 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
112 |
boogie_status -- {* @{text max} has been completely proved *} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
113 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
114 |
boogie_end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
115 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
116 |
end |