%----------------------------------------------------------------------
%   Filename:   cav.tex
%----------------------------------------------------------------------
%   Last modified on Thu Oct  1 19:07:04 1992 by lamport
%        modified on Wed Jan 29 15:52 1992 by urban  
%----------------------------------------------------------------------
\documentstyle[11pt]{article}



\addtolength{\textheight}{1.5\baselineskip}
\addtolength{\topmargin}{-.5\baselineskip}

\title{\vspace*{-\baselineskip} %%% formatting hack
\bf Mechanical Verification\\ of Concurrent Systems with TLA}
\author{Urban Engberg \\ {\small Aarhus University}
\and Peter Gr\o{}nning
 \\ {\small Technical University of Denmark} \and 
    Leslie Lamport \\ {\small Digital Equipment Corporation}\\[-.2em]
    {\small Systems Research Center}}
\date{}
\renewcommand{\topfraction}{1}
\renewcommand{\bottomfraction}{1}
\renewcommand{\textfraction}{0}

\newcommand{\kwd}[1]{{\bf #1}}

\newcommand{\xand}{$\wedge$ }
\newcommand{\xor}{$\vee$ }
\newcommand{\ximplies}{$\Rightarrow$ }
\newcommand{\xbox}{$\Box$}
\newcommand{\xexists}{$\exists$}
\newcommand{\xforall}{$\forall$}
\newcommand{\xlambda}{$\lambda$}
\newcommand{\xmaps}{$\rightarrow$\ }
\newcommand{\xneq}{$\neq$ }
\newcommand{\xless}{$<$ }
\newcommand{\xleq}{$\leq$ }
\newcommand{\xin}{$\in$ }
\newcommand{\xassignin}{$:\in$ }
\newcommand{\xvar}[1]{{\it #1\/}}
\newcommand{\xact}[1]{${\cal #1\/}$}
\newcommand{\xdefeq}{$\stackrel{\scriptscriptstyle\Delta}{=}$ }
\newcommand{\xinfty}{$\infty$}
\newcommand{\xsuf}[1]{$_{#1}$}
\newcommand{\xsfsuf}[1]{$_{#1}$}

%\newcommand{\pand}{\verb:/\:}
%\newcommand{\por}{\verb:\/:}
\newcommand{\pimplies}{{\tt=>}}
\newcommand{\pbox}{{\tt[]}}
\newcommand{\plbrack}{{\tt[}}
\newcommand{\prbrack}{{\tt]}}
\newcommand{\plpar}{{\tt(}}
\newcommand{\prpar}{{\tt)}}
\newcommand{\plcrl}{{\tt \{}}
\newcommand{\prcrl}{{\tt \}}}
\newcommand{\pstar}{{\tt*}}
\newcommand{\pcolon}{{\tt:}}
\newcommand{\pexists}{\kwd{Exists}}
\newcommand{\pforall}{\kwd{Forall}}
\newcommand{\plambda}{\kwd{Lambda}}
\newcommand{\pmaps}{{\tt->}}
%\newcommand{\pneq}{\verb:~=:}
\newcommand{\pless}{{\tt<}}
\newcommand{\pleq}{{\tt>}}
\newcommand{\pin}{\kwd{in}}
\newcommand{\passignin}{{\tt:}\kwd{in}}
\newcommand{\passigneq}{{\tt:=}}
\newcommand{\pvar}[1]{{\it #1\/}}
\newcommand{\pact}[1]{{\it #1\/}}
\newcommand{\pdef}[1]{{\it #1\/}}
\newcommand{\pdefeq}{{\tt==}}
\newcommand{\pinfty}{\xvar{infty}}
\newcommand{\psuf}[1]{#1}
\newcommand{\psfsuf}[1]{\_#1}

%\newcommand{\lpdash}{\vdash_{\hspace{-.4em}\scriptscriptstyle \rm LP}}
%\newcommand{\lpimplies}{\Rightarrow}
%\newcommand{\lpand}{\ \&\ }
%\newcommand{\lpor}{\mid}

%\newcommand{\timplies}{\stackrel{\scriptscriptstyle \rm tla}{\Rightarrow}}
%\newcommand{\tand}{\stackrel{\scriptscriptstyle \rm tla}{\wedge}}
%\newcommand{\tor}{\stackrel{\scriptscriptstyle \rm tla}{\vee}}

\newcommand{\nimplies}{\Rightarrow}

\newcommand{\linespace}{\\[-1.5ex]}
\newcommand{\smallspace}{\\[-2.5ex]}

\newenvironment{tlafigure}{
\begin{tabbing}
  mm\=rullepoelse \= \pdefeq\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \kill
  }{
\end{tabbing}
}

\newenvironment{tlaquote}{
\begin{quote}
  \begin{tabbing}
    mm\=rullepoelse \= \pdefeq\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \pimplies\ \= \kill
    }{
  \end{tabbing}
\end{quote}
}

\newenvironment{tlaproof}{
%\begin{footnotesize}
\begin{scriptsize}
  \begin{tabbing}

    mm\=mm\=mm\=mm\=mm\=mm\=mm\=mm\=mm\=\+\kill
    }{
  \end{tabbing}
\end{scriptsize}
%\end{footnotesize}
}

%% \ruler draws an em ruler 
\def\emruler{\begin{picture}(0,0)
\put(0,0){\line(0,1){1}}
\put(1,0){\line(0,1){.5}}
\put(2,0){\line(0,1){.5}}
\put(3,0){\line(0,1){.5}}
\put(4,0){\line(0,1){.5}}
\put(5,0){\line(0,1){.75}}
\put(6,0){\line(0,1){.5}}
\put(7,0){\line(0,1){.5}}
\put(8,0){\line(0,1){.5}}
\put(9,0){\line(0,1){.5}}
\end{picture}}
\def\ruler{\setlength{\unitlength}{1em}%
\begin{picture}(0,0)
\put(0,0){\emruler}
\put(10,0){\emruler}
\put(20,0){\emruler}
\put(30,0){\emruler}
\put(40,0){\emruler}
\put(50,0){\emruler}
\put(60,0){\emruler}
\put(70,0){\emruler}
\end{picture}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           Definitions for Section 2.                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \nat    == set of natural numbers
% \deq    == equals by def
% \implies == =>
% \WF{x}{A}  
% \dom{f} == domain f
% \replace{f}{s}{v} ==  f[s := v]
% \setreplace{f}{s}{T} == f[s :in T]
% \functions{S}{T}  == [S -> T]
% \interval{a}{b} == [a, b)
% \ifthenelse{a}{b}{c} == if a then b else c

% \vbl{xyz}   == "variable-name" xyz
% \act{N}  ==  Script N 
% \s{n}    == an n-em horizontal space
% \vs{n}   == An n-em vertical space below current line--even in array.
%
% \pf  == Proof:
% \qed == QED:

\newcommand{\nat}{{\it Nat\/}}
\newcommand{\mathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\newcommand{\implies}{\mathrel{\Rightarrow}}
\newcommand{\WF}[2]{\mathdef{{\rm WF}_{#1}(#2)}}
\newcommand{\dom}[1]{\mathdef{{\it dom\/}\,#1}}
\newcommand{\replace}[3]{\mathdef{#1[#2\,:=\,#3]}}
\newcommand{\setreplace}[3]{\mathdef{#1[#2\,:\in\,#3]}}
\newcommand{\functions}[2]{\mathdef{[#1\rightarrow#2]}}
\newcommand{\interval}[2]{\mathdef{[#1,\,#2)}}

\newcommand{\vbl}[1]{{\it #1\/}}
\newcommand{\act}[1]{\mathdef{{\cal #1}}}
\newcommand{\s}[1]{\hspace*{#1em}}
\newcommand{\vs}[1]{\raisebox{-#1em}{\rule{0pt}{.1pt}}}
\newcommand{\ifthenelse}[3]{\mathdef{{\bf if}\s{.5}#1\s{.5}%
         {\bf then}\s{.5}#2\s{.5}{\bf else}\s{.5}#3}}

\newcommand{\pf}{{\bf Proof }}
\newcommand{\qed}{{\bf qed }}


\begin{document}

 \thispagestyle{empty}
 \mbox{}
 \vfill
 \begin{center}
 \LARGE
 \bf Mechanical Verification\\ of Concurrent Systems with TLA
 
 \large
 \vspace{1.5\baselineskip}
 
 \hspace*{-.075\textwidth}
 \begin{minipage}[t]{.45\textwidth}
   \centering
   Urban Engberg \\ {\small Aarhus University}
 \end{minipage}%
~% 
 \begin{minipage}[t]{.45\textwidth}
   \centering
   Peter Gr\o{}nning \\ 
   {\small Technical University of Denmark} 
 \end{minipage}\\[.75\baselineskip]
 
 \begin{minipage}[t]{.75\textwidth}
   \centering
   Leslie Lamport \\ 
   {\small Digital Equipment Corporation}\\[-.2em]
   {\small Systems Research Center}
 \end{minipage}

\vspace{1.5\baselineskip}
14 September 1992 -- version 2

 \end{center}
 

 \vspace{7\baselineskip} 
 
 \noindent
 All but this page 
to appear in {\em Proceedings of the 
 Fourth International Workshop on Computer-Aided Verification\/}
 \vfill \vfill 
 \newpage

\setcounter{page}{1}

\maketitle

\begin{abstract}
We describe an initial version of a system for mechanically checking
the correctness proof of a concurrent system.  Input to the system
consists of the correctness properties, expressed in TLA (the temporal
logic of actions), and their proofs, written in a humanly readable,
hierarchically structured form.  The system uses a mechanical verifier
to check each step of the proof, translating the step's assertion into
a theorem in the verifier's logic and its proof into instructions for
the verifier.  Checking is now done by LP (the Larch Prover),
using two different translations---one for action reasoning and one
for temporal reasoning.  The use of additional mechanical verifiers is
planned.  Our immediate goal is a practical system for mechanically
checking proofs of behavioral properties of a concurrent system; we
assume ordinary properties of the data structures used by the system.
\end{abstract}

\section{Introduction}
TLA, the Temporal Logic of Actions, is a logic for specifying and
reasoning about concurrent systems.  Systems and their properties are
described by logical formulas; the TLA formula $\Pi\implies\Phi$
asserts that the system represented by $\Pi$ satisfies the property, or
implements the system, represented by $\Phi$.  TLA is a linear-time
temporal logic~\cite{lamport:sometime} that can express liveness
(eventuality) as well as safety (invariance) properties.  Although TLA
is a formal logic, the TLA specification of a concurrent system is no
more difficult to write than the system's description in a conventional
programming language.

Since TLA is a formal logic, it allows completely rigorous reasoning.
It is clear that TLA proofs can, in principle, be checked mechanically.
In 1991, we began a one-year effort to determine if mechanical
verification with TLA is practical.  We decided to use the LP
verification system~\cite{garland:overview,garland:guide}, 
initially planning to
write proofs directly in LP\@.  However, we found the LP encoding to be
distracting, making large proofs difficult.  We therefore decided to
write a TLA to LP translator, so specifications, theorems, and proof
steps could be written in TLA\@.  Writing specifications and theorems
directly in TLA avoids the errors that can be introduced when hand
translating what one wants to prove into the language of a verifier.
The translator also allows mechanically checked proofs to have the same
structure as hand proofs, making them easier to write and understand.

Working on the translator has thus far allowed us time to verify only a
few simple examples, including an algorithm to compute a spanning tree
on an arbitrary graph.  Experience with more realistic examples is
needed to determine if mechanical verification of TLA formulas can be a
practical tool for concurrent-system design.  It will never be easy to
write rigorous proofs.  However, we find it very encouraging that
mechanically checkable proofs written in the translator seem to be only
two to three times longer than careful hand proofs.

TLA, its LP encoding, and the translator are described in the following
three sections, using the spanning-tree algorithm as an example.  In
this example, we prove that a system satisfies a property.  An
important feature of TLA is the ability to prove that one system
implements (is a refinement of) another.  However, space does not
permit an example of such a proof.

%\input{sec2}

\section{TLA\label{sec:tla}}

For the purposes of this paper, we can consider TLA to be ordinary
predicate logic, except with two classes of variables called {\em rigid
variables\/} and {\em flexible variables}, extended with the two
operators $'$ (prime) and $\Box$.  Quantification is over rigid
variables only.  (Full TLA also includes quantification over flexible
variables, which serves as a hiding operator.) We often refer to
flexible variables simply as variables.  

The semantics of TLA is based on the concept of a {\em state}, which is
an assignment of values to (flexible) variables.  The meaning of a TLA
formula is a set of {\em behaviors}, where a behavior is a sequence of
states.  The operator $\Box$ is the standard temporal-logic ``always''
operator~\cite{pnueli:temporal}; the prime is a ``next-state''
operator.  The complete semantics of TLA can be found
elsewhere~\cite{lamport:newtla}; here we explain
TLA informally through simple examples.

As a first example, we write a TLA formula specifying a program that
starts with the variable $x$ equal to any natural number, and keeps
incrementing $x$ by 1 forever.  Letting \nat\ denote the set of
natural numbers, the obvious way to express this with the prime
and $\Box$ operators is
\begin{equation} \label{eq:rtla}
  (x\in\nat) \;\land\; \Box(x'=x+1)
\end{equation}
The predicate $x\in\nat$ asserts that the value of $x$ in the initial
state is an element of \nat; the action $x'=x+1$ asserts that the value of
$x$ in the next state is always 1 greater than its value in the current
state, and the temporal formula $\Box(x'=x+1)$ asserts that this is true 
for all steps---that is, for all pairs of successive states.

Formula (\ref{eq:rtla}) asserts that the value of $x$ is incremented in
each step of a behavior.  For reasons explained in
\cite{lamport:what-good}, we want also to allow steps that leave $x$
unchanged.  Letting $[{\cal A}]_{f}$ denote ${\cal A}\lor(f'=f)$, this
is expressed by the TLA formula
\begin{equation} \label{eq:tla1}
    (x\in\nat) \;\land\; \Box[x'=x+1]_{x} \;\land\; \WF{x}{x'=x+1}
\end{equation}
The conjunct $\Box[x'=x+1]_{x}$ asserts that every step of the program
either increments $x$ by 1 or leaves it unchanged.  It allows behaviors
in which $x$ remains unchanged forever.  The conjunct $\WF{x}{x'=x+1}$
expresses the liveness property that infinitely many $x'=x+1$ steps 
(ones that do increment $x$) occur.  The reader is referred to
\cite{lamport:newtla} for an explanation of the {\rm WF} operator
and its definition in terms of $'$ and $\Box$.

In general, the canonical form of a TLA formula describing an algorithm
is
\begin{equation} \label{eq:canonical}
  \vbl{Init} \;\land\;\Box[\act{N}]_{v} \;\land\; F
\end{equation}
where \vbl{Init} is a predicate describing the initial state, \act{N}
is an action describing how the variables may change, $v$ is the tuple
of all program variables, and $F$ is a liveness condition.  The conjunct
$\Box[\act{N}]_{v}$ asserts that every step is either an \act{N}
step or else leaves all variables unchanged (since a tuple is 
unchanged iff every component is unchanged).

Our major example is a simple algorithm that, given a finite connected graph
and a root, constructs a spanning tree.  For each node $n$, the
algorithm computes the distance $d[n]$ from $n$ to the root and, if $n$
is not the root, its father $f[n]$ in the spanning tree.  

When the algorithm is expressed formally, $d$ and $f$ are variables
whose values are functions with domain equal to the set of nodes.
Before describing the algorithm, we introduce some notation for
expressing functions.  The expression 
 \( \lambda x\in S : e(x) \)
denotes a function $f$ whose domain is $S$, such that $f[x]$ equals
$e(x)$ for all $x$ in $S$.  If $f$ is a function, then
\replace{f}{s}{v} is the function that is the same as $f$ except with
$f[s]=v$.  This is defined formally as follows, where \dom{f} denotes
the domain of $f$, and $\,\deq\,$ means {\em equals by definition}.
 \[ \replace{f}{s}{v} \;\;\deq\;\;
    \lambda x\in \dom{f} : \ifthenelse{x=s}{v}{f[x]}
 \]
(Thus, $s\notin\dom{f}$ implies $\replace{f}{s}{v}=f$.)
If $f$ is a function and $T$ a set, then \setreplace{f}{s}{T} is the
set of all functions \replace{f}{s}{v} with $v\in T$.  Finally,
\functions{S}{T} denotes the set of all functions $f$ with domain $S$
such that $f[x]\in T$ for all $x\in S$.  

We now describe the spanning-tree algorithm.  Initially, $d[n]$ equals
0 for the root and equals $\infty$ for all other nodes.  For each node
$n$, there is a process that repeatedly executes {\em improvement
steps} that choose a neighbor $m$ with
$d[m]+1<d[n]$, decrease $d[n]$, and set $f[n]$ to $m$.  The
improvement step could simply decrease $d[n]$ to $d[m]+1$, but for
reasons that are irrelevant to this discussion, we consider a more
general algorithm in which $d[n]$ is set to a nondeterministically
chosen number between its old value and $d[m]$.  The algorithm
terminates when no more improvement steps are possible.

The TLA formula $\Pi$ describing this algorithm is defined in
Figure~\ref{fig:st-alg}, where \vbl{Node} is the set of nodes,
\vbl{Root} is the root, $\vbl{Nbrs}(n)$ is the set of neighbors of node
$n$ in the graph, and \interval{a}{b} is the set of natural numbers $c$
such that $a\leq c<b$.  We adopt the convention that a list bulleted
with $\land$'s denotes the conjunction of the items, and we use
indentation to eliminate parentheses.  We have found this convention
extremely helpful in making large formulas easier to read.

%% \pagebreak %%%

The initial condition is described by the predicate \vbl{Init}.  It
asserts that $d[n]$ has the appropriate value (0 or $\infty$) and that
$f[n]$ is a node, for each $n\in\vbl{Node}$.

Action $\act{N}_{2}(n,m)$ describes an improvement step, in which
$d[n]$ is decreased and $f[n]$ set equal to $m$.  However, it does not
assert that $m$ is a neighbor of $n$.  The action is enabled only if
$d[m]+1 < d[n]$.  (In this formula, $d$ and $f$ are flexible
variables, while $m$ and $n$ are rigid variables.)

Action \act{N} is the disjunction of the actions $\act{N}_{2}(n,m)$ for
every node $n$ and neighbor $m$ of $n$.  It is the next-state relation
of the algorithm, describing how the variables $d$ and $f$ may change.
We define $v$ to be the pair $(d,f)$ of variables, and $\Pi$ to be the
canonical formula describing the algorithm.  The weak fairness
condition \WF{v}{\act{N}} asserts that \act{N} steps are eventually
taken as long as they remain possible---that is, as long as the action
\act{N} remains enabled.  Concurrency is represented by
the nondeterministic interleaving of the different processes'
(atomic) improvement steps.


\begin{figure}[tb]
\[\begin{array}{@{}l@{}} \vs{-1.25}%%% spacing hack
    \vbl{Init} \s{.75}\deq\s{.75} \begin{array}[t]{@{\land\s{.5}}l@{}}
                                    d = \lambda n\in\vbl{Node} : 
                                       \ifthenelse{n=\vbl{Root}}{0}{\infty}
                                   \\
                                    f \in \functions{\vbl{Node}}{\vbl{Node}}
                                  \vs{.75}
                                  \end{array}
   %
   \\
   %
    \act{N}_{2}(n,m) \s{.75}\deq\s{.75}  
                \begin{array}[t]{@{\land\s{.5}}l@{}}
                   d[m] \neq \infty\\
                   d'\in \setreplace{d}{n}{\interval{d[m]+1}{d[n]}}\\
                   f' = \replace{f}{n}{m}
                 \vs{.5}
                 \end{array}   
   %
   \\
   %
\begin{array}{@{}l@{\s{.75}\deq\s{.75}}l@{}}
    \act{N} & \exists n\in\vbl{Node} : 
                  \exists m\in \vbl{Nbrs}(n) : \act{N}_{2}(n,m)
   %
   \\[.2em]
   %
    v & (d, f)
   %
   \\[.2em]
    \Pi & \vbl{Init} \;\land\; \Box[\act{N}]_{v} \;\land\;\WF{v}{\act{N}}
 \end{array}
 \end{array}\]
\vspace{-\baselineskip}
\caption{The spanning-tree algorithm.} \label{fig:st-alg}
\vspace*{1em}%%%spacing hack
\end{figure}

The correctness property to be proved is that, for every node $n$, the
values of $d[n]$ and $f[n]$ eventually become and remain correct.
Letting $\vbl{Dist}(n,m)$ denote the distance in the graph between
nodes $n$ and $m$, the correctness of these values is
expressed by the predicate \vbl{Done}, defined to equal
 \[     \forall\,n\in\vbl{Node} :\;
          \begin{array}[t]{@{\land\s{.5}}l@{}}
             d[n] = \vbl{Dist}(\vbl{Root}, n)\\
             0 < d[n] < \infty \; \implies\;
                  \begin{array}[t]{@{\land\s{.25}}l@{}}
                   f[n]\in\vbl{Nbrs}(n)\\
                   \vbl{Dist}(\vbl{Root}, f[n]) = \vbl{Dist}(\vbl{Root}, n)-1
                 \end{array} 
           \end{array} 
 \]
(If the graph is not connected, then for every node $n$ not in the
root's connected component, \vbl{Done} asserts only that
$d[n]=\infty$.) The assertion that \vbl{Done} eventually becomes and
remains true is expressed by the TLA formula $\Diamond\Box\vbl{Done}$,
where $\Diamond F$, read {\em eventually\/} $F$, is defined to equal
$\lnot\Box\lnot F$.  Correctness of the algorithm is expressed by the
formula
\( \Pi\;\implies\;\Diamond\Box\vbl{Done} \),
which asserts that $\Diamond\Box\vbl{Done}$ holds for every behavior
satisfying $\Pi$.

%%% \pagebreak %%%

The usual first step in reasoning about a concurrent algorithm is to
prove an invariant.  The appropriate invariant \vbl{Inv} for our
algorithm is the following, where $\,\backslash\,$ denotes set
difference.
  \[ \begin{array}[t]{@{\land\s{.5}}l@{}}
         d\in\functions{\vbl{Node}}{\nat\cup\{\infty\}} 
       \\[.2em]
         f \in \functions{\vbl{Node}}{\vbl{Node}}
       \\[.2em]
         d[\vbl{Root}]=0 
       \\[.2em]
         \forall\,n\in\vbl{Node}\,\backslash\,\{\vbl{Root}\} \,:\,
               d[n] < \infty \;\implies\;
                  \begin{array}[t]{@{\land\s{.25}}l@{}}
                   \vbl{Dist}(\vbl{Root}, n) \leq d[n]\\
                   f[n]\in\vbl{Nbrs}(n)\\
                   d[f[n]] < d[n]
                 \end{array} 
     \end{array} 
  \]
The invariance of
\vbl{Inv} is asserted by the formula $\Pi\implies\Box\vbl{Inv}$.  For
brevity, we prove the invariance only of the first two conjuncts
of \vbl{Inv}, which we call \vbl{TC}\@.  A careful hand proof of the
TLA formula $\Pi\implies\Box\vbl{TC}$ expressing the invariance of
\vbl{TC} appears in Figure~\ref{fig:tc-inv-proof} and is discussed
below.  A similar proof for the complete invariant \vbl{Inv} takes
about two pages, but has the same basic structure.

The proof in Figure~\ref{fig:tc-inv-proof} uses a structured format
that we find quite helpful for managing the complexity of proofs.
Step~1 proves that \vbl{TC} holds in the initial state.  Step~2 proves
that any single step starting in a state with \vbl{TC} true leaves it
true.  Step~3 applies the following standard TLA proof 
rule~\cite{lamport:newtla}, where $I'$ denotes the formula obtained
from $I$ by replacing $x$ with $x'$, for each flexible variable $x$.
 \[ {\rm INV1:}\s{.75} \begin{array}[t]{@{}c@{}}
                   I\land[\act{N}]_{v}\;\implies\;I'\\
                    \hline
                   I \land\Box[\act{N}]_{v}\;\implies\;\Box I
                  \end{array}
 \]
The theorem follows trivially from steps 1 and 3.  Step~2, the
``induction step'', is the major part of an invariance proof.  For this
simple invariant, its proof is easy.


\begin{figure}[tb]
\begin{tabbing}
{\bf Theorem} \ $\Pi$ $\implies$ $\Box\vbl{TC}$\\[.5em]
1. \= \vbl{Init} $\implies$ \vbl{TC}\+\\
    \pf\ We assume \vbl{Init} and prove \vbl{TC}.\\
    1.1. \= $d \in \functions{\vbl{Node}}{\nat\cup\{\infty\}}$\+\\
    \begin{minipage}{31.2em}
          \pf\ By definition of \vbl{Init}, considering
               separately the cases
               $\vbl{n}=\vbl{Root}$ and $\vbl{n}\neq\vbl{Root}$.\strut
     \end{minipage}\-\\
%
    1.2. \> $f \in\functions{\vbl{Node}}{\vbl{Node}}$\+\\
          \pf\ By definition of \vbl{Init}.\-\\
    \qed\ Step 1 follows from 1.1, 1.2, and the definition of 
          \vbl{TC}.\-\\[.5em]
%
2. $\vbl{TC}\land [\act{N}]_{v}\;\implies\;\vbl{TC}'$\+\\
     \pf\ We assume \vbl{TC} and $[\act{N}]_{v}$ and prove $\vbl{TC}'$.\\
    2.1. \= $\act{N}\implies \vbl{TC}'$\+\\
        \begin{minipage}{31.2em}
        \pf\ Since $\act{N}=\exists\vbl{n}\in\vbl{Node}, \,
                       \vbl{m}\in\vbl{Nbrs}(n): \act{N}_{2}(n,m)$, it
               suffices to assume $\vbl{n}\in\vbl{Node}$, 
                      $\vbl{m}\in\vbl{Nbrs}(n)$, and 
               $\act{N}_{2}(n, m)$, and to prove $\vbl{TC}'$.\strut
        \end{minipage}\\
%
        2.1.1. \= $d'\in\functions{\vbl{Node}}{\nat\cup\{\infty\}}$\+\\
        \begin{minipage}{29.4em}
          \pf\ By definition of \vbl{TC} and
                 $\act{N}_{2}$, since
                $\interval{d[m] + 1}{d[n]}
               \subseteq\nat\cup\{\infty\}$.\strut
        \end{minipage}\- \\
%
        2.1.2. \> $f'\in\functions{\vbl{Node}}{\vbl{Node}}$\+\\
        \begin{minipage}{29.4em}
         \pf\ By definition of \vbl{TC} and $\act{N}_{2}$,
          since $\vbl{Nbrs}(n) \subseteq \vbl{Node}$, for all nodes
          $n$.\strut
        \end{minipage}\-\\
     \qed\ Step 2.1 follows from 2.1.1, 2.1.2, and the definition of 
      \vbl{TC}.\-\\
%          
      2.2. \> $(v'=v) \;\implies\; \vbl{TC}'$ \+\\
        \pf\ Follows trivially from the definitions.\-\\
%
    \qed\ Step 2 follows from 2.1 and 2.2, since $[\act{N}]_{v} =
           \act{N}\lor(v'=v)$.\-\\[.5em]
%
  3. \= $\vbl{TC} \land \Box [\act{N}]_{v}\;\implies\; \Box\vbl{TC}$\+\\
     \pf\ By step 2 and rule INV1.\-\\
\qed\ The theorem follows from 1, 3, and the definition of $\Pi$.
\end{tabbing}
\vspace{-\baselineskip}
\caption{The proof of invariance of \vbl{TC}.}\label{fig:tc-inv-proof}
\end{figure}

The proof that $\Pi\implies\Box\vbl{Inv}$ is like the invariance proof
for \vbl{TC}, except step~2 is more difficult.  The proof of the
correctness property $\Pi\implies\Diamond\Box\vbl{Done}$ then uses
ordinary temporal-logic reasoning and the TLA proof rule
WF1~\cite{lamport:newtla}; space does not permit its description.

% End of Section 2


% \input{sec3}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           Definitions for Section 3.                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 
% \lpimplies, \lpand, \lpor  : LP's logical symbols
% \timplies, \tand, \tor     : TLA's logical symbols

\newcommand{\lpimplies}{\Rightarrow}
\newcommand{\lpand}{\ \&\ }
\newcommand{\lpor}{\mid}
\newcommand{\timplies}{\stackrel{\scriptscriptstyle \rm tla}{\Rightarrow}}
\newcommand{\tand}{\stackrel{\scriptscriptstyle \rm tla}{\wedge}}
\newcommand{\tor}{\stackrel{\scriptscriptstyle \rm tla}{\vee}}


\section{Encoding TLA in LP}


LP is based on a fragment of multisorted first-order logic.  To reason
about TLA with LP, one must encode TLA formulas in LP's logic.  Our
initial plan was to have a single encoding.  However, as
Figure~\ref{fig:tc-inv-proof} shows, two different kinds of reasoning
are used in TLA proofs: steps 1 and 2 illustrate {\em action
reasoning}, not involving temporal operators; step~3 illustrates {\em
temporal reasoning}.  Since it is formally a special case, action
reasoning is possible in any encoding that allows temporal reasoning.
However, such reasoning can be made easier with a special encoding for
formulas not containing the temporal operator $\Box$.  Action reasoning
is almost always the longest and most difficult part of a proof, so we
decided to use separate encodings for the action and temporal
reasoning.  We have found the resulting simplification of action
reasoning to be worth the inconvenience of having two different
encodings.

% \subsection{Encoding Action Reasoning}

The encoding of action reasoning in LP is straightforward.  TLA's rigid
variables become LP variables.  For each TLA flexible variable $x$, we
encode $x$ and $x'$ as two distinct LP constants.  Thus, the TLA action
$(x'=x+1)\land(y'=y)$ is encoded in LP as \verb|(x'=x+1)&(y'=y)|.

% \subsection{Encoding Temporal Reasoning}

The encoding of temporal reasoning is more subtle.  In TLA, a formula
is an assertion that is true or false for a behavior.  Let $\sigma
\models F$ denote that the behavior $\sigma$ satisfies the TLA formula
$F$.  Formula $F$ is valid iff $\sigma \models F$ is true for all
behaviors $\sigma$.  The validity of $F$ is represented in LP's logic
by $\forall \sigma: \sigma\models F$.  Neglecting details of the
precise ASCII syntax, this formula is written in LP as $\sigma\models
F$, universal quantification over the free variable $\sigma$ being
implicit.  The semantic operator $\models$, which cannot appear in
a TLA formula, becomes part of the formula's LP translation.

TLA's (temporal) proof rules have straightforward translations into
LP\@.  For example, the proof rule INV1 asserts
 \[ \frac{\forall \sigma : \sigma \models (I \land [N]_f \implies I')}%
     {\forall \sigma: \sigma \models (I \land \Box{}[N]_f \implies \Box{}I)}
 \]
In this rule, $\land$, $\implies$, and $'$ are operators declared in LP
to represent the corresponding TLA operators.  In particular, $\land$
and $\implies$ are different from LP's built-in conjunction (\verb|&|)
and implication (\verb|=>|) operators.  Propositional reasoning about
temporal formulas is done in LP using such axioms as
  \[ \sigma\models (F\land G) \s{.75}=\s{.75}
 (\sigma\models F) \;\hbox{\verb|&|}\;
                                  (\sigma\models G)
  \]  

%% End of Section 3




%\input{sec4}

\section{The Translator}

The TLA translator is a program written in Standard ML
\cite{harper:sml} that translates ``humanly readable'' TLA
specifications and proofs into LP proof scripts.  Their readability
makes proofs easier to maintain when the specifications change than
they would be if written directly in LP\@.  The different encodings for
action reasoning and temporal reasoning are translated into two
separate LP input files.  Formulas proved in the action encoding are
asserted in the temporal encoding.  The proof succeeds if LP
successfully processes both files.


\subsection{Specifications}

Figure \ref{fig:tlac-span} is the input to the TLA translator
corresponding to the spanning-tree algorithm of
Figure~\ref{fig:st-alg}.  (All translator input is shown exactly
as typed by the user, except that multiple fonts have been used for clarity.)
It begins with a declaration of \pvar{Span} as
the name of the specification, followed by a directive to read
the file \pvar{frame}, which contains declarations of all
constants such as 0, $+$, \pvar{Nbrs}, and \pvar{Node}.  
The next two lines
declare \pvar{d} and \pvar{f} to be (flexible) variables.  
(In TLA's typeless logic,
the only sorts are Boolean and Any.) The rest of the
specification is a direct transliteration of
Figure~\ref{fig:tlac-span}, except for two differences: the action
\pact{N}\psuf{1}(\pvar{n}) is defined for use in the proofs, and \pstar\ is used instead
of comma to denote ordered pairs.  The translation of these definitions into LP
rewrite rules is straightforward, except for quantified expressions and the
lambda-construct.  LP does not now support full first-order quantification, so
we have defined LP operators and associated proof rules for quantification and
lambda abstraction.  Each occurrence of a quantifier or ``lambda'' requires the
definition of an auxiliary function, which is named for reference in proofs by
a term in brackets \plbrack\pstar\ \ldots\ \pstar\prbrack.


\begin{figure}[tb]
  
\begin{tlafigure}

\kwd{Name} \xvar{Span}\\
\smallspace
\kwd{Use} \xvar{frame}\\
\smallspace
\kwd{Variables}\\
  \>\pvar{d}, \pvar{f}  \>\pcolon\ \kwd{Any}\\
\smallspace
\kwd{Predicates}\\
  \>\pvar{Init}	        \>\pdefeq\ \>\verb:/\:\ \pvar{d} = \plambda\ \pvar{n} \pin\ \xvar{Node} \pcolon\ \\
		             \>\>\>\>\>~\kwd{If} \pvar{n} = \xvar{Root} \kwd{Then} 0 \kwd{Else} \pinfty\ \plbrack \pstar\ dist \pcolon\ \kwd{Any} \pstar\prbrack\\
                             \>\>\>\verb:/\:\ \pvar{f} \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{Node}\prbrack\\
\smallspace
\kwd{Actions}\\
  \>\pact{N}\psuf{2}\plpar \pvar{n}, \pvar{m}\prpar  \>\pdefeq\ \>\verb:/\:\ \pvar{d}\plbrack\pvar{m}\prbrack\ \verb:~=: \pinfty\\
                             \>\>\>\verb:/\:\ \pvar{d}$'$ \pin\ \pvar{d}\plbrack\pvar{n} \passignin\ \xvar{openInter}\plpar \pvar{d}\plbrack\pvar{m}\prbrack\ + 1, \pvar{d}\plbrack\pvar{n}\prbrack\prpar \prbrack\\
                             \>\>\>\verb:/\:\ \pvar{f}$'$ = \pvar{f}\plbrack\pvar{n} \passigneq\ \pvar{m}\prbrack\\
\smallspace
  \>\pact{N}\psuf{1}\plpar \pvar{n}\prpar  \>\pdefeq\ \>\pexists\ \pvar{m} \pin\ \xvar{Nbrs}\plpar \pvar{n}\prpar\  \pcolon\ \pact{N}\psuf{2}\plpar \pvar{n}, \pvar{m}\prpar\  \plbrack\pstar\ n\psuf{1}\plpar \pvar{n}\prpar\  \pstar\prbrack\\
\smallspace
  \>\pact{N}            \>\pdefeq\ \>\pexists\ \pvar{n} \pin\ \xvar{Node} \pcolon\ \pact{N}\psuf{1}\plpar \pvar{n}\prpar\  \plbrack\pstar\ n \pstar\prbrack\\
\smallspace
\kwd{Statefunctions}\\
  \>\pvar{v}	        \>\pdefeq\ \>\plpar \pvar{d} \pstar\ \pvar{f}\prpar \\
\smallspace
\kwd{Formulas}\\
  \>\pvar{Pi}	\>\pdefeq\ \>\pvar{Init} \verb:/\:\ \pbox\plbrack\pact{N}\prbrack\psfsuf{\pvar{v}} \verb:/\:\ \kwd{WF}\plpar \pvar{v}, \pact{N}\prpar 

\end{tlafigure}
\vspace{-\baselineskip}
  \caption{The spanning-tree algorithm, in the translator's input language.}
  \label{fig:tlac-span}
\end{figure}

In TLA, prime ($'$) is an operator that can be applied to predicates
like \pvar{Init} and to state functions like \pvar{v}, where priming an
expression replaces all variables by their primed versions.  In the LP
action encoding, primed and unprimed variables become distinct
constants, so the prime operator cannot be expressed.  The ``bar
operator'' used in refinement~\cite[Section 9.3.2]{lamport:newtla} and
TLA's {\em Enabled\/} operator~\cite[Section 3.7]{lamport:newtla} are
similarly inexpressible.  The translator must therefore add to the LP
encoding rewrite rules explicitly defining such expressions as
\pvar{Init}$'$, $\overline{\pvar{v}}$, and ${\it Enabled~{\cal N}}$.
Definitions for the primed and barred expressions are generated
automatically by the translator.  Definitions for the {\it Enabled\/}
predicates must now be provided by the user; future versions of the
translator will generate them as well.


\subsection{Proofs}

The invariant \xvar{TC} of our spanning-tree algorithm is specified in
the translator's language as
\begin{tlafigure}
  \>\pvar{TC} \pdefeq\ \pvar{d} \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{NatInf}\prbrack\ \verb:/\:\ \pvar{f} \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{Node}\prbrack
\end{tlafigure}
where \xvar{NatInf} denotes $\nat\cup\{\infty\}$.
The hand proof of invariance of \xvar{TC} was based on certain tacit
assumptions about \pvar{Root}, \xvar{Node}, and \pvar{Nbrs}.  The
formal statement of these assumptions is the assertion \xvar{Assump},
defined in the translator input to be the conjunction of the following
two assertions.  (Since the set construct has a bound variable, it
requires the same kind of auxiliary function used for quantifiers and
``lambda''.)
\begin{tlafigure}
\+\kill
  \pvar{Assump1} \= \pdefeq\ \pvar{Root} \pin\ \xvar{Node}\\
%\linespace
  \pvar{Assump2} \>\pdefeq\ \= \pforall\ n \pin\ \xvar{Node} \pcolon\ \\
              \>   \> \hspace{1em}%
                     \pvar{Nbrs}\plpar \pvar{n}\prpar\  
                         $=$ \= \plcrl\pvar{m} \pin\ \xvar{Node} :\\
     \> \>  \> \hspace{1em}%
    \pvar{NbrRel}\plpar \pvar{n}, \pvar{m}\prpar\  
     \plbrack\pstar\ a22\plpar \pvar{n}\prpar\  \pstar\prbrack\prcrl\ \ 
                     \plbrack\pstar\ a21 \pstar\prbrack
\end{tlafigure}
where \pvar{NbrRel} denotes the neighbor relation on the graph.  Further
assumptions about \pvar{NbrRel} are needed for the complete correctness proof
of the algorithm.

Figure~\ref{fig:tlac-proof} contains the translator version of the
invariance proof of Figure~\ref{fig:tc-inv-proof}.  
It has the same structure as the
hand proof in Figure \ref{fig:tc-inv-proof}.  Steps are numbered in the
more compact fashion $\langle\mbox{\it level\/}\rangle\mbox{\it
step}$, with \kwd{Step}$\langle2\rangle3$ denoting the third
substep of level two and \kwd{Hyp}$\langle1\rangle.2$ denoting the
second hypothesis of level one of the current proof.

The proof is written in a natural deduction style, the translator
input \kwd{Assume}~$A$~\kwd{Prove}~$B$ denoting that
$A \Rightarrow B$ is to be
proved by assuming $A$ and proving $B$.
The goal $B$ can be omitted if it is the same as the current goal.  (In
the temporal encoding, assuming $A$ and proving $B$ means assuming
$\sigma\models A$ and proving $\sigma\models B$, for an arbitrary
constant $\sigma$.) The construct \kwd{Reduce~by}~$A$~\kwd{To}~$B$
expresses an argument of the form ``By $A$ it suffices to prove $B$.''
It is converted into LP's style of
direct reasoning by rearranging the proof steps.  \kwd{Normalize},
\kwd{Apply}, and \kwd{Crit} are LP commands.  The applied rules, such
as BoxElim1, are defined in LP for reasoning about the translator
output.  In step $\langle1\rangle3$, INV1 
applies the INV1-rule and \kwd{Crit}'s the current
hypotheses with the resulting fact.  


\begin{figure}
\vspace{-8ex}
  
\begin{tlaproof}
\kwd{Theorem} TC\+\\
  \kwd{Assume} \pbox \pvar{Assump} 
                       ~\kwd{Prove} \pvar{Pi} \pimplies\ \pbox \pvar{TC}\-\\
\linespace
\kwd{Proof}\+\\
  $\langle1\rangle1$ \kwd{Assume} \pvar{Assump}, \pvar{Init} ~\kwd{Prove} \pvar{TC}\+\\
\linespace
    $\langle2\rangle1$ \pvar{d} \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{NatInf}\prbrack\pushtabs\\
    \kwd{Reduce} \=\kwd{by} \=Normalize \kwd{Hyp}$\langle1\rangle.2$ with
\pdef{Init},\+\+\\
                         Apply ProveFuncSpaceLambda to \kwd{Red}\-\-\\
    \kwd{To} ~\kwd{Assume} \pvar{n} \pin\ \xvar{Node} ~\kwd{Prove} \pvar{d}\plbrack\pvar{n}\prbrack \pin\ \xvar{NatInf}\\
    \poptabs\+
\linespace
      $\langle3\rangle1$ \kwd{Case} \pvar{n} $=$ \xvar{Root}\\
      \kwd{Qed} \kwd{by} Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{Init}\\
\linespace
      $\langle3\rangle2$ \kwd{Case} \pvar{n} \verb|~|$=$ \xvar{Root}\\
      \kwd{Qed} \kwd{by} Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{Init}\-\\
\linespace
    \kwd{Qed} \kwd{by} \kwd{Cases}\\
\linespace
    $\langle2\rangle2$ \pvar{f} \kwd{in} \plbrack \xvar{Node} \pmaps\ \xvar{Node}\prbrack\\
    \kwd{Qed} \kwd{by} Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{Init}\-\\
\linespace
  \kwd{Qed} \kwd{by} Normalize \kwd{Goal} with \pdef{TC}\\
\linespace
  $\langle1\rangle2$ \kwd{Assume} \pvar{Assump}, \pvar{TC}, \plbrack\pact{N}\prbrack\psfsuf{\pvar{v}} ~\kwd{Prove} \pvar{TC}$'$\+\\
\linespace
    $\langle2\rangle1$ \kwd{Case} \pact{N}\pushtabs\\
    \kwd{Reduce} \=\kwd{by} Normalize \kwd{Hyp} with \pdef{N}\\
    \kwd{To} ~\kwd{Assume} \pvar{n} \pin\ \xvar{Node} \verb:/\:\ \pact{N}\psuf{1}\plpar \pvar{n}\prpar \\
    \kwd{Reduce} \>\kwd{by} Normalize \kwd{Hyp} with \pdef{N}\psuf{1}\\
    \kwd{To} ~\kwd{Assume} \pvar{m} \pin\ \xvar{Nbrs}\plpar \pvar{n}\prpar\  \verb:/\:\ \pact{N}\psuf{2}\plpar \pvar{n}, \pvar{m}\prpar \+\\
    \poptabs
\linespace
      $\langle3\rangle1$ \pvar{d}$'$ \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{NatInf}\prbrack\+\\
\linespace
        $\langle4\rangle1$ \kwd{Assume} \pvar{k} \pin\ \xvar{openInter}\plpar \pvar{d}\plbrack\pvar{m}\prbrack\ + 1, \pvar{d}\plbrack\pvar{n}\prbrack\prpar\  ~\kwd{Prove} \pvar{k} \pin\ \xvar{NatInf}\\
	\kwd{Qed} \kwd{by} Normalize \kwd{Hyp} with UseOpenInterval\-\pushtabs\\
\linespace
      \kwd{Qed} \kwd{by} \=Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{TC},\+\\
                         Normalize \kwd{Hyp}$\langle2\rangle$ with \pdef{N}\psuf{2},\\
                         Apply ProveFuncSpaceUpdateIn to \kwd{Hyp}$\langle1\rangle.2$ \kwd{Hyp}$\langle2\rangle$ \kwd{Step}$\langle4\rangle1$\-\\
                         \poptabs
\linespace
      $\langle3\rangle2$ \pvar{f}$'$ \pin\ \plbrack \xvar{Node} \pmaps\ \xvar{Node}\prbrack\+\\
\linespace
        $\langle4\rangle1$ \pvar{m} \pin\ \xvar{Node}\\
	\kwd{Qed} \kwd{by} Normalize \kwd{Hyp}$\langle1\rangle.1$ with 
         \xvar{Assump} \xvar{Assump2}\-\pushtabs\\
\linespace
      \kwd{Qed} \kwd{by} \=Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{TC},\+\\
                         Normalize \kwd{Hyp}$\langle2\rangle$ with \pdef{N}\psuf{2},\\
                         Apply ProveFuncSpaceUpdateEq to \kwd{Hyp}$\langle1\rangle.2$ \kwd{Hyp}$\langle2\rangle$ \kwd{Step}$\langle4\rangle1$\-\-\\
                         \poptabs
\linespace
    \kwd{Qed} \kwd{by} Normalize \kwd{Goal} with \pdef{TC}\\
\linespace
    $\langle2\rangle2$ \kwd{Case} Unchanged\plpar \pvar{v}\prpar \pushtabs\\
    \kwd{Qed} \kwd{by} \=Normalize \kwd{Hyp} with \pdef{v},\+\\
                       Normalize \kwd{Hyp}$\langle1\rangle.2$ with \pdef{TC},\\
                       Normalize \kwd{Goal} with \pdef{TC}\-\-\\
                       \poptabs
\linespace
  \kwd{Qed} \kwd{by} \kwd{Cases}\\
\linespace
  $\langle1\rangle3$ \kwd{Assume} \pbox \pvar{Assump}, \pvar{TC}, \pbox \plbrack\pact{N}\prbrack\psfsuf{\pvar{v}} ~\kwd{Prove} \pbox \pvar{TC}\\
  \kwd{Qed} \kwd{by} INV1 on \kwd{Step}$\langle1\rangle2$\-\pushtabs\\
\linespace
\kwd{Qed} \kwd{by} \=Normalize \kwd{Hyp} with Pi,\+\\
                    Apply BoxElim1 to \kwd{Hyp},\\
                    Crit \kwd{Hyp} with \kwd{Step}1 \kwd{Step}3\-\\
                    \poptabs
\end{tlaproof}
\vspace{-1.5\baselineskip}
  \caption{Proof of invariance of \xvar{TC}, in the translator's input 
         language.}
  \label{fig:tlac-proof}
\end{figure}







Figure~\ref{fig:tc-output} shows 
\begin{figure}[tb]
%\begin{scriptsize}
\begin{footnotesize}
\begin{verbatim}
set name Theorem_Tc1_2_1_1
prove in(d', funcSpace(Node, NatInf))
  set name Theorem_TC_2_1_1_1
  prove (in(v_k_, openInter(((d@v_m_c)+1), (d@v_n_c))) => in(v_k_,NatInf))
    resume by =>
    <> 1 subgoal for proof of =>
      normalize Theorem_TC_2_1_1_1ImpliesHyp with UseOpenInterval 
      [] => subgoal
    [] conjecture
  set name Theorem_TC_2_1_1
  normalize Theorem_TC_2ImpliesHyp.2 with TC 
  normalize Theorem_TC_2_1ImpliesHyp with N12 
  apply ProveFuncSpaceUpdateIn to Theorem_TC_2ImpliesHyp.2 Theorem...
  [] conjecture
\end{verbatim}
%\end{scriptsize}
\end{footnotesize}
\vspace{-\baselineskip}
  \caption{Translator output
  for step $\langle3\rangle1$ in the proof of step $\langle1\rangle2$ 
  of Figure~\protect\ref{fig:tlac-proof}.}
  \label{fig:tc-output}
\end{figure}
the LP input in the action-reasoning file generated from step
$\langle3\rangle1$ in the proof of step $\langle1\rangle2$.  Additional
translator constructs allow arbitrary LP input to be inserted into the
output, making the full power of LP available through the translator.
(Soundness is maintained if no LP {\tt assert} commands are inserted.)
Such direct use of LP was not needed in this proof; our ultimate goal
is to make it unnecessary in general.

The predicate \xvar{TC} is just one part of the entire invariant
\xvar{Inv}.  About three more pages of translator input completes the
proof of invariance of \xvar{Inv}.  The rest of the correctness proof
takes about six more pages.  These proofs required additional
properties of numbers (elements of \xvar{NatInf}), functions, and the
distance function \xvar{Dist}---including the well-foundedness of the
ordering on
  $[\xvar{Node} \rightarrow \xvar{Nat}\cup\{\infty\}]$
defined by $f\leq g$ iff $f[n]\leq g[n]$ for all $n\in\xvar{Node}$.
Properties of the natural numbers (associativity of addition etc.)\
were expressed directly in LP\@.  Properties of the distance
function needed for the proof were asserted in the translator
input. Although
these properties can be proved from more primitive definitions, we have
ignored such conventional verification in order to concentrate on the
novel aspects of TLA. 


% End of Section 4

\section{Future Directions}

It is obviously easier to write a TLA proof in TLA than in an LP
encoding of TLA\@.  It was not obvious to us how much easier it would
be.  Our initial experience indicates that writing a proof with the
translator can be an order of magnitude faster than doing the proof
directly in LP\@.  Such a speed-up is possible only if the proof can be
written in the translator with no direct use of LP\@.  We are planning
to enhance the translator to eliminate all direct LP
reasoning.

Translating the steps of a proof rather than just the property to be
proved permits the use of multiple verification methods.  The
translator now generates separate LP input for action and temporal
reasoning.  We plan to generate input to other verification systems as
well.  Steps that are provable by simple temporal reasoning will be
verified automatically by a decision procedure for propositional
temporal logic.  Some steps might be proved with a model checker by
enumerating all possibilities.  We may also investigate the use of
theorem provers other than LP as ``back ends'' for the translator.



\newpage

\bibliographystyle{plain}
%\bibliographystyle{alpha}
%\bibliography{mybib}
\begin{thebibliography}{1}

\bibitem{garland:overview}
Stephen~J. Garland and John~V. Guttag.
\newblock An overview of {LP}, the {Larch} {Prover}.
\newblock In N.~Dershowitz, editor, {\em Proceedings of the Third International
  Conference on Rewriting Techniques and Applications}, volume 355 of {\em
  Lecture Notes on Computer Science}, pages 137--151. Springer-Verlag, April
  1989.

\bibitem{garland:guide}
Stephen~J. Garland and John~V. Guttag.
\newblock A guide to {LP}, the {L}arch {P}rover.
\newblock Technical Report~82, Digital Equipment Corporation Systems Research
  Center, December 1991.

\bibitem{harper:sml}
Robert Harper, David MacQueen, and Christopher Wadsworth.
\newblock Standard {ML}.
\newblock Internal Report ECS--LFCS--86--2, Edingburgh University, March 1986.

\bibitem{lamport:sometime}
Leslie Lamport.
\newblock `{S}ometime' is sometimes `not never': A tutorial on the temporal
  logic of programs.
\newblock In {\em Proceedings of the Seventh Annual Symposium on Principles of
  Programming Languages}, pages 174--185. ACM SIGACT-SIGPLAN, January 1980.

\bibitem{lamport:what-good}
Leslie Lamport.
\newblock What good is temporal logic?
\newblock In R.~E.~A. Mason, editor, {\em Information Processing 83:
  Proceedings of the IFIP 9th World Congress}, pages 657--668, Paris, September
  1983. IFIP, North-Holland.

\bibitem{lamport:newtla}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock Technical Report~79, Digital Equipment Corporation, Systems Research
  Center, December 1991.

\bibitem{pnueli:temporal}
Amir Pnueli.
\newblock The temporal logic of programs.
\newblock In {\em Proceedings of the 18th Annual Symposium on the Foundations
  of Computer Science}, pages 46--57. IEEE, November 1977.

\end{thebibliography}


\end{document}

