src/HOL/Boogie/Boogie.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 36899 bcd6fce5bf06
child 45294 3c5d3d286055
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:      HOL/Boogie/Boogie.thy
     2     Author:     Sascha Boehme, TU Muenchen
     3 *)
     4 
     5 header {* Integration of the Boogie program verifier *}
     6 
     7 theory Boogie
     8 imports Word
     9 uses
    10   ("Tools/boogie_vcs.ML")
    11   ("Tools/boogie_loader.ML")
    12   ("Tools/boogie_tactics.ML")
    13   ("Tools/boogie_commands.ML")
    14 begin
    15 
    16 text {*
    17 HOL-Boogie and its applications are described in:
    18 \begin{itemize}
    19 
    20 \item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff.
    21 HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier.
    22 Theorem Proving in Higher Order Logics, 2008.
    23 
    24 \item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff.
    25 HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler.
    26 Journal of Automated Reasoning, 2009.
    27 
    28 \end{itemize}
    29 *}
    30 
    31 
    32 
    33 section {* Built-in types and functions of Boogie *}
    34 
    35 subsection {* Labels *}
    36 
    37 text {*
    38 See "Generating error traces from verification-condition counterexamples"
    39 by Leino e.a. (2004) for a description of Boogie's labelling mechanism and
    40 semantics.
    41 *}
    42 
    43 definition assert_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "assert_at l P = P"
    44 definition block_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "block_at l P = P"
    45 
    46 lemmas labels = assert_at_def block_at_def
    47 
    48 
    49 subsection {* Integer arithmetics *}
    50 
    51 text {*
    52 The operations @{text div} and @{text mod} are built-in in Boogie, but
    53 without a particular semantics due to different interpretations in
    54 programming languages. We assume that each application comes with a
    55 proper axiomatization.
    56 *}
    57 
    58 axiomatization
    59   boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and
    60   boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70)
    61 
    62 
    63 
    64 section {* Boogie environment *}
    65 
    66 text {*
    67 Proving Boogie-generated verification conditions happens inside
    68 a Boogie environment:
    69 
    70   boogie_open "b2i file without extension"
    71   boogie_vc "verification condition 1" ...
    72   boogie_vc "verification condition 2" ...
    73   boogie_vc "verification condition 3" ...
    74   boogie_end
    75 
    76 See the Boogie examples for more details.
    77  
    78 At most one Boogie environment should occur per theory,
    79 otherwise unexpected effects may arise.
    80 *}
    81 
    82 
    83 
    84 section {* Setup *}
    85 
    86 ML {*
    87 structure Boogie_Axioms = Named_Thms
    88 (
    89   val name = "boogie"
    90   val description =
    91     "Boogie background axioms loaded along with Boogie verification conditions"
    92 )
    93 *}
    94 setup Boogie_Axioms.setup
    95 
    96 use "Tools/boogie_vcs.ML"
    97 use "Tools/boogie_loader.ML"
    98 use "Tools/boogie_tactics.ML"
    99 setup Boogie_Tactics.setup
   100 
   101 use "Tools/boogie_commands.ML"
   102 setup Boogie_Commands.setup
   103 
   104 end