author oheimb
Wed, 08 Aug 2001 14:12:36 +0200
changeset 11477 4d042d3f957d
parent 11376 bf98ad1c22c6
child 11560 46d0bde121ab
permissions -rw-r--r--
changed to full expressions with side effects




%subsection instead of section to make the toc readable

%remove spaces from the isabelle environment (trivlist makes them too large)

\newcommand{\nJava}{\it NanoJava}

%remove clutter from the toc


\author{David von Oheimb \\ Tobias Nipkow}

  These theories define {\nJava}, a very small fragment of the programming 
  language Java (with essentially just classes) derived from the one given 
  in \cite{NipkowOP00}.
  For {\nJava}, an operational semantics is given as well as a Hoare logic,
  which is proved both sound and (relatively) complete. 
  The Hoare logic supports side-effecting expressions and
  implements a new approach for handling auxiliary variables.
  A more complex Hoare logic covering a much larger subset of Java is described
  in \cite{DvO-CPE01}.\\
See also the homepage of project Bali at \url{}.

\parindent 0pt \parskip 0.5ex