1 |
1 %\documentclass[11pt,a4paper]{article} |
2 \documentclass[11pt,a4paper]{article} |
2 \documentclass[11pt,a4paper]{book} |
3 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup} |
3 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup} |
4 |
4 |
5 \urlstyle{rm} |
5 \urlstyle{rm} |
6 \pagestyle{myheadings} |
6 \pagestyle{myheadings} |
7 |
7 |
|
8 %make a bit more space |
8 \addtolength{\hoffset}{-1,5cm} |
9 \addtolength{\hoffset}{-1,5cm} |
9 \addtolength{\textwidth}{4cm} |
10 \addtolength{\textwidth}{4cm} |
10 \addtolength{\voffset}{-2cm} |
11 \addtolength{\voffset}{-2cm} |
11 \addtolength{\textheight}{4cm} |
12 \addtolength{\textheight}{4cm} |
12 |
13 |
13 %subsection instead of section to make the toc readable |
14 %subsection instead of section to make the toc readable |
|
15 \newcommand{\isaheader}[1] |
|
16 {\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
14 \renewcommand{\thesubsection}{\arabic{subsection}} |
17 \renewcommand{\thesubsection}{\arabic{subsection}} |
15 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
18 \renewcommand{\isamarkupheader}[1]{#1} |
16 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}} |
19 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}} |
|
20 \renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}} |
17 |
21 |
18 %remove spaces from the isabelle environment (trivlist makes them too large) |
22 %remove spaces from the isabelle environment (trivlist makes them too large) |
19 \renewenvironment{isabelle} |
23 %\renewenvironment{isabelle} |
20 {\begin{isabellebody}} |
24 %{\begin{isabellebody}} |
21 {\end{isabellebody}} |
25 %{\end{isabellebody}} |
|
26 |
22 |
27 |
23 \newcommand{\mJava}{$\mu$Java} |
28 \newcommand{\mJava}{$\mu$Java} |
|
29 \newcommand{\secref}[1]{Section~\ref{#1}} |
|
30 \newcommand{\secrefs}[1]{Sections~\ref{#1}} |
|
31 \newcommand{\charef}[1]{Chapter~\ref{#1}} |
|
32 \newcommand{\charefs}[1]{Chapters~\ref{#1}} |
|
33 |
24 |
34 |
25 %remove clutter from the toc |
35 %remove clutter from the toc |
26 \setcounter{secnumdepth}{3} |
36 \setcounter{secnumdepth}{3} |
27 \setcounter{tocdepth}{2} |
37 \setcounter{tocdepth}{2} |
28 |
38 |
29 \begin{document} |
39 \begin{document} |
30 |
40 |
31 \title{\mJava} |
41 \title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\ |
32 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
42 % {\large -- VerifiCard Project Deliverables -- } |
|
43 } |
|
44 \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and |
|
45 Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker} |
33 \maketitle |
46 \maketitle |
34 |
47 |
35 \begin{abstract}\noindent |
|
36 This formal development defines {\mJava}, a small fragment of the |
|
37 programming language Java (with essentially just classes), together with a |
|
38 corresponding virtual machine, a specification of its bytecode verifier |
|
39 and a lightweight bytecode verifier. |
|
40 It is shown that {\mJava} and the given specification of the bytecode |
|
41 verifier are type-safe, and that the lightweight bytecode verifier |
|
42 is functionally equivalent to the bytecode verifier specification. |
|
43 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}. |
|
44 \end{abstract} |
|
45 |
48 |
46 \tableofcontents |
49 \tableofcontents |
47 \parindent 0pt \parskip 0.5ex |
50 \parindent 0pt \parskip 0.5ex |
48 |
51 |
|
52 \input{introduction.tex} |
|
53 |
|
54 \section*{Theory Dependencies} |
|
55 |
|
56 Figure \ref{theory-deps} shows the dependencies between |
|
57 the Isabelle theories in the following sections. |
|
58 |
|
59 \begin{figure} |
49 \begin{center} |
60 \begin{center} |
50 \includegraphics[scale=0.4]{session_graph} |
61 \includegraphics[scale=0.4]{session_graph} |
51 \end{center} |
62 \end{center} |
|
63 \caption{Theory Dependency Graph\label{theory-deps}} |
|
64 \end{figure} |
52 |
65 |
53 \newpage |
66 \newpage |
54 \input{session} |
67 \input{session} |
55 |
68 |
56 \newpage |
69 \newpage |