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