%%
%%
\documentclass{entcs} \usepackage{entcsmacro}
% \documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{url}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2


\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\def\lastname{Dawson}
\begin{frontmatter}

\title{Formalising General Correctness}
\author{Jeremy E. Dawson \thanksref{arclg}\thanksref{jedemail}}
\address{NICTA, RSISE, \\
Australian National University,
Canberra ACT 0200, Australia}
\thanks[arclg]{Supported by an Australian Research Council Large Grant}
\thanks[jedemail]{\texttt{jeremy@csl.anu.edu.au},
\url{http://csl.anu.edu.au/~jeremy/} }
\begin{abstract}
We consider the abstract command language of Dunne, 
and his account of general correctness. 
We provide an operational interpretation of his abstract commands,
and use the automated theorem proving system Isabelle to prove that 
this operational interpretation leads to Dunne's semantics.
We consider the difficulties in precisely formalising 
some formulae found in the literature.
\\[1ex]
Keywords: general correctness, abstract commands.
\end{abstract}
\end{frontmatter}


\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
% \newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}


\sloppy 

%\newpage

%% Here begins the main text

\newcommand\file{}

\newcommand\hinput[1]{\renewcommand\file{#1.tex}
  \markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
  \input{#1}}

\input{defs}
\input{intro}
\input{mng}
\input{frames}
\input{concl}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \newpage
\input{bib}

\end{document}