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