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