src/HOL/MicroJava/document/introduction.tex
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 12914 71015f46b3c1
child 68649 f849fc1cb65e
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     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: