src/HOL/NanoJava/document/root.tex
 changeset 11477 4d042d3f957d parent 11376 bf98ad1c22c6 child 11560 46d0bde121ab
equal inserted replaced
11476:06c1998340a8 11477:4d042d3f957d
    34 \begin{abstract}\noindent
    34 \begin{abstract}\noindent
    35   These theories define {\nJava}, a very small fragment of the programming
    35   These theories define {\nJava}, a very small fragment of the programming
    36   language Java (with essentially just classes) derived from the one given
    36   language Java (with essentially just classes) derived from the one given
    37   in \cite{NipkowOP00}.
    37   in \cite{NipkowOP00}.
    38   For {\nJava}, an operational semantics is given as well as a Hoare logic,
    38   For {\nJava}, an operational semantics is given as well as a Hoare logic,
    39   which is proved both sound and (relatively) complete. The Hoare logic
    39   which is proved both sound and (relatively) complete.

    40   The Hoare logic supports side-effecting expressions and
    40   implements a new approach for handling auxiliary variables.
    41   implements a new approach for handling auxiliary variables.
    41   A more complex Hoare logic covering a much larger subset of Java is described
    42   A more complex Hoare logic covering a much larger subset of Java is described
    42   in \cite{DvO-CPE01}.\\
    43   in \cite{DvO-CPE01}.\\
    43 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
    44 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
    44 \end{abstract}
    45 \end{abstract}