src/HOL/SMT_Examples/Boogie.thy
author wenzelm
Sat, 16 Nov 2013 16:57:09 +0100
changeset 54447 019394de2b41
parent 52722 2c81f7baf8c4
child 56818 689a3eeb6f9e
permissions -rw-r--r--
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/SMT_Examples/Boogie.thy
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     3
*)
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     4
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     5
header {* Proving Boogie-generated verification conditions *}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     6
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     7
theory Boogie
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
     8
imports Main
54447
019394de2b41 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents: 52722
diff changeset
     9
keywords "boogie_file" :: thy_load ("b2i")
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    10
begin
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    11
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    12
text {*
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    13
HOL-Boogie and its applications are described in:
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    14
\begin{itemize}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    15
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    16
\item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    17
HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    18
Theorem Proving in Higher Order Logics, 2008.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    19
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    20
\item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    21
HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    22
Journal of Automated Reasoning, 2009.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    23
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    24
\end{itemize}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    25
*}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    26
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    27
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    28
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    29
section {* Built-in types and functions of Boogie *}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    30
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    31
subsection {* Integer arithmetics *}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    32
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    33
text {*
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    34
The operations @{text div} and @{text mod} are built-in in Boogie, but
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    35
without a particular semantics due to different interpretations in
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    36
programming languages. We assume that each application comes with a
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    37
proper axiomatization.
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    38
*}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    39
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    40
axiomatization
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    41
  boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    42
  boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70)
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    43
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    44
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    45
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    46
section {* Setup *}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    47
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    48
ML_file "boogie.ML"
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    49
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    50
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    51
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    52
section {* Verification condition proofs *}
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    53
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    54
declare [[smt_oracle = false]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    55
declare [[smt_read_only_certificates = true]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    56
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    57
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    58
declare [[smt_certificates = "Boogie_Max.certs"]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    59
54447
019394de2b41 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents: 52722
diff changeset
    60
boogie_file Boogie_Max
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    61
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    62
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    63
declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    64
54447
019394de2b41 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents: 52722
diff changeset
    65
boogie_file Boogie_Dijkstra
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    66
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    67
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    68
declare [[z3_with_extensions = true]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    69
declare [[smt_certificates = "VCC_Max.certs"]]
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    70
54447
019394de2b41 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
wenzelm
parents: 52722
diff changeset
    71
boogie_file VCC_Max
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    72
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents:
diff changeset
    73
end