1 (* Title: HOL/Boogie/Boogie.thy |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Integration of the Boogie program verifier *} |
|
6 |
|
7 theory Boogie |
|
8 imports Word |
|
9 keywords |
|
10 "boogie_open" :: thy_load and |
|
11 "boogie_end" :: thy_decl and |
|
12 "boogie_vc" :: thy_goal and |
|
13 "boogie_status" :: diag |
|
14 begin |
|
15 |
|
16 text {* |
|
17 HOL-Boogie and its applications are described in: |
|
18 \begin{itemize} |
|
19 |
|
20 \item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff. |
|
21 HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier. |
|
22 Theorem Proving in Higher Order Logics, 2008. |
|
23 |
|
24 \item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff. |
|
25 HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler. |
|
26 Journal of Automated Reasoning, 2009. |
|
27 |
|
28 \end{itemize} |
|
29 *} |
|
30 |
|
31 |
|
32 |
|
33 section {* Built-in types and functions of Boogie *} |
|
34 |
|
35 subsection {* Labels *} |
|
36 |
|
37 text {* |
|
38 See "Generating error traces from verification-condition counterexamples" |
|
39 by Leino e.a. (2004) for a description of Boogie's labelling mechanism and |
|
40 semantics. |
|
41 *} |
|
42 |
|
43 definition assert_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "assert_at l P = P" |
|
44 definition block_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "block_at l P = P" |
|
45 |
|
46 lemmas labels = assert_at_def block_at_def |
|
47 |
|
48 |
|
49 subsection {* Integer arithmetics *} |
|
50 |
|
51 text {* |
|
52 The operations @{text div} and @{text mod} are built-in in Boogie, but |
|
53 without a particular semantics due to different interpretations in |
|
54 programming languages. We assume that each application comes with a |
|
55 proper axiomatization. |
|
56 *} |
|
57 |
|
58 axiomatization |
|
59 boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and |
|
60 boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70) |
|
61 |
|
62 |
|
63 |
|
64 section {* Boogie environment *} |
|
65 |
|
66 text {* |
|
67 Proving Boogie-generated verification conditions happens inside |
|
68 a Boogie environment: |
|
69 |
|
70 boogie_open "b2i file with extension" |
|
71 boogie_vc "verification condition 1" ... |
|
72 boogie_vc "verification condition 2" ... |
|
73 boogie_vc "verification condition 3" ... |
|
74 boogie_end |
|
75 |
|
76 See the Boogie examples for more details. |
|
77 |
|
78 At most one Boogie environment should occur per theory, |
|
79 otherwise unexpected effects may arise. |
|
80 *} |
|
81 |
|
82 |
|
83 |
|
84 section {* Setup *} |
|
85 |
|
86 ML {* |
|
87 structure Boogie_Axioms = Named_Thms |
|
88 ( |
|
89 val name = @{binding boogie} |
|
90 val description = |
|
91 "Boogie background axioms loaded along with Boogie verification conditions" |
|
92 ) |
|
93 *} |
|
94 setup Boogie_Axioms.setup |
|
95 |
|
96 ML_file "Tools/boogie_vcs.ML" |
|
97 ML_file "Tools/boogie_loader.ML" |
|
98 ML_file "Tools/boogie_tactics.ML" |
|
99 setup Boogie_Tactics.setup |
|
100 |
|
101 ML_file "Tools/boogie_commands.ML" |
|
102 setup Boogie_Commands.setup |
|
103 |
|
104 end |
|