author | Walther Neuper <walther.neuper@jku.at> |
Mon, 15 Mar 2021 10:04:17 +0100 | |
changeset 60174 | 21d482c9ab68 |
parent 60166 | 7d6f46b7fc10 |
child 60199 | f2a13c9ed039 |
permissions | -rw-r--r-- |
boehmes@53859 | 1 |
(* Title: HOL/SMT_Examples/Boogie.thy |
boehmes@53859 | 2 |
Author: Sascha Boehme, TU Muenchen |
boehmes@53859 | 3 |
*) |
boehmes@53859 | 4 |
|
wneuper@59324 | 5 |
section \<open>Proving Boogie-generated verification conditions\<close> |
boehmes@53859 | 6 |
|
boehmes@53859 | 7 |
theory Boogie |
boehmes@53859 | 8 |
imports Main |
walther@60174 | 9 |
(*WAS "boogie_file" :: thy_load ("b2i") *) |
walther@60166 | 10 |
keywords "boogie_file" :: thy_load |
boehmes@53859 | 11 |
begin |
boehmes@53859 | 12 |
|
wneuper@59324 | 13 |
text \<open> |
boehmes@53859 | 14 |
HOL-Boogie and its applications are described in: |
boehmes@53859 | 15 |
\begin{itemize} |
boehmes@53859 | 16 |
|
boehmes@53859 | 17 |
\item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff. |
boehmes@53859 | 18 |
HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier. |
boehmes@53859 | 19 |
Theorem Proving in Higher Order Logics, 2008. |
boehmes@53859 | 20 |
|
boehmes@53859 | 21 |
\item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff. |
boehmes@53859 | 22 |
HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler. |
boehmes@53859 | 23 |
Journal of Automated Reasoning, 2009. |
boehmes@53859 | 24 |
|
boehmes@53859 | 25 |
\end{itemize} |
wneuper@59324 | 26 |
\<close> |
boehmes@53859 | 27 |
|
boehmes@53859 | 28 |
|
boehmes@53859 | 29 |
|
wneuper@59324 | 30 |
section \<open>Built-in types and functions of Boogie\<close> |
boehmes@53859 | 31 |
|
wneuper@59324 | 32 |
subsection \<open>Integer arithmetics\<close> |
boehmes@53859 | 33 |
|
wneuper@59324 | 34 |
text \<open> |
wneuper@59324 | 35 |
The operations \<open>div\<close> and \<open>mod\<close> are built-in in Boogie, but |
boehmes@53859 | 36 |
without a particular semantics due to different interpretations in |
boehmes@53859 | 37 |
programming languages. We assume that each application comes with a |
boehmes@53859 | 38 |
proper axiomatization. |
wneuper@59324 | 39 |
\<close> |
boehmes@53859 | 40 |
|
boehmes@53859 | 41 |
axiomatization |
boehmes@53859 | 42 |
boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and |
boehmes@53859 | 43 |
boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70) |
boehmes@53859 | 44 |
|
boehmes@53859 | 45 |
|
boehmes@53859 | 46 |
|
wneuper@59324 | 47 |
section \<open>Setup\<close> |
boehmes@53859 | 48 |
|
walther@59606 | 49 |
ML_file \<open>boogie.ML\<close> |
boehmes@53859 | 50 |
|
boehmes@53859 | 51 |
|
boehmes@53859 | 52 |
|
wneuper@59324 | 53 |
section \<open>Verification condition proofs\<close> |
boehmes@53859 | 54 |
|
wneuper@59180 | 55 |
declare [[smt_oracle = false]] |
wneuper@59180 | 56 |
declare [[smt_read_only_certificates = true]] |
boehmes@53859 | 57 |
|
boehmes@53859 | 58 |
|
walther@59606 | 59 |
external_file \<open>Boogie_Max.certs\<close> |
wneuper@59180 | 60 |
declare [[smt_certificates = "Boogie_Max.certs"]] |
boehmes@53859 | 61 |
|
walther@60174 | 62 |
(*WAS \<open>Boogie_Max\<close> *) |
walther@60166 | 63 |
boogie_file \<open>Boogie_Max.b2i\<close> |
boehmes@53859 | 64 |
|
boehmes@53859 | 65 |
|
walther@59606 | 66 |
external_file \<open>Boogie_Dijkstra.certs\<close> |
wneuper@59180 | 67 |
declare [[smt_certificates = "Boogie_Dijkstra.certs"]] |
boehmes@53859 | 68 |
|
walther@60174 | 69 |
(*WAS \<open>Boogie_Dijkstra\<close> *) |
walther@60166 | 70 |
boogie_file \<open>Boogie_Dijkstra.b2i\<close> |
boehmes@53859 | 71 |
|
boehmes@53859 | 72 |
|
wneuper@59180 | 73 |
declare [[z3_extensions = true]] |
walther@59606 | 74 |
external_file \<open>VCC_Max.certs\<close> |
wneuper@59180 | 75 |
declare [[smt_certificates = "VCC_Max.certs"]] |
boehmes@53859 | 76 |
|
walther@60174 | 77 |
(*WAS \<open>VCC_Max\<close> *) |
walther@60166 | 78 |
boogie_file \<open>VCC_Max.b2i\<close> |
boehmes@53859 | 79 |
|
boehmes@53859 | 80 |
end |