author | wenzelm |
Mon, 02 Oct 2017 19:38:39 +0200 | |
changeset 66758 | 9312ce5a938d |
parent 66741 | c90fb8bee1dd |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
52722 | 1 |
(* Title: HOL/SMT_Examples/Boogie.thy |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
*) |
|
4 |
||
63167 | 5 |
section \<open>Proving Boogie-generated verification conditions\<close> |
52722 | 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 |
||
63167 | 12 |
text \<open> |
52722 | 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} |
|
63167 | 25 |
\<close> |
52722 | 26 |
|
27 |
||
28 |
||
63167 | 29 |
section \<open>Built-in types and functions of Boogie\<close> |
52722 | 30 |
|
63167 | 31 |
subsection \<open>Integer arithmetics\<close> |
52722 | 32 |
|
63167 | 33 |
text \<open> |
34 |
The operations \<open>div\<close> and \<open>mod\<close> are built-in in Boogie, but |
|
52722 | 35 |
without a particular semantics due to different interpretations in |
36 |
programming languages. We assume that each application comes with a |
|
37 |
proper axiomatization. |
|
63167 | 38 |
\<close> |
52722 | 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 |
||
63167 | 46 |
section \<open>Setup\<close> |
52722 | 47 |
|
48 |
ML_file "boogie.ML" |
|
49 |
||
50 |
||
51 |
||
63167 | 52 |
section \<open>Verification condition proofs\<close> |
52722 | 53 |
|
58061 | 54 |
declare [[smt_oracle = false]] |
66741 | 55 |
declare [[smt_read_only_certificates = true]] |
52722 | 56 |
|
57 |
||
66758 | 58 |
external_file "Boogie_Max.certs" |
58367
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58061
diff
changeset
|
59 |
declare [[smt_certificates = "Boogie_Max.certs"]] |
52722 | 60 |
|
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
61 |
boogie_file Boogie_Max |
52722 | 62 |
|
63 |
||
66758 | 64 |
external_file "Boogie_Dijkstra.certs" |
58367
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58061
diff
changeset
|
65 |
declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
52722 | 66 |
|
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
67 |
boogie_file Boogie_Dijkstra |
52722 | 68 |
|
69 |
||
58061 | 70 |
declare [[z3_extensions = true]] |
66758 | 71 |
external_file "VCC_Max.certs" |
58367
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58061
diff
changeset
|
72 |
declare [[smt_certificates = "VCC_Max.certs"]] |
52722 | 73 |
|
54447
019394de2b41
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents:
52722
diff
changeset
|
74 |
boogie_file VCC_Max |
52722 | 75 |
|
76 |
end |