author Fabian Huch <>
Thu, 29 Sep 2022 14:15:01 +0200
changeset 76223 be91db94e526
parent 73404 299f6a8faccc
permissions -rw-r--r--
amend jenkins ci build;




%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{}
and the conference version of this document \cite{NanoJava}.

\parindent 0pt \parskip 0.5ex