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
     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 = false]] (* FIXME *)

    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