1%
2% Copyright 2014, NICTA
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(NICTA_GPL)
9%
10
11\documentclass[11pt,a4paper]{scrreprt}
12
13\newif \ifDraft         \Draftfalse
14
15% These old font commands have been removed from newer versions of
16% the scrreprt document class, but isabelle.sty still uses them.
17\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
18\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
19\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
20\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
21\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
22\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
23\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
24
25\usepackage{isabelle,isabellesym}
26
27% further packages required for unusual symbols (see also
28% isabellesym.sty), use only when needed
29
30%\usepackage{amssymb}
31  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
32  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
33  %\<triangleq>, \<yen>, \<lozenge>
34
35\usepackage[english]{babel}
36  %option greek for \<euro>
37  %option english (default language) for \<guillemotleft>, \<guillemotright>
38
39%\usepackage[only,bigsqcap]{stmaryrd}
40  %for \<Sqinter>
41
42%\usepackage{eufrak}
43  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
44
45%\usepackage{textcomp}
46  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
47  %\<currency>
48
49
50% Extra CAmkES bits.
51\usepackage{graphicx}
52\usepackage{enumerate}
53
54% From ERTOS setup
55\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth}
56\usepackage{times,cite,url,fancyhdr,microtype,color,geometry}
57
58\renewcommand{\ttdefault}{cmtt}        % CM rather than courier for \tt
59
60\usepackage{xspace}
61\usepackage{listings}
62\newcommand{\camkeslisting}[1]{{\lstset{basicstyle=\small\ttfamily,keywordstyle=\bf,morekeywords={assembly,component,composition,connection,control,consumes,dataport,emits,event,from,in,inout,int,out,procedure,provides,smallstring,to,uses}}\lstinputlisting{#1}}}
63
64
65\ifDraft
66\usepackage{draftcopy}
67\newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
68\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
69\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}}
70\date{\small\today}
71\else
72\newcommand{\Comment}[1]{\relax}
73\newcommand{\FIXME}[1]{\relax}
74\newcommand{\todo}[1]{\relax}
75\date{}
76\fi
77
78
79% From camkes manual
80\newcommand{\selfour}{seL4\xspace}
81\newcommand{\Selfour}{SeL4\xspace}
82\newcommand{\camkes}{CAmkES\xspace}
83
84\newcommand{\code}[1]{\texttt{#1}}
85
86
87\newcommand{\titl}{CAmkES Formalisation of a Component Platform}
88\newcommand{\authors}{Matthew Fernandez, Gerwin Klein, Ihor Kuz, Toby Murray}
89
90\definecolor{lcol}{rgb}{0,0,0.5}
91\usepackage[bookmarks,hyperindex,pdftex,
92            colorlinks=true,linkcolor=lcol,citecolor=lcol,
93            filecolor=lcol,urlcolor=lcol,
94            pdfauthor={\authors},
95            pdftitle={\titl},
96            plainpages=false]{hyperref}
97
98
99\addto\extrasenglish{%
100\renewcommand{\chapterautorefname}{Chapter}
101\renewcommand{\sectionautorefname}{Section}
102\renewcommand{\subsectionautorefname}{Section}
103\renewcommand{\subsubsectionautorefname}{Section}
104\renewcommand{\appendixautorefname}{Appendix}
105\renewcommand{\Hfootnoteautorefname}{Footnote}
106}
107
108% urls in roman style
109\urlstyle{rm}
110
111\lstset{basicstyle=\small\tt}
112
113% isabelle style
114\isabellestyle{tt}
115
116% for uniform isabelle font size
117\renewcommand{\isastyle}{\isastyleminor}
118
119% Abstract various things that might change.
120\newcommand{\ccode}[1]{\texttt{#1}}
121\newcommand{\isabelletype}[1]{\emph{#1}}
122\newcommand{\isabelleterm}[1]{\emph{#1}}
123
124\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
125\renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
126\renewcommand{\isamarkupsection}[1]{\section{#1}}
127\renewcommand{\isamarkupsubsection}[1]{\section{#1}}
128\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}}
129
130\newcommand{\nictafundingacknowledgement}{%
131NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. NICTA is also funded and supported by the Australian Capital Territory, the New South Wales, Queensland and Victorian Governments, the Australian National University, the University of New South Wales, the University of Melbourne, the University of Queensland, the University of Sydney, Griffith University, Queensland University of Technology, Monash University and other university partners.}
132
133
134\newcommand{\trdisclaimer}{%
135This material is based on research sponsored by Air Force Research Laboratory
136and the Defense Advanced Research Projects Agency (DARPA) under agreement number
137FA8750-12-9-0179. The U.S. Government is authorized to reproduce and distribute
138reprints for Governmental purposes notwithstanding any copyright notation
139thereon.
140
141The views and conclusions contained herein are those of the authors and should
142not be interpreted as necessarily representing the official policies or
143endorsements, either expressed or implied, of Air Force Research Laboratory,
144the Defense Advanced Research Projects Agency or the U.S.Government.}
145
146\newcommand{\smalldisclaimer}{}
147\newcommand{\bigdisclaimer}{%
148\nictafundingacknowledgement
149
150\vspace{2ex}
151\trdisclaimer}
152
153
154\newcommand{\pgstyle}{%
155\fancyhf{}%
156\renewcommand{\headrulewidth}{0pt}%
157\fancyfoot[C]{}%
158\fancyfoot[L]{\smalldisclaimer}%
159\fancyfoot[R]{\sl\thepage}}
160
161\fancypagestyle{plain}{\pgstyle}
162
163
164\begin{document}
165
166\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex
167
168%--------- title page
169\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm}
170
171\begin{center}
172 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo}
173\end{center}
174
175\vspace{14ex}
176\textsf{\huge \titl}
177
178%\vspace{2ex}
179%\textsf{\huge \subtitl}
180
181\vspace{4ex}
182\rule{0.85\textwidth}{5pt}
183\vspace{4ex}
184
185{\large \authors
186
187\vspace{2ex}
188April 2014}
189
190\vfill
191{\small
192\bigdisclaimer
193}
194
195\thispagestyle{empty}
196\newpage
197%--------- end title page
198
199\tableofcontents
200
201\input{intro}
202
203% generated text of all theories
204\input{session}
205
206% This document has no references, but Isabelle unconditionally calls bibtex,
207% foolishly expecting me to back up what I'm saying. Fake a bibliography to
208% pacify it.
209\renewcommand{\refname}{}
210\nocite{*}
211\bibliographystyle{abbrv}
212
213\end{document}
214