(*  Title:      HOL/Boogie/Boogie.thy

    Author:     Sascha Boehme, TU Muenchen

*)

header {* Integration of the Boogie program verifier *}

theory Boogie

imports Word

uses

  ("Tools/boogie_vcs.ML")

  ("Tools/boogie_loader.ML")

  ("Tools/boogie_tactics.ML")

  ("Tools/boogie_commands.ML")

begin

text {*

HOL-Boogie and its applications are described in:

\begin{itemize}

\item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff.

HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier.

Theorem Proving in Higher Order Logics, 2008.

\item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff.

HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler.

Journal of Automated Reasoning, 2009.

\end{itemize}

*}

section {* Built-in types and functions of Boogie *}

subsection {* Labels *}

text {*

See "Generating error traces from verification-condition counterexamples"

by Leino e.a. (2004) for a description of Boogie's labelling mechanism and

semantics.

*}

definition assert_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "assert_at l P = P"

definition block_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "block_at l P = P"

lemmas labels = assert_at_def block_at_def

subsection {* Integer arithmetics *}

text {*

The operations @{text div} and @{text mod} are built-in in Boogie, but

without a particular semantics due to different interpretations in

programming languages. We assume that each application comes with a

proper axiomatization.

*}

axiomatization

  boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and

  boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70)

section {* Boogie environment *}

text {*

Proving Boogie-generated verification conditions happens inside

a Boogie environment:

  boogie_open "b2i file without extension"

  boogie_vc "verification condition 1" ...

  boogie_vc "verification condition 2" ...

  boogie_vc "verification condition 3" ...

  boogie_end

See the Boogie examples for more details.

At most one Boogie environment should occur per theory,

otherwise unexpected effects may arise.

*}

section {* Setup *}

ML {*

structure Boogie_Axioms = Named_Thms

(

  val name = "boogie"

  val description =

    "Boogie background axioms loaded along with Boogie verification conditions"

)

*}

setup Boogie_Axioms.setup

use "Tools/boogie_vcs.ML"

use "Tools/boogie_loader.ML"

use "Tools/boogie_tactics.ML"

setup Boogie_Tactics.setup

use "Tools/boogie_commands.ML"

setup Boogie_Commands.setup

end