src/HOL/MicroJava/document/root.tex
author kleing
Thu, 21 Sep 2000 12:13:36 +0200
changeset 10044 07218d743c62
parent 10023 1b8b8ddedea7
child 11075 b996b1857028
permissions -rw-r--r--
tuned, added lightweight BV to abstract, added Bali link
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
     1
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
9980
5eec17e4e95e added latexsym (no longer loaded by isabellesym);
wenzelm
parents: 9919
diff changeset
     3
\usepackage{latexsym,isabelle,isabellesym,pdfsetup}
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
     4
10023
1b8b8ddedea7 *** empty log message ***
wenzelm
parents: 9987
diff changeset
     5
\urlstyle{rm}
9919
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
     6
\pagestyle{myheadings}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
     7
9755
kleing
parents: 8193
diff changeset
     8
\addtolength{\hoffset}{-1,5cm}
kleing
parents: 8193
diff changeset
     9
\addtolength{\textwidth}{4cm}
kleing
parents: 8193
diff changeset
    10
\addtolength{\voffset}{-2cm}
kleing
parents: 8193
diff changeset
    11
\addtolength{\textheight}{4cm}
kleing
parents: 8193
diff changeset
    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
f96d8e02ff1d added mJava macro
oheimb
parents: 9980
diff changeset
    22
\newcommand{\mJava}{$\mu$Java}
9820
2aa2871d0dec improved section markup;
wenzelm
parents: 9764
diff changeset
    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
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
    28
\begin{document}
9820
2aa2871d0dec improved section markup;
wenzelm
parents: 9764
diff changeset
    29
9985
f96d8e02ff1d added mJava macro
oheimb
parents: 9980
diff changeset
    30
\title{\mJava}
9919
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    31
\author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    32
\maketitle
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    33
10044
07218d743c62 tuned, added lightweight BV to abstract, added Bali link
kleing
parents: 10023
diff changeset
    34
\begin{abstract}\noindent
9987
ed35be80285d added mJava macro
oheimb
parents: 9985
diff changeset
    35
  This formal development defines {\mJava}, a small fragment of the
9985
f96d8e02ff1d added mJava macro
oheimb
parents: 9980
diff changeset
    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
ed35be80285d added mJava macro
oheimb
parents: 9985
diff changeset
    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
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    43
\end{abstract}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    44
9755
kleing
parents: 8193
diff changeset
    45
\tableofcontents
9820
2aa2871d0dec improved section markup;
wenzelm
parents: 9764
diff changeset
    46
\parindent 0pt \parskip 0.5ex
9919
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    47
9755
kleing
parents: 8193
diff changeset
    48
\newpage
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
    49
\input{session}
9820
2aa2871d0dec improved section markup;
wenzelm
parents: 9764
diff changeset
    50
10044
07218d743c62 tuned, added lightweight BV to abstract, added Bali link
kleing
parents: 10023
diff changeset
    51
\newpage
9919
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    52
\nocite{*}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    53
\bibliographystyle{abbrv}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    54
\bibliography{root}
3cf12ab0b8ac added title, abstract, bibliography;
wenzelm
parents: 9820
diff changeset
    55
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents:
diff changeset
    56
\end{document}