8 \addtolength{\hoffset}{-1,5cm} |
8 \addtolength{\hoffset}{-1,5cm} |
9 \addtolength{\textwidth}{4cm} |
9 \addtolength{\textwidth}{4cm} |
10 \addtolength{\voffset}{-2cm} |
10 \addtolength{\voffset}{-2cm} |
11 \addtolength{\textheight}{4cm} |
11 \addtolength{\textheight}{4cm} |
12 |
12 |
13 \renewcommand{\thesection}{\arabic{section}} |
13 %subsection instead of section to make the toc readable |
14 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}} |
14 \renewcommand{\thesubsection}{\arabic{subsection}} |
|
15 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
|
16 |
|
17 %remove spaces from the isabelle environment (trivlist makes them too large) |
|
18 \renewenvironment{isabelle} |
|
19 {\begin{isabellebody}} |
|
20 {\end{isabellebody}} |
|
21 |
15 \newcommand{\mJava}{$\mu$Java} |
22 \newcommand{\mJava}{$\mu$Java} |
|
23 |
|
24 %remove clutter from the toc |
|
25 \setcounter{secnumdepth}{2} |
|
26 \setcounter{tocdepth}{2} |
16 |
27 |
17 \begin{document} |
28 \begin{document} |
18 |
29 |
19 \title{\mJava} |
30 \title{\mJava} |
20 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
31 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
21 \maketitle |
32 \maketitle |
22 |
33 |
23 \begin{abstract} |
34 \begin{abstract}\noindent |
24 This formal development defines {\mJava}, a small fragment of the |
35 This formal development defines {\mJava}, a small fragment of the |
25 programming language Java (with essentially just classes), together with a |
36 programming language Java (with essentially just classes), together with a |
26 corresponding virtual machine and a specification of its bytecode verifier. |
37 corresponding virtual machine, a specification of its bytecode verifier |
|
38 and a lightweight bytecode verifier. |
27 It is shown that {\mJava} and the given specification of the bytecode |
39 It is shown that {\mJava} and the given specification of the bytecode |
28 verifier are type-safe. |
40 verifier are type-safe, and that the lightweight bytecode verifier |
|
41 is functionally equivalent to the bytecode verifier specification. |
|
42 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}. |
29 \end{abstract} |
43 \end{abstract} |
30 |
44 |
31 \tableofcontents |
45 \tableofcontents |
32 \parindent 0pt \parskip 0.5ex |
46 \parindent 0pt \parskip 0.5ex |
33 |
47 |
34 \newpage |
48 \newpage |
35 \input{session} |
49 \input{session} |
36 |
50 |
|
51 \newpage |
37 \nocite{*} |
52 \nocite{*} |
38 \bibliographystyle{abbrv} |
53 \bibliographystyle{abbrv} |
39 \bibliography{root} |
54 \bibliography{root} |
40 |
55 |
41 \end{document} |
56 \end{document} |