--- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
*)
-header "The Bytecode Verifier"
+header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
theory BVSpec = Effect:
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "BV Type Safety Proof"
+header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
theory BVSpecTypeSafe = Correct:
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Feb 21 09:54:08 2002 +0100
@@ -7,7 +7,7 @@
The invariant for the type safety proof.
*)
-header "BV Type Safety Invariant"
+header {* \isaheader{BV Type Safety Invariant} *}
theory Correct = BVSpec + JVMExec:
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Effect of Instructions on the State Type *}
+header {* \isaheader{Effect of Instructions on the State Type} *}
theory Effect = JVMType + JVMExceptions:
--- a/src/HOL/MicroJava/BV/EffectMono.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Monotonicity of eff and app *}
+header {* \isaheader{Monotonicity of eff and app} *}
theory EffectMono = Effect:
--- a/src/HOL/MicroJava/BV/Err.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
The error type
*)
-header "The Error Type"
+header {* \isaheader{The Error Type} *}
theory Err = Semilat:
--- a/src/HOL/MicroJava/BV/JType.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 TUM
*)
-header "The Java Type System as Semilattice"
+header {* \isaheader{The Java Type System as Semilattice} *}
theory JType = WellForm + Err:
--- a/src/HOL/MicroJava/BV/JVM.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 TUM
*)
-header "Kildall for the JVM"
+header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
EffectMono + BVSpec:
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
*)
-header "The JVM Type System as Semilattice"
+header {* \isaheader{The JVM Type System as Semilattice} *}
theory JVMType = Opt + Product + Listn + JType:
--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
Kildall's algorithm
*)
-header "Kildall's Algorithm"
+header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
theory Kildall = Typing_Framework + While_Combinator + Product:
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Completeness of the LBV *}
+header {* \isaheader{Completeness of the LBV} *}
(* This theory is currently broken. The port to exceptions
didn't make it into the Isabelle 2001 release. It is included for
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* Correctness of the LBV *}
+header {* \isaheader{Correctness of the LBV} *}
(* This theory is currently broken. The port to exceptions
didn't make it into the Isabelle 2001 release. It is included for
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* The Lightweight Bytecode Verifier *}
+header {* \isaheader{The Lightweight Bytecode Verifier} *}
theory LBVSpec = Effect + Kildall:
--- a/src/HOL/MicroJava/BV/Listn.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
Lists of a fixed length
*)
-header "Fixed Length Lists"
+header {* \isaheader{Fixed Length Lists} *}
theory Listn = Err:
--- a/src/HOL/MicroJava/BV/Opt.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
More about options
*)
-header "More about Options"
+header {* \isaheader{More about Options} *}
theory Opt = Err:
--- a/src/HOL/MicroJava/BV/Product.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
Products as semilattices
*)
-header "Products as Semilattices"
+header {* \isaheader{Products as Semilattices} *}
theory Product = Err:
--- a/src/HOL/MicroJava/BV/Semilat.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,10 @@
Semilattices
*)
-header "Semilattices"
+header {*
+ \chapter{Bytecode Verifier}\label{cha:bv}
+ \isaheader{Semilattices}
+*}
theory Semilat = While_Combinator:
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 TUM
*)
-header "Typing and Dataflow Analysis Framework"
+header {* \isaheader{Typing and Dataflow Analysis Framework} *}
theory Typing_Framework = Listn:
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
*)
-header "Static and Dynamic Welltyping"
+header {* \isaheader{Static and Dynamic Welltyping} *}
theory Typing_Framework_err = Typing_Framework:
--- a/src/HOL/MicroJava/J/Conform.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Conformity Relations for Type Soundness Proof"
+header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
theory Conform = State + WellType:
--- a/src/HOL/MicroJava/J/Decl.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Class Declarations and Programs"
+header {* \isaheader{Class Declarations and Programs} *}
theory Decl = Type:
--- a/src/HOL/MicroJava/J/Eval.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Operational Evaluation (big step) Semantics"
+header {* \isaheader{Operational Evaluation (big step) Semantics} *}
theory Eval = State + WellType:
--- a/src/HOL/MicroJava/J/Example.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Example MicroJava Program"
+header {* \isaheader{Example MicroJava Program} *}
theory Example = Eval:
--- a/src/HOL/MicroJava/J/JBasis.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,10 @@
Copyright 1999 TU Muenchen
*)
-header "Some Auxiliary Definitions"
+header {*
+ \chapter{Java Source Language}\label{cha:j}
+ \isaheader{Some Auxiliary Definitions}
+*}
theory JBasis = Main:
--- a/src/HOL/MicroJava/J/JListExample.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Thu Feb 21 09:54:08 2002 +0100
@@ -3,7 +3,7 @@
Author: Stefan Berghofer
*)
-header {* Example for generating executable code from Java semantics *}
+header {* \isaheader{Example for generating executable code from Java semantics} *}
theory JListExample = Eval:
@@ -107,7 +107,7 @@
Expr ({list_name}(LAcc l1_name)..
append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
-subsection {* Big step execution *}
+section {* Big step execution *}
ML {*
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Type Safety Proof"
+header {* \isaheader{Type Safety Proof} *}
theory JTypeSafe = Eval + Conform:
--- a/src/HOL/MicroJava/J/State.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/State.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Program State"
+header {* \isaheader{Program State} *}
theory State = TypeRel + Value:
--- a/src/HOL/MicroJava/J/Term.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Expressions and Statements"
+header {* \isaheader{Expressions and Statements} *}
theory Term = Value:
--- a/src/HOL/MicroJava/J/Type.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Java types"
+header {* \isaheader{Java types} *}
theory Type = JBasis:
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Relations between Java Types"
+header {* \isaheader{Relations between Java Types} *}
theory TypeRel = Decl:
--- a/src/HOL/MicroJava/J/Value.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Java Values"
+header {* \isaheader{Java Values} *}
theory Value = Type:
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Well-formedness of Java programs"
+header {* \isaheader{Well-formedness of Java programs} *}
theory WellForm = TypeRel:
--- a/src/HOL/MicroJava/J/WellType.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Well-typedness Constraints"
+header {* \isaheader{Well-typedness Constraints} *}
theory WellType = Term + WellForm:
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header {* Exception handling in the JVM *}
+header {* \isaheader{Exception handling in the JVM} *}
theory JVMExceptions = JVMInstructions:
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* Program Execution in the JVM *}
+header {* \isaheader{Program Execution in the JVM} *}
theory JVMExec = JVMExecInstr + JVMExceptions:
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
*)
-header {* JVM Instruction Semantics *}
+header {* \isaheader{JVM Instruction Semantics} *}
theory JVMExecInstr = JVMInstructions + JVMState:
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Instructions of the JVM *}
+header {* \isaheader{Instructions of the JVM} *}
theory JVMInstructions = JVMState:
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Feb 21 09:54:08 2002 +0100
@@ -3,7 +3,7 @@
Author: Stefan Berghofer
*)
-header {* Example for generating executable code from JVM semantics *}
+header {* \isaheader{Example for generating executable code from JVM semantics} *}
theory JVMListExample = JVMExec:
--- a/src/HOL/MicroJava/JVM/JVMState.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,10 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* State of the JVM *}
+header {*
+ \chapter{Java Virtual Machine}\label{cha:jvm}
+ \isaheader{State of the JVM}
+*}
theory JVMState = Conform:
--- a/src/HOL/MicroJava/ROOT.ML Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Thu Feb 21 09:54:08 2002 +0100
@@ -4,15 +4,17 @@
add_path "JVM";
add_path "BV";
+no_document use_thy "While_Combinator";
+
use_thy "JTypeSafe";
use_thy "Example";
use_thy "JListExample";
use_thy "JVMListExample";
use_thy "BVSpecTypeSafe";
use_thy "JVM";
-use_thy "LBVSpec";
(* momentarily broken:
+use_thy "LBVSpec";
use_thy "LBVCorrect";
use_thy "LBVComplete";
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/document/introduction.tex Thu Feb 21 09:54:08 2002 +0100
@@ -0,0 +1,110 @@
+
+\section*{Introduction}
+\label{sec:introduction}
+
+This document contains the automatically generated listings of the
+Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard,
+dedicated to the study of the interaction of the source language, byte
+code, the byte code verifier and the compiler. In order to make the
+Isabelle sources more accessible, this introduction provides a brief
+survey of the main concepts of \mJava.
+
+The \mJava{} \textbf{source language} (see \charef{cha:j})
+only comprises a part of the original JavaCard language. It models
+features such as:
+\begin{itemize}
+\item The basic ``primitive types'' of Java
+\item Object orientation, in particular classes, and relevant
+ relations on classes (subclass, widening)
+
+\item Methods and method signatures
+\item Inheritance and overriding of methods, dynamic binding
+
+\item Representatives of ``relevant'' expressions and statements
+\item Generation and propagation of system exceptions
+\end{itemize}
+
+However, the following features are missing in \mJava{} wrt.{} JavaCard:
+\begin{itemize}
+\item Some primitive types (\texttt{byte, short})
+\item Interfaces and related concepts, arrays
+\item Most numeric operations, syntactic variants of statements
+ (\texttt{do}-loop, \texttt{for}-loop)
+\item Complex block structure, method bodies with multiple returns
+\item Abrupt termination (\texttt{break, continue})
+\item Class and method modifiers (such as \texttt{static} and
+ \texttt{public/private} access modifiers)
+\item User-defined exception classes and an explicit
+ \texttt{throw}-statement. Exceptions cannot be caught.
+\item A ``definite assignment'' check
+\end{itemize}
+In addition, features are missing that are not part of the JavaCard
+language, such as multithreading and garbage collection. No attempt
+has been made to model peculiarities of JavaCard such as the applet
+firewall or the transaction mechanism.
+
+For a more complete Isabelle model of JavaCard, the reader should
+consult the Bali formalization
+(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
+models most of the source language features of JavaCard, however without
+describing the bytecode level.
+
+The central topics of the source language formalization are:
+\begin{itemize}
+\item Description of the structure of the ``runtime environment'', in
+ particular structure of classes and the program state
+\item Definition of syntax, typing rules and operational semantics of
+ statements and expressions
+\item Definition of ``conformity'' (characterizing type safety) and a
+ type safety proof
+\end{itemize}
+
+
+The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm})
+corresponds rather directly to the source level, in the sense that the
+same data types are supported and bytecode instructions required for
+emulating the source level operations are provided. Again, only one
+representative of different variants of instructions has been
+selected; for example, there is only one comparison operator. The
+formalization of the bytecode level is purely descriptive (``no
+theorems'') and rather brief as compared to the source level; all
+questions related to type systems for and type correctness of bytecode
+are dealt with in chapter on bytecode verification.
+
+The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is
+dealt with in several stages:
+\begin{itemize}
+\item First, the notion of ``method type'' is introduced, which
+ corresponds to the notion of ``type'' on the source level.
+\item Well-typedness of instructions wrt. a method type is defined
+ (see \secref{sec:BVSpec}). Roughly speaking, determining
+ well-typedness is \emph{type checking}.
+\item It is shown that bytecode that is well-typed in this sense can
+ be safely executed -- a type soundness proof on the bytecode level
+ (\secref{sec:BVSpecTypeSafe}).
+\item Given raw bytecode, one of the purposes of bytecode verification
+ is to determine a method type that is well-typed according to the
+ above definition. Roughly speaking, this is \emph{type inference}.
+ The Isabelle formalization presents bytecode verification as an
+ instance of an abstract dataflow algorithm (Kildall's algorithm, see
+ \secrefs{sec:Kildall} to \ref{sec:JVM}).
+%\item For \emph{lightweight bytecode verification}, type checking of
+% bytecode can be reduced to method types with small size.
+\end{itemize}
+
+Bytecode verification in \mJava{} so far takes into account:
+\begin{itemize}
+\item Operations and branching instructions
+\item Exceptions
+\end{itemize}
+Initialization during object creation is not accounted for in the
+present document
+(see the formalization in
+\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
+neither is the \texttt{jsr} instruction.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/src/HOL/MicroJava/document/root.tex Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/document/root.tex Thu Feb 21 09:54:08 2002 +0100
@@ -1,26 +1,36 @@
-
-\documentclass[11pt,a4paper]{article}
+%\documentclass[11pt,a4paper]{article}
+\documentclass[11pt,a4paper]{book}
\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
\urlstyle{rm}
\pagestyle{myheadings}
+%make a bit more space
\addtolength{\hoffset}{-1,5cm}
\addtolength{\textwidth}{4cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{4cm}
%subsection instead of section to make the toc readable
+\newcommand{\isaheader}[1]
+{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
\renewcommand{\thesubsection}{\arabic{subsection}}
-\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
+\renewcommand{\isamarkupheader}[1]{#1}
\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
+\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
%remove spaces from the isabelle environment (trivlist makes them too large)
-\renewenvironment{isabelle}
-{\begin{isabellebody}}
-{\end{isabellebody}}
+%\renewenvironment{isabelle}
+%{\begin{isabellebody}}
+%{\end{isabellebody}}
+
\newcommand{\mJava}{$\mu$Java}
+\newcommand{\secref}[1]{Section~\ref{#1}}
+\newcommand{\secrefs}[1]{Sections~\ref{#1}}
+\newcommand{\charef}[1]{Chapter~\ref{#1}}
+\newcommand{\charefs}[1]{Chapters~\ref{#1}}
+
%remove clutter from the toc
\setcounter{secnumdepth}{3}
@@ -28,27 +38,30 @@
\begin{document}
-\title{\mJava}
-\author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
+\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\
+% {\large -- VerifiCard Project Deliverables -- }
+}
+\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
+ Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
\maketitle
-\begin{abstract}\noindent
- This formal development defines {\mJava}, a small fragment of the
- programming language Java (with essentially just classes), together with a
- corresponding virtual machine, a specification of its bytecode verifier
- and a lightweight bytecode verifier.
- It is shown that {\mJava} and the given specification of the bytecode
- verifier are type-safe, and that the lightweight bytecode verifier
- is functionally equivalent to the bytecode verifier specification.
- See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
-\end{abstract}
\tableofcontents
\parindent 0pt \parskip 0.5ex
+\input{introduction.tex}
+
+\section*{Theory Dependencies}
+
+Figure \ref{theory-deps} shows the dependencies between
+the Isabelle theories in the following sections.
+
+\begin{figure}
\begin{center}
\includegraphics[scale=0.4]{session_graph}
\end{center}
+\caption{Theory Dependency Graph\label{theory-deps}}
+\end{figure}
\newpage
\input{session}