%remove spaces from the isabelle environment (trivlist makes them too large) \renewenvironment{isabelle}
{\begin{isabellebody}}
{\end{isabellebody}}
\newcommand{\nJava}{\it NanoJava}
%remove clutter from the toc \setcounter{secnumdepth}{3} \setcounter{tocdepth}{2}
\begin{document}
\title{\nJava} \author{David von Oheimb \\ Tobias Nipkow} \maketitle
\begin{abstract}\noindent
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{https://isabelle.in.tum.de/Bali/}
and the conference version of this document \cite{NanoJava}. \end{abstract}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
