src/HOL/SMT_Examples/Boogie.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 58889 5b7a9633cfa8
child 66740 ece9435ca78e
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/SMT_Examples/Boogie.thy
     2     Author:     Sascha Boehme, TU Muenchen
     3 *)
     4 
     5 section \<open>Proving Boogie-generated verification conditions\<close>
     6 
     7 theory Boogie
     8 imports Main
     9 keywords "boogie_file" :: thy_load ("b2i")
    10 begin
    11 
    12 text \<open>
    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}
    25 \<close>
    26 
    27 
    28 
    29 section \<open>Built-in types and functions of Boogie\<close>
    30 
    31 subsection \<open>Integer arithmetics\<close>
    32 
    33 text \<open>
    34 The operations \<open>div\<close> and \<open>mod\<close> are built-in in Boogie, but
    35 without a particular semantics due to different interpretations in
    36 programming languages. We assume that each application comes with a
    37 proper axiomatization.
    38 \<close>
    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 
    46 section \<open>Setup\<close>
    47 
    48 ML_file "boogie.ML"
    49 
    50 
    51 
    52 section \<open>Verification condition proofs\<close>
    53 
    54 declare [[smt_oracle = false]]
    55 declare [[smt_read_only_certificates = true]]
    56 
    57 
    58 declare [[smt_certificates = "Boogie_Max.certs"]]
    59 
    60 boogie_file Boogie_Max
    61 
    62 
    63 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    64 
    65 boogie_file Boogie_Dijkstra
    66 
    67 
    68 declare [[z3_extensions = true]]
    69 declare [[smt_certificates = "VCC_Max.certs"]]
    70 
    71 boogie_file VCC_Max
    72 
    73 end