new document
authorkleing
Thu Feb 21 09:54:08 2002 +0100 (2002-02-21)
changeset 12911704713ca07ea
parent 12910 f5bceeec9d91
child 12912 0e144958cf27
new document
src/HOL/MicroJava/BV/BVSpec.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Opt.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/BV/Typing_Framework.thy
src/HOL/MicroJava/BV/Typing_Framework_err.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/JVMExceptions.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/MicroJava/JVM/JVMExecInstr.thy
src/HOL/MicroJava/JVM/JVMInstructions.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/MicroJava/JVM/JVMState.thy
src/HOL/MicroJava/ROOT.ML
src/HOL/MicroJava/document/introduction.tex
src/HOL/MicroJava/document/root.tex
     1.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Feb 20 17:30:46 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Feb 21 09:54:08 2002 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -header "The Bytecode Verifier"
     1.8 +header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
     1.9  
    1.10  theory BVSpec = Effect:
    1.11  
     2.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Feb 20 17:30:46 2002 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Feb 21 09:54:08 2002 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4      Copyright   1999 Technische Universitaet Muenchen
     2.5  *)
     2.6  
     2.7 -header "BV Type Safety Proof"
     2.8 +header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
     2.9  
    2.10  theory BVSpecTypeSafe = Correct:
    2.11  
     3.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 20 17:30:46 2002 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 21 09:54:08 2002 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  The invariant for the type safety proof.
     3.5  *)
     3.6  
     3.7 -header "BV Type Safety Invariant"
     3.8 +header {* \isaheader{BV Type Safety Invariant} *}
     3.9  
    3.10  theory Correct = BVSpec + JVMExec:
    3.11  
     4.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Wed Feb 20 17:30:46 2002 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Thu Feb 21 09:54:08 2002 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4      Copyright   2000 Technische Universitaet Muenchen
     4.5  *)
     4.6  
     4.7 -header {* Effect of Instructions on the State Type *}
     4.8 +header {* \isaheader{Effect of Instructions on the State Type} *}
     4.9  
    4.10  theory Effect = JVMType + JVMExceptions:
    4.11  
     5.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Feb 20 17:30:46 2002 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Feb 21 09:54:08 2002 +0100
     5.3 @@ -4,7 +4,7 @@
     5.4      Copyright   2000 Technische Universitaet Muenchen
     5.5  *)
     5.6  
     5.7 -header {* Monotonicity of eff and app *}
     5.8 +header {* \isaheader{Monotonicity of eff and app} *}
     5.9  
    5.10  theory EffectMono = Effect:
    5.11  
     6.1 --- a/src/HOL/MicroJava/BV/Err.thy	Wed Feb 20 17:30:46 2002 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Thu Feb 21 09:54:08 2002 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  The error type
     6.5  *)
     6.6  
     6.7 -header "The Error Type"
     6.8 +header {* \isaheader{The Error Type} *}
     6.9  
    6.10  theory Err = Semilat:
    6.11  
     7.1 --- a/src/HOL/MicroJava/BV/JType.thy	Wed Feb 20 17:30:46 2002 +0100
     7.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Thu Feb 21 09:54:08 2002 +0100
     7.3 @@ -4,7 +4,7 @@
     7.4      Copyright   2000 TUM
     7.5  *)
     7.6  
     7.7 -header "The Java Type System as Semilattice"
     7.8 +header {* \isaheader{The Java Type System as Semilattice} *}
     7.9  
    7.10  theory JType = WellForm + Err:
    7.11  
     8.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Wed Feb 20 17:30:46 2002 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Feb 21 09:54:08 2002 +0100
     8.3 @@ -4,7 +4,7 @@
     8.4      Copyright   2000 TUM
     8.5  *)
     8.6  
     8.7 -header "Kildall for the JVM"
     8.8 +header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
     8.9  
    8.10  theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
    8.11               EffectMono + BVSpec:
     9.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 20 17:30:46 2002 +0100
     9.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Thu Feb 21 09:54:08 2002 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4  
     9.5  *)
     9.6  
     9.7 -header "The JVM Type System as Semilattice"
     9.8 +header {* \isaheader{The JVM Type System as Semilattice} *}
     9.9  
    9.10  theory JVMType = Opt + Product + Listn + JType:
    9.11  
    10.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 20 17:30:46 2002 +0100
    10.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Feb 21 09:54:08 2002 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  Kildall's algorithm
    10.5  *)
    10.6  
    10.7 -header "Kildall's Algorithm"
    10.8 +header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
    10.9  
   10.10  theory Kildall = Typing_Framework + While_Combinator + Product:
   10.11  
    11.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Feb 20 17:30:46 2002 +0100
    11.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Feb 21 09:54:08 2002 +0100
    11.3 @@ -4,7 +4,7 @@
    11.4      Copyright   2000 Technische Universitaet Muenchen
    11.5  *)
    11.6  
    11.7 -header {* Completeness of the LBV *}
    11.8 +header {* \isaheader{Completeness of the LBV} *}
    11.9  
   11.10  (* This theory is currently broken. The port to exceptions
   11.11    didn't make it into the Isabelle 2001 release. It is included for 
    12.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Feb 20 17:30:46 2002 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Feb 21 09:54:08 2002 +0100
    12.3 @@ -4,7 +4,7 @@
    12.4      Copyright   1999 Technische Universitaet Muenchen
    12.5  *)
    12.6  
    12.7 -header {* Correctness of the LBV *}
    12.8 +header {* \isaheader{Correctness of the LBV} *}
    12.9  
   12.10  (* This theory is currently broken. The port to exceptions
   12.11    didn't make it into the Isabelle 2001 release. It is included for 
    13.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Feb 20 17:30:46 2002 +0100
    13.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 21 09:54:08 2002 +0100
    13.3 @@ -4,7 +4,7 @@
    13.4      Copyright   1999 Technische Universitaet Muenchen
    13.5  *)
    13.6  
    13.7 -header {* The Lightweight Bytecode Verifier *}
    13.8 +header {* \isaheader{The Lightweight Bytecode Verifier} *}
    13.9  
   13.10  theory LBVSpec = Effect + Kildall:
   13.11  
    14.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 20 17:30:46 2002 +0100
    14.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Thu Feb 21 09:54:08 2002 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  Lists of a fixed length
    14.5  *)
    14.6  
    14.7 -header "Fixed Length Lists"
    14.8 +header {* \isaheader{Fixed Length Lists} *}
    14.9  
   14.10  theory Listn = Err:
   14.11  
    15.1 --- a/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 20 17:30:46 2002 +0100
    15.2 +++ b/src/HOL/MicroJava/BV/Opt.thy	Thu Feb 21 09:54:08 2002 +0100
    15.3 @@ -6,7 +6,7 @@
    15.4  More about options
    15.5  *)
    15.6  
    15.7 -header "More about Options"
    15.8 +header {* \isaheader{More about Options} *}
    15.9  
   15.10  theory Opt = Err:
   15.11  
    16.1 --- a/src/HOL/MicroJava/BV/Product.thy	Wed Feb 20 17:30:46 2002 +0100
    16.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Thu Feb 21 09:54:08 2002 +0100
    16.3 @@ -6,7 +6,7 @@
    16.4  Products as semilattices
    16.5  *)
    16.6  
    16.7 -header "Products as Semilattices"
    16.8 +header {* \isaheader{Products as Semilattices} *}
    16.9  
   16.10  theory Product = Err:
   16.11  
    17.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 20 17:30:46 2002 +0100
    17.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Feb 21 09:54:08 2002 +0100
    17.3 @@ -6,7 +6,10 @@
    17.4  Semilattices
    17.5  *)
    17.6  
    17.7 -header "Semilattices"
    17.8 +header {* 
    17.9 +  \chapter{Bytecode Verifier}\label{cha:bv}
   17.10 +  \isaheader{Semilattices} 
   17.11 +*}
   17.12  
   17.13  theory Semilat = While_Combinator:
   17.14  
    18.1 --- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Feb 20 17:30:46 2002 +0100
    18.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Feb 21 09:54:08 2002 +0100
    18.3 @@ -4,7 +4,7 @@
    18.4      Copyright   2000 TUM
    18.5  *)
    18.6  
    18.7 -header "Typing and Dataflow Analysis Framework"
    18.8 +header {* \isaheader{Typing and Dataflow Analysis Framework} *}
    18.9  
   18.10  theory Typing_Framework = Listn:
   18.11  
    19.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Feb 20 17:30:46 2002 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Thu Feb 21 09:54:08 2002 +0100
    19.3 @@ -5,7 +5,7 @@
    19.4  
    19.5  *)
    19.6  
    19.7 -header "Static and Dynamic Welltyping"
    19.8 +header {* \isaheader{Static and Dynamic Welltyping} *}
    19.9  
   19.10  theory Typing_Framework_err = Typing_Framework:
   19.11  
    20.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed Feb 20 17:30:46 2002 +0100
    20.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Thu Feb 21 09:54:08 2002 +0100
    20.3 @@ -4,7 +4,7 @@
    20.4      Copyright   1999 Technische Universitaet Muenchen
    20.5  *)
    20.6  
    20.7 -header "Conformity Relations for Type Soundness Proof"
    20.8 +header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
    20.9  
   20.10  theory Conform = State + WellType:
   20.11  
    21.1 --- a/src/HOL/MicroJava/J/Decl.thy	Wed Feb 20 17:30:46 2002 +0100
    21.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Thu Feb 21 09:54:08 2002 +0100
    21.3 @@ -4,7 +4,7 @@
    21.4      Copyright   1999 Technische Universitaet Muenchen
    21.5  *)
    21.6  
    21.7 -header "Class Declarations and Programs"
    21.8 +header {* \isaheader{Class Declarations and Programs} *}
    21.9  
   21.10  theory Decl = Type:
   21.11  
    22.1 --- a/src/HOL/MicroJava/J/Eval.thy	Wed Feb 20 17:30:46 2002 +0100
    22.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Thu Feb 21 09:54:08 2002 +0100
    22.3 @@ -4,7 +4,7 @@
    22.4      Copyright   1999 Technische Universitaet Muenchen
    22.5  *)
    22.6  
    22.7 -header "Operational Evaluation (big step) Semantics"
    22.8 +header {* \isaheader{Operational Evaluation (big step) Semantics} *}
    22.9  
   22.10  theory Eval = State + WellType:
   22.11  
    23.1 --- a/src/HOL/MicroJava/J/Example.thy	Wed Feb 20 17:30:46 2002 +0100
    23.2 +++ b/src/HOL/MicroJava/J/Example.thy	Thu Feb 21 09:54:08 2002 +0100
    23.3 @@ -4,7 +4,7 @@
    23.4      Copyright   1999 Technische Universitaet Muenchen
    23.5  *)
    23.6  
    23.7 -header "Example MicroJava Program"
    23.8 +header {* \isaheader{Example MicroJava Program} *}
    23.9  
   23.10  theory Example = Eval:
   23.11  
    24.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Wed Feb 20 17:30:46 2002 +0100
    24.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 21 09:54:08 2002 +0100
    24.3 @@ -4,7 +4,10 @@
    24.4      Copyright   1999 TU Muenchen
    24.5  *)
    24.6  
    24.7 -header "Some Auxiliary Definitions"
    24.8 +header {* 
    24.9 +  \chapter{Java Source Language}\label{cha:j}
   24.10 +  \isaheader{Some Auxiliary Definitions}
   24.11 +*}
   24.12  
   24.13  theory JBasis = Main: 
   24.14  
    25.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Wed Feb 20 17:30:46 2002 +0100
    25.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Feb 21 09:54:08 2002 +0100
    25.3 @@ -3,7 +3,7 @@
    25.4      Author:     Stefan Berghofer
    25.5  *)
    25.6  
    25.7 -header {* Example for generating executable code from Java semantics *}
    25.8 +header {* \isaheader{Example for generating executable code from Java semantics} *}
    25.9  
   25.10  theory JListExample = Eval:
   25.11  
   25.12 @@ -107,7 +107,7 @@
   25.13        Expr ({list_name}(LAcc l1_name)..
   25.14          append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
   25.15  
   25.16 -subsection {* Big step execution *}
   25.17 +section {* Big step execution *}
   25.18  
   25.19  ML {*
   25.20  
    26.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 20 17:30:46 2002 +0100
    26.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 21 09:54:08 2002 +0100
    26.3 @@ -4,7 +4,7 @@
    26.4      Copyright   1999 Technische Universitaet Muenchen
    26.5  *)
    26.6  
    26.7 -header "Type Safety Proof"
    26.8 +header {* \isaheader{Type Safety Proof} *}
    26.9  
   26.10  theory JTypeSafe = Eval + Conform:
   26.11  
    27.1 --- a/src/HOL/MicroJava/J/State.thy	Wed Feb 20 17:30:46 2002 +0100
    27.2 +++ b/src/HOL/MicroJava/J/State.thy	Thu Feb 21 09:54:08 2002 +0100
    27.3 @@ -4,7 +4,7 @@
    27.4      Copyright   1999 Technische Universitaet Muenchen
    27.5  *)
    27.6  
    27.7 -header "Program State"
    27.8 +header {* \isaheader{Program State} *}
    27.9  
   27.10  theory State = TypeRel + Value:
   27.11  
    28.1 --- a/src/HOL/MicroJava/J/Term.thy	Wed Feb 20 17:30:46 2002 +0100
    28.2 +++ b/src/HOL/MicroJava/J/Term.thy	Thu Feb 21 09:54:08 2002 +0100
    28.3 @@ -4,7 +4,7 @@
    28.4      Copyright   1999 Technische Universitaet Muenchen
    28.5  *)
    28.6  
    28.7 -header "Expressions and Statements"
    28.8 +header {* \isaheader{Expressions and Statements} *}
    28.9  
   28.10  theory Term = Value:
   28.11  
    29.1 --- a/src/HOL/MicroJava/J/Type.thy	Wed Feb 20 17:30:46 2002 +0100
    29.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Feb 21 09:54:08 2002 +0100
    29.3 @@ -4,7 +4,7 @@
    29.4      Copyright   1999 Technische Universitaet Muenchen
    29.5  *)
    29.6  
    29.7 -header "Java types"
    29.8 +header {* \isaheader{Java types} *}
    29.9  
   29.10  theory Type = JBasis:
   29.11  
    30.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Feb 20 17:30:46 2002 +0100
    30.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 21 09:54:08 2002 +0100
    30.3 @@ -4,7 +4,7 @@
    30.4      Copyright   1999 Technische Universitaet Muenchen
    30.5  *)
    30.6  
    30.7 -header "Relations between Java Types"
    30.8 +header {* \isaheader{Relations between Java Types} *}
    30.9  
   30.10  theory TypeRel = Decl:
   30.11  
    31.1 --- a/src/HOL/MicroJava/J/Value.thy	Wed Feb 20 17:30:46 2002 +0100
    31.2 +++ b/src/HOL/MicroJava/J/Value.thy	Thu Feb 21 09:54:08 2002 +0100
    31.3 @@ -4,7 +4,7 @@
    31.4      Copyright   1999 Technische Universitaet Muenchen
    31.5  *)
    31.6  
    31.7 -header "Java Values"
    31.8 +header {* \isaheader{Java Values} *}
    31.9  
   31.10  theory Value = Type:
   31.11  
    32.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 20 17:30:46 2002 +0100
    32.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Feb 21 09:54:08 2002 +0100
    32.3 @@ -4,7 +4,7 @@
    32.4      Copyright   1999 Technische Universitaet Muenchen
    32.5  *)
    32.6  
    32.7 -header "Well-formedness of Java programs"
    32.8 +header {* \isaheader{Well-formedness of Java programs} *}
    32.9  
   32.10  theory WellForm = TypeRel:
   32.11  
    33.1 --- a/src/HOL/MicroJava/J/WellType.thy	Wed Feb 20 17:30:46 2002 +0100
    33.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Thu Feb 21 09:54:08 2002 +0100
    33.3 @@ -4,7 +4,7 @@
    33.4      Copyright   1999 Technische Universitaet Muenchen
    33.5  *)
    33.6  
    33.7 -header "Well-typedness Constraints"
    33.8 +header {* \isaheader{Well-typedness Constraints} *}
    33.9  
   33.10  theory WellType = Term + WellForm:
   33.11  
    34.1 --- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Wed Feb 20 17:30:46 2002 +0100
    34.2 +++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Thu Feb 21 09:54:08 2002 +0100
    34.3 @@ -4,7 +4,7 @@
    34.4      Copyright   2001 Technische Universitaet Muenchen
    34.5  *)
    34.6  
    34.7 -header {* Exception handling in the JVM *}
    34.8 +header {* \isaheader{Exception handling in the JVM} *}
    34.9  
   34.10  theory JVMExceptions = JVMInstructions:
   34.11  
    35.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Feb 20 17:30:46 2002 +0100
    35.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Feb 21 09:54:08 2002 +0100
    35.3 @@ -4,7 +4,7 @@
    35.4      Copyright   1999 Technische Universitaet Muenchen
    35.5  *)
    35.6  
    35.7 -header {* Program Execution in the JVM *}
    35.8 +header {* \isaheader{Program Execution in the JVM} *}
    35.9  
   35.10  theory JVMExec = JVMExecInstr + JVMExceptions:
   35.11  
    36.1 --- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Feb 20 17:30:46 2002 +0100
    36.2 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Feb 21 09:54:08 2002 +0100
    36.3 @@ -5,7 +5,7 @@
    36.4  *)
    36.5  
    36.6  
    36.7 -header {* JVM Instruction Semantics *}
    36.8 +header {* \isaheader{JVM Instruction Semantics} *}
    36.9  
   36.10  
   36.11  theory JVMExecInstr = JVMInstructions + JVMState:
    37.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Wed Feb 20 17:30:46 2002 +0100
    37.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Feb 21 09:54:08 2002 +0100
    37.3 @@ -4,7 +4,7 @@
    37.4      Copyright   2000 Technische Universitaet Muenchen
    37.5  *)
    37.6  
    37.7 -header {* Instructions of the JVM *}
    37.8 +header {* \isaheader{Instructions of the JVM} *}
    37.9  
   37.10  
   37.11  theory JVMInstructions = JVMState:
    38.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Feb 20 17:30:46 2002 +0100
    38.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Feb 21 09:54:08 2002 +0100
    38.3 @@ -3,7 +3,7 @@
    38.4      Author:     Stefan Berghofer
    38.5  *)
    38.6  
    38.7 -header {* Example for generating executable code from JVM semantics *}
    38.8 +header {* \isaheader{Example for generating executable code from JVM semantics} *}
    38.9  
   38.10  theory JVMListExample = JVMExec:
   38.11  
    39.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Feb 20 17:30:46 2002 +0100
    39.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 21 09:54:08 2002 +0100
    39.3 @@ -4,7 +4,10 @@
    39.4      Copyright   1999 Technische Universitaet Muenchen
    39.5  *)
    39.6  
    39.7 -header {* State of the JVM *}
    39.8 +header {* 
    39.9 +  \chapter{Java Virtual Machine}\label{cha:jvm}
   39.10 +  \isaheader{State of the JVM} 
   39.11 +*}
   39.12  
   39.13  theory JVMState = Conform:
   39.14  
    40.1 --- a/src/HOL/MicroJava/ROOT.ML	Wed Feb 20 17:30:46 2002 +0100
    40.2 +++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 21 09:54:08 2002 +0100
    40.3 @@ -4,15 +4,17 @@
    40.4  add_path "JVM";
    40.5  add_path "BV";
    40.6  
    40.7 +no_document use_thy "While_Combinator";
    40.8 +
    40.9  use_thy "JTypeSafe";
   40.10  use_thy "Example";
   40.11  use_thy "JListExample";
   40.12  use_thy "JVMListExample";
   40.13  use_thy "BVSpecTypeSafe";
   40.14  use_thy "JVM";
   40.15 -use_thy "LBVSpec"; 
   40.16  
   40.17  (* momentarily broken:
   40.18 +use_thy "LBVSpec"; 
   40.19  use_thy "LBVCorrect";
   40.20  use_thy "LBVComplete";
   40.21  *)
    41.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    41.2 +++ b/src/HOL/MicroJava/document/introduction.tex	Thu Feb 21 09:54:08 2002 +0100
    41.3 @@ -0,0 +1,110 @@
    41.4 +
    41.5 +\section*{Introduction}
    41.6 +\label{sec:introduction}
    41.7 +
    41.8 +This document contains the automatically generated listings of the
    41.9 +Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard,
   41.10 +dedicated to the study of the interaction of the source language, byte
   41.11 +code, the byte code verifier and the compiler. In order to make the
   41.12 +Isabelle sources more accessible, this introduction provides a brief
   41.13 +survey of the main concepts of \mJava.
   41.14 +
   41.15 +The \mJava{} \textbf{source language} (see \charef{cha:j})
   41.16 +only comprises a part of the original JavaCard language. It models
   41.17 +features such as:
   41.18 +\begin{itemize}
   41.19 +\item The basic ``primitive types'' of Java 
   41.20 +\item Object orientation, in particular classes, and relevant
   41.21 +  relations on classes (subclass, widening)
   41.22 +
   41.23 +\item Methods and method signatures
   41.24 +\item Inheritance and overriding of methods, dynamic binding
   41.25 +
   41.26 +\item Representatives of ``relevant'' expressions and statements 
   41.27 +\item Generation and propagation of system exceptions
   41.28 +\end{itemize}
   41.29 +
   41.30 +However, the following features are missing in \mJava{} wrt.{} JavaCard:
   41.31 +\begin{itemize}
   41.32 +\item Some primitive types (\texttt{byte, short})
   41.33 +\item Interfaces and related concepts, arrays
   41.34 +\item Most numeric operations, syntactic variants of statements
   41.35 +  (\texttt{do}-loop, \texttt{for}-loop)
   41.36 +\item Complex block structure, method bodies with multiple returns
   41.37 +\item Abrupt termination (\texttt{break, continue})
   41.38 +\item Class and method modifiers (such as \texttt{static} and
   41.39 +  \texttt{public/private} access modifiers)
   41.40 +\item User-defined exception classes and an explicit
   41.41 +  \texttt{throw}-statement. Exceptions cannot be caught.
   41.42 +\item A ``definite assignment'' check
   41.43 +\end{itemize}
   41.44 +In addition, features are missing that are not part of the JavaCard
   41.45 +language, such as multithreading and garbage collection. No attempt
   41.46 +has been made to model peculiarities of JavaCard such as the applet
   41.47 +firewall or the transaction mechanism.
   41.48 +
   41.49 +For a more complete Isabelle model of JavaCard, the reader should
   41.50 +consult the Bali formalization
   41.51 +(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
   41.52 +models most of the source language features of JavaCard, however without
   41.53 +describing the bytecode level.
   41.54 +
   41.55 +The central topics of the source language formalization are:
   41.56 +\begin{itemize}
   41.57 +\item Description of the structure of the ``runtime environment'', in
   41.58 +  particular structure of classes and the program state
   41.59 +\item Definition of syntax, typing rules and operational semantics of
   41.60 +  statements and expressions
   41.61 +\item Definition of ``conformity'' (characterizing type safety) and a
   41.62 +  type safety proof
   41.63 +\end{itemize}
   41.64 +
   41.65 +
   41.66 +The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm})
   41.67 +corresponds rather directly to the source level, in the sense that the
   41.68 +same data types are supported and bytecode instructions required for
   41.69 +emulating the source level operations are provided. Again, only one
   41.70 +representative of different variants of instructions has been
   41.71 +selected; for example, there is only one comparison operator.  The
   41.72 +formalization of the bytecode level is purely descriptive (``no
   41.73 +theorems'') and rather brief as compared to the source level; all
   41.74 +questions related to type systems for and type correctness of bytecode
   41.75 +are dealt with in chapter on bytecode verification.
   41.76 +
   41.77 +The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is
   41.78 +dealt with in several stages:
   41.79 +\begin{itemize}
   41.80 +\item First, the notion of ``method type'' is introduced, which
   41.81 +  corresponds to the notion of ``type'' on the source level.
   41.82 +\item Well-typedness of instructions wrt. a method type is defined
   41.83 +  (see \secref{sec:BVSpec}). Roughly speaking, determining
   41.84 +  well-typedness is \emph{type checking}.
   41.85 +\item It is shown that bytecode that is well-typed in this sense can
   41.86 +  be safely executed -- a type soundness proof on the bytecode level
   41.87 +  (\secref{sec:BVSpecTypeSafe}). 
   41.88 +\item Given raw bytecode, one of the purposes of bytecode verification
   41.89 +  is to determine a method type that is well-typed according to the
   41.90 +  above definition. Roughly speaking, this is \emph{type inference}.
   41.91 +  The Isabelle formalization presents bytecode verification as an
   41.92 +  instance of an abstract dataflow algorithm (Kildall's algorithm, see
   41.93 +  \secrefs{sec:Kildall} to \ref{sec:JVM}).
   41.94 +%\item For \emph{lightweight bytecode verification}, type checking of
   41.95 +%  bytecode can be reduced to method types with small size. 
   41.96 +\end{itemize}
   41.97 +
   41.98 +Bytecode verification in \mJava{} so far takes into account:
   41.99 +\begin{itemize}
  41.100 +\item Operations and branching instructions
  41.101 +\item Exceptions
  41.102 +\end{itemize}
  41.103 +Initialization during object creation is not accounted for in the
  41.104 +present document 
  41.105 +(see the formalization in
  41.106 +\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
  41.107 +neither is the \texttt{jsr} instruction.
  41.108 +
  41.109 +
  41.110 +%%% Local Variables:
  41.111 +%%% mode: latex
  41.112 +%%% TeX-master: "root"
  41.113 +%%% End:
    42.1 --- a/src/HOL/MicroJava/document/root.tex	Wed Feb 20 17:30:46 2002 +0100
    42.2 +++ b/src/HOL/MicroJava/document/root.tex	Thu Feb 21 09:54:08 2002 +0100
    42.3 @@ -1,26 +1,36 @@
    42.4 -
    42.5 -\documentclass[11pt,a4paper]{article}
    42.6 +%\documentclass[11pt,a4paper]{article}
    42.7 +\documentclass[11pt,a4paper]{book}
    42.8  \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
    42.9  
   42.10  \urlstyle{rm}
   42.11  \pagestyle{myheadings}
   42.12  
   42.13 +%make a bit more space
   42.14  \addtolength{\hoffset}{-1,5cm}
   42.15  \addtolength{\textwidth}{4cm}
   42.16  \addtolength{\voffset}{-2cm}
   42.17  \addtolength{\textheight}{4cm}
   42.18  
   42.19  %subsection instead of section to make the toc readable
   42.20 +\newcommand{\isaheader}[1]
   42.21 +{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
   42.22  \renewcommand{\thesubsection}{\arabic{subsection}}
   42.23 -\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
   42.24 +\renewcommand{\isamarkupheader}[1]{#1}
   42.25  \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
   42.26 +\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
   42.27  
   42.28  %remove spaces from the isabelle environment (trivlist makes them too large)
   42.29 -\renewenvironment{isabelle}
   42.30 -{\begin{isabellebody}}
   42.31 -{\end{isabellebody}}
   42.32 +%\renewenvironment{isabelle}
   42.33 +%{\begin{isabellebody}}
   42.34 +%{\end{isabellebody}}
   42.35 +
   42.36  
   42.37  \newcommand{\mJava}{$\mu$Java}
   42.38 +\newcommand{\secref}[1]{Section~\ref{#1}}
   42.39 +\newcommand{\secrefs}[1]{Sections~\ref{#1}}
   42.40 +\newcommand{\charef}[1]{Chapter~\ref{#1}}
   42.41 +\newcommand{\charefs}[1]{Chapters~\ref{#1}}
   42.42 +
   42.43  
   42.44  %remove clutter from the toc
   42.45  \setcounter{secnumdepth}{3}
   42.46 @@ -28,27 +38,30 @@
   42.47  
   42.48  \begin{document}
   42.49  
   42.50 -\title{\mJava}
   42.51 -\author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
   42.52 +\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\
   42.53 +%  {\large -- VerifiCard Project Deliverables -- }
   42.54 +}
   42.55 +\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
   42.56 +  Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
   42.57  \maketitle
   42.58  
   42.59 -\begin{abstract}\noindent
   42.60 -  This formal development defines {\mJava}, a small fragment of the
   42.61 -  programming language Java (with essentially just classes), together with a
   42.62 -  corresponding virtual machine, a specification of its bytecode verifier
   42.63 -  and a lightweight bytecode verifier.
   42.64 -  It is shown that {\mJava} and the given specification of the bytecode
   42.65 -  verifier are type-safe, and that the lightweight bytecode verifier
   42.66 -  is functionally equivalent to the bytecode verifier specification.
   42.67 -  See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
   42.68 -\end{abstract}
   42.69  
   42.70  \tableofcontents
   42.71  \parindent 0pt \parskip 0.5ex
   42.72  
   42.73 +\input{introduction.tex}
   42.74 +
   42.75 +\section*{Theory Dependencies}
   42.76 +
   42.77 +Figure \ref{theory-deps} shows the dependencies between 
   42.78 +the Isabelle theories in the following sections.
   42.79 +
   42.80 +\begin{figure}
   42.81  \begin{center}
   42.82    \includegraphics[scale=0.4]{session_graph}
   42.83  \end{center}
   42.84 +\caption{Theory Dependency Graph\label{theory-deps}}
   42.85 +\end{figure}
   42.86  
   42.87  \newpage
   42.88  \input{session}