src/HOL/NanoJava/document/root.tex
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 11855 bdae1f29f35d child 68649 f849fc1cb65e permissions -rw-r--r--
tuned proofs;
     1 \documentclass[11pt,a4paper]{article}

     2 \usepackage{graphicx,latexsym,isabelle,isabellesym,latexsym,pdfsetup}

     3

     4 \urlstyle{tt}

     5 \pagestyle{myheadings}

     6

     7 \addtolength{\hoffset}{-1,5cm}

     8 \addtolength{\textwidth}{4cm}

     9 \addtolength{\voffset}{-2cm}

    10 \addtolength{\textheight}{4cm}

    11

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

    13 \renewenvironment{isabelle}

    14 {\begin{isabellebody}}

    15 {\end{isabellebody}}

    16

    17 \newcommand{\nJava}{\it NanoJava}

    18

    19 %remove clutter from the toc

    20 \setcounter{secnumdepth}{3}

    21 \setcounter{tocdepth}{2}

    22

    23 \begin{document}

    24

    25 \title{\nJava}

    26 \author{David von Oheimb \\ Tobias Nipkow}

    27 \maketitle

    28

    29 \begin{abstract}\noindent

    30   These theories define {\nJava}, a very small fragment of the programming

    31   language Java (with essentially just classes) derived from the one given

    32   in \cite{NipkowOP00}.

    33   For {\nJava}, an operational semantics is given as well as a Hoare logic,

    34   which is proved both sound and (relatively) complete.

    35   The Hoare logic supports side-effecting expressions and

    36   implements a new approach for handling auxiliary variables.

    37   A more complex Hoare logic covering a much larger subset of Java is described

    38   in \cite{DvO-CPE01}.\\

    39 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}

    40 and the conference version of this document \cite{NanoJava}.

    41 \end{abstract}

    42

    43 \tableofcontents

    44 \parindent 0pt \parskip 0.5ex

    45

    46 \begin{center}

    47   \includegraphics[scale=0.7]{session_graph}

    48 \end{center}

    49

    50 \newpage

    51 \input{session}

    52

    53 \newpage

    54 \nocite{*}

    55 \bibliographystyle{abbrv}

    56 \bibliography{root}

    57

    58 \end{document}