author | wenzelm |
Tue, 22 Apr 2014 12:03:58 +0200 | |
changeset 56629 | ca302c495bca |
parent 54447 | 019394de2b41 |
child 56818 | 689a3eeb6f9e |
permissions | -rw-r--r-- |
52722 | 1 |
(* Title: HOL/SMT_Examples/Boogie.thy |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Proving Boogie-generated verification conditions *} |
|
6 |
||
7 |
theory Boogie |
|
8 |
imports Main |
|
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
9 |
keywords "boogie_file" :: thy_load ("b2i") |
52722 | 10 |
begin |
11 |
||
12 |
text {* |
|
13 |
HOL-Boogie and its applications are described in: |
|
14 |
\begin{itemize} |
|
15 |
||
16 |
\item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff. |
|
17 |
HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier. |
|
18 |
Theorem Proving in Higher Order Logics, 2008. |
|
19 |
||
20 |
\item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff. |
|
21 |
HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler. |
|
22 |
Journal of Automated Reasoning, 2009. |
|
23 |
||
24 |
\end{itemize} |
|
25 |
*} |
|
26 |
||
27 |
||
28 |
||
29 |
section {* Built-in types and functions of Boogie *} |
|
30 |
||
31 |
subsection {* Integer arithmetics *} |
|
32 |
||
33 |
text {* |
|
34 |
The operations @{text div} and @{text mod} are built-in in Boogie, but |
|
35 |
without a particular semantics due to different interpretations in |
|
36 |
programming languages. We assume that each application comes with a |
|
37 |
proper axiomatization. |
|
38 |
*} |
|
39 |
||
40 |
axiomatization |
|
41 |
boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and |
|
42 |
boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70) |
|
43 |
||
44 |
||
45 |
||
46 |
section {* Setup *} |
|
47 |
||
48 |
ML_file "boogie.ML" |
|
49 |
||
50 |
||
51 |
||
52 |
section {* Verification condition proofs *} |
|
53 |
||
54 |
declare [[smt_oracle = false]] |
|
55 |
declare [[smt_read_only_certificates = true]] |
|
56 |
||
57 |
||
58 |
declare [[smt_certificates = "Boogie_Max.certs"]] |
|
59 |
||
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
60 |
boogie_file Boogie_Max |
52722 | 61 |
|
62 |
||
63 |
declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
|
64 |
||
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
65 |
boogie_file Boogie_Dijkstra |
52722 | 66 |
|
67 |
||
68 |
declare [[z3_with_extensions = true]] |
|
69 |
declare [[smt_certificates = "VCC_Max.certs"]] |
|
70 |
||
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
71 |
boogie_file VCC_Max |
52722 | 72 |
|
73 |
end |