# HG changeset patch # User kleing # Date 1014281648 -3600 # Node ID 704713ca07eada8af4431d230aa9ea3f7d8f06f6 # Parent f5bceeec9d91f642ac39549639272852d82b0303 new document diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/BVSpec.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Correct.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Effect.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/EffectMono.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Err.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JType.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JVM.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JVMType.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Kildall.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVComplete.thy --- 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 diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVCorrect.thy --- 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 diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVSpec.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Listn.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Opt.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Product.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Semilat.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Typing_Framework.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Typing_Framework_err.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Conform.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Decl.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Eval.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Example.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JBasis.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JListExample.thy --- 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 {* diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JTypeSafe.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/State.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Term.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Type.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/TypeRel.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Value.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/WellForm.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/WellType.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExceptions.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExec.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExecInstr.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMInstructions.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMListExample.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMState.thy --- 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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/ROOT.ML --- 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"; *) diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/document/introduction.tex --- /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: diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/document/root.tex --- 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}