src/HOL/MicroJava/document/introduction.tex
 author haftmann Fri Jun 11 17:14:02 2010 +0200 (2010-06-11) changeset 37407 61dd8c145da7 parent 12914 71015f46b3c1 child 68649 f849fc1cb65e permissions -rwxr-xr-x
declare lex_prod_def [code del]
     1 \chapter{Preface}

     2

     3 \section{Introduction}

     4 \label{sec:introduction}

     5

     6 This document contains the automatically generated listings of the

     7 Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard,

     8 dedicated to the study of the interaction of the source language, byte

     9 code, the byte code verifier and the compiler. In order to make the

    10 Isabelle sources more accessible, this introduction provides a brief

    11 survey of the main concepts of \mJava.

    12

    13 The \mJava{} \textbf{source language} (see \charef{cha:j})

    14 only comprises a part of the original JavaCard language. It models

    15 features 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

    28 However, 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}

    42 In addition, features are missing that are not part of the JavaCard

    43 language, such as multithreading and garbage collection. No attempt

    44 has been made to model peculiarities of JavaCard such as the applet

    45 firewall or the transaction mechanism.

    46

    47 For a more complete Isabelle model of JavaCard, the reader should

    48 consult the Bali formalization

    49 (\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which

    50 models most of the source language features of JavaCard, however without

    51 describing the bytecode level.

    52

    53 The 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

    64 The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm})

    65 corresponds rather directly to the source level, in the sense that the

    66 same data types are supported and bytecode instructions required for

    67 emulating the source level operations are provided. Again, only one

    68 representative of different variants of instructions has been

    69 selected; for example, there is only one comparison operator.  The

    70 formalization of the bytecode level is purely descriptive (no

    71 theorems'') and rather brief as compared to the source level; all

    72 questions related to type systems for and type correctness of bytecode

    73 are dealt with in chapter on bytecode verification.

    74

    75 The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is

    76 dealt 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

    96 Bytecode verification in \mJava{} so far takes into account:

    97 \begin{itemize}

    98 \item Operations and branching instructions

    99 \item Exceptions

   100 \end{itemize}

   101 Initialization during object creation is not accounted for in the

   102 present document

   103 (see the formalization in

   104 \url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),

   105 neither is the \texttt{jsr} instruction.

   106

   107

   108 %%% Local Variables:

   109 %%% mode: latex

   110 %%% TeX-master: "root"

   111 %%% End: