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