1\chapter{Preface}
2
3\section{Introduction}
4\label{sec:introduction}
5
6This document contains the automatically generated listings of the
7Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard,
8dedicated to the study of the interaction of the source language, byte
9code, the byte code verifier and the compiler. In order to make the
10Isabelle sources more accessible, this introduction provides a brief
11survey of the main concepts of \mJava.
12
13The \mJava{} \textbf{source language} (see \charef{cha:j})
14only comprises a part of the original JavaCard language. It models
15features such as:
16\begin{itemize}
17\item The basic ``primitive types'' of Java 
18\item Object orientation, in particular classes, and relevant
19  relations on classes (subclass, widening)
20
21\item Methods and method signatures
22\item Inheritance and overriding of methods, dynamic binding
23
24\item Representatives of ``relevant'' expressions and statements 
25\item Generation and propagation of system exceptions
26\end{itemize}
27
28However, the following features are missing in \mJava{} wrt.{} JavaCard:
29\begin{itemize}
30\item Some primitive types (\texttt{byte, short})
31\item Interfaces and related concepts, arrays
32\item Most numeric operations, syntactic variants of statements
33  (\texttt{do}-loop, \texttt{for}-loop)
34\item Complex block structure, method bodies with multiple returns
35\item Abrupt termination (\texttt{break, continue})
36\item Class and method modifiers (such as \texttt{static} and
37  \texttt{public/private} access modifiers)
38\item User-defined exception classes and an explicit
39  \texttt{throw}-statement. Exceptions cannot be caught.
40\item A ``definite assignment'' check
41\end{itemize}
42In addition, features are missing that are not part of the JavaCard
43language, such as multithreading and garbage collection. No attempt
44has been made to model peculiarities of JavaCard such as the applet
45firewall or the transaction mechanism.
46
47For a more complete Isabelle model of JavaCard, the reader should
48consult the Bali formalization
49(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
50models most of the source language features of JavaCard, however without
51describing the bytecode level.
52
53The central topics of the source language formalization are:
54\begin{itemize}
55\item Description of the structure of the ``runtime environment'', in
56  particular structure of classes and the program state
57\item Definition of syntax, typing rules and operational semantics of
58  statements and expressions
59\item Definition of ``conformity'' (characterizing type safety) and a
60  type safety proof
61\end{itemize}
62
63
64The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm})
65corresponds rather directly to the source level, in the sense that the
66same data types are supported and bytecode instructions required for
67emulating the source level operations are provided. Again, only one
68representative of different variants of instructions has been
69selected; for example, there is only one comparison operator.  The
70formalization of the bytecode level is purely descriptive (``no
71theorems'') and rather brief as compared to the source level; all
72questions related to type systems for and type correctness of bytecode
73are dealt with in chapter on bytecode verification.
74
75The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is
76dealt with in several stages:
77\begin{itemize}
78\item First, the notion of ``method type'' is introduced, which
79  corresponds to the notion of ``type'' on the source level.
80\item Well-typedness of instructions wrt. a method type is defined
81  (see \secref{sec:BVSpec}). Roughly speaking, determining
82  well-typedness is \emph{type checking}.
83\item It is shown that bytecode that is well-typed in this sense can
84  be safely executed -- a type soundness proof on the bytecode level
85  (\secref{sec:BVSpecTypeSafe}). 
86\item Given raw bytecode, one of the purposes of bytecode verification
87  is to determine a method type that is well-typed according to the
88  above definition. Roughly speaking, this is \emph{type inference}.
89  The Isabelle formalization presents bytecode verification as an
90  instance of an abstract dataflow algorithm (Kildall's algorithm, see
91  \secrefs{sec:Kildall} to \ref{sec:JVM}).
92%\item For \emph{lightweight bytecode verification}, type checking of
93%  bytecode can be reduced to method types with small size. 
94\end{itemize}
95
96Bytecode verification in \mJava{} so far takes into account:
97\begin{itemize}
98\item Operations and branching instructions
99\item Exceptions
100\end{itemize}
101Initialization during object creation is not accounted for in the
102present document 
103(see the formalization in
104\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
105neither is the \texttt{jsr} instruction.
106
107
108%%% Local Variables:
109%%% mode: latex
110%%% TeX-master: "root"
111%%% End:
112