src/HOL/SMT_Examples/Boogie.thy
author blanchet
Sun Oct 01 15:17:43 2017 +0200 (21 months ago)
changeset 66740 ece9435ca78e
parent 63167 0909deb8059b
child 66741 c90fb8bee1dd
permissions -rw-r--r--
updated SMT certificates and added one test
boehmes@52722
     1
(*  Title:      HOL/SMT_Examples/Boogie.thy
boehmes@52722
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@52722
     3
*)
boehmes@52722
     4
wenzelm@63167
     5
section \<open>Proving Boogie-generated verification conditions\<close>
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
wenzelm@63167
    12
text \<open>
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}
wenzelm@63167
    25
\<close>
boehmes@52722
    26
boehmes@52722
    27
boehmes@52722
    28
wenzelm@63167
    29
section \<open>Built-in types and functions of Boogie\<close>
boehmes@52722
    30
wenzelm@63167
    31
subsection \<open>Integer arithmetics\<close>
boehmes@52722
    32
wenzelm@63167
    33
text \<open>
wenzelm@63167
    34
The operations \<open>div\<close> and \<open>mod\<close> 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.
wenzelm@63167
    38
\<close>
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
wenzelm@63167
    46
section \<open>Setup\<close>
boehmes@52722
    47
boehmes@52722
    48
ML_file "boogie.ML"
boehmes@52722
    49
boehmes@52722
    50
boehmes@52722
    51
wenzelm@63167
    52
section \<open>Verification condition proofs\<close>
boehmes@52722
    53
blanchet@58061
    54
declare [[smt_oracle = false]]
blanchet@66740
    55
declare [[smt_read_only_certificates = false]] (* FIXME *)
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