|
1 \documentclass[11pt,a4paper]{article} |
|
2 \usepackage{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 %subsection instead of section to make the toc readable |
|
13 \renewcommand{\thesubsection}{\arabic{subsection}} |
|
14 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
|
15 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}} |
|
16 |
|
17 %remove spaces from the isabelle environment (trivlist makes them too large) |
|
18 \renewenvironment{isabelle} |
|
19 {\begin{isabellebody}} |
|
20 {\end{isabellebody}} |
|
21 |
|
22 \newcommand{\nJava}{\it NanoJava} |
|
23 |
|
24 %remove clutter from the toc |
|
25 \setcounter{secnumdepth}{3} |
|
26 \setcounter{tocdepth}{2} |
|
27 |
|
28 \begin{document} |
|
29 |
|
30 \title{\nJava} |
|
31 \author{David von Oheimb \\ Tobias Nipkow} |
|
32 \maketitle |
|
33 |
|
34 \begin{abstract}\noindent |
|
35 These theories define {\nJava}, a very small fragment of the programming |
|
36 language Java (with essentially just classes) derived from the one given |
|
37 in \cite{NipkowOP00}. |
|
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 |
|
40 implements a new approach for handling auxiliary variables. |
|
41 A more complex Hoare logic covering a much larger subset of Java is described |
|
42 in \cite{DvO-CPE01}.\\ |
|
43 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}. |
|
44 \end{abstract} |
|
45 |
|
46 \tableofcontents |
|
47 \parindent 0pt \parskip 0.5ex |
|
48 |
|
49 \newpage |
|
50 \input{session} |
|
51 |
|
52 \newpage |
|
53 \nocite{*} |
|
54 \bibliographystyle{abbrv} |
|
55 \bibliography{root} |
|
56 |
|
57 \end{document} |