%% %% \documentclass{llncs} %\documentclass[a4paper,11pt,twocolumn]{article} %\usepackage{makeidx} %\usepackage{acmnew-xref} % \usepackage[scrtime]{prelim2e} \usepackage{latexsym} \usepackage{amsmath} \usepackage{amssymb} % \usepackage{exptrees} \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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Preamble \newcommand\cfile{} \newcommand\comment[1]{} % \newcommand\cc[1]{} % for label names \newcommand\cc[1]{#1} % for label names % \renewcommand\footnote[1]{} % for footnotes % \pagestyle{myheadings} \renewcommand\theenumi{(\alph{enumi})} \renewcommand\labelenumi{\theenumi} \renewcommand\theenumii{(\roman{enumii})} \renewcommand\labelenumii{\theenumii} \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\up[1]{\vspace{-#1ex}} \newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree \newcommand\state{\textit{state}} \newcommand\outcome{\textit{outcome}} \newcommand\tcres{\textit{tcres}} \newcommand\unittc{\textit{unit\_tc}} \newcommand\unitos{\textit{unit\_os}} \newcommand\exto{\textit{ext\_o}} \newcommand\extos{\textit{ext\_os}} \newcommand\exttc{\textit{ext\_tc}} \newcommand\pexttc{\textit{pext\_tc}} \newcommand\prodtc{\textit{prod\_tc}} \newcommand\seqtc{\textit{seq\_tc}} \newcommand\swaptc{\textit{swap\_tc}} \newcommand\swapi{\textit{swapi}} \newcommand\set{\textit{set}} \newcommand\infch{\textit{infch}} \newcommand\infchs{\textit{infchs}} \newcommand\icnt{\textit{icnt}} \newcommand\reachnt{\textit{reach\_NT}} \newcommand\TorN{\texttt{TorN}} \newcommand\Term{\texttt{Term}} \newcommand\ssos{\texttt{sts\_of\_ocs}} \newcommand\NonTerm{\texttt{NonTerm}} \newcommand\val{\textit{value}} \newcommand\name{\textit{name}} \newcommand\choice{\textit{choice}} \newcommand\Cs{\ensuremath{\mathcal{C}}} \newcommand\Qs{\ensuremath{\mathcal{Q}}} \newcommand\Ss{\ensuremath{\mathcal{S}}} \newcommand\As{\ensuremath{\mathcal{A}}} \newcommand\spom{\textit{spom}} \newcommand\wpom{\textit{wpom}} \newcommand\wlp{\textit{wlp}} \newcommand\slp{\textit{slp}} \renewcommand\wp{\textit{wp}} \renewcommand\sp{\textit{sp}} \newcommand\trm{\textit{trm}} \newcommand\bool{\textit{bool}} \newcommand\nat{\textit{nat}} \newcommand\aexp{\textit{exp}} \newcommand\bexp{\textit{bexp}} \newcommand\seq{\textit{seq}} \newcommand\skp{\textit{skip}} \newcommand\magic{\textit{magic}} \newcommand\abort{\textit{abort}} \newcommand\magictc{\textit{magic\_tc}} \newcommand\aborttc{\textit{abort\_tc}} \newcommand\pcaux{\textit{pc\_aux}} \newcommand\while{\textit{while}} \newcommand\iif{\textit{if}} \newcommand\els{\textit{else}} \newcommand\then{\textit{then}} \newcommand\eend{\textit{end}} \newcommand\ddo{\textit{do}} \newcommand\prd{\textit{prd}} \newcommand\fram{\textit{frame}} \newcommand\frm{\textit{frame}} \newcommand\rep{\textit{rep}} \newcommand\repall{\textit{repall}} \newcommand\setvars{\textit{setvars}} \newcommand\chst{\textit{chst}} \newcommand\tc{\textit{\_tc}} \newcommand\lub{\textit{lub}} \newcommand\pext{\textit{pext}} \newcommand\prodd{\textit{prod}} \newcommand\dorp{\textit{dorp}} \newcommand\swap{\textit{swap}} \newcommand\ext{\textit{ext}} \newcommand\id{\textit{id}} \newcommand\unit{\textit{unit}} \newcommand\map{\textit{map}} \newcommand\join{\textit{join}} \newcommand\oo{\ensuremath{\circ}} \newcommand\om{\ensuremath{\odot}} \newcommand\M{\ensuremath{_M}} \newcommand\NM{\ensuremath{_{NM}}} \newcommand\unitM{\ensuremath{\unit_{M}}} \newcommand\extM{\ensuremath{\ext_M}} \newcommand\mapM{\ensuremath{\map_M}} \newcommand\joinM{\ensuremath{\join_M}} \newcommand\oM{\ensuremath{\odot_M}} \newcommand\N{\ensuremath{_N}} \newcommand\extN{\ensuremath{\ext_N}} \newcommand\unitN{\ensuremath{\unit_N}} \newcommand\oN{\ensuremath{\odot_N}} \newcommand\extNM{\ensuremath{\ext_{NM}}} \newcommand\pextNM{\ensuremath{\pext_{NM}}} \newcommand\unitNM{\ensuremath{\unit_{NM}}} \newcommand\mapNM{\ensuremath{\map_{NM}}} \newcommand\joinNM{\ensuremath{\join_{NM}}} \newcommand\oNM{\ensuremath{\odot_{NM}}} \newcommand\extfun{\textit{ext-funct}} \newcommand\extlu{\textit{ext-L-unit}} \newcommand\extru{\textit{ext-R-unit}} \newcommand\pextlu{\textit{pext-L-unit}} \newcommand\pextru{\textit{pext-R-unit}} \newcommand\pextfun{\textit{pext-funct}} \newcommand\pextomap{\textit{pextomap}} \newcommand\pextpm{\textit{pext-pm}} \newcommand\omext{\textit{\om -ext}} \newcommand\extom{\textit{ext-\om}} \newcommand\mapext{\textit{map-ext}} \newcommand\joinext{\textit{join-ext}} % \newcommand\ompext{\textit{\om -pext}} % \newcommand\bindext{\textit{bind-ext}} % \newcommand\pextext{\textit{pext-ext}} \newcommand\extjm{\textit{ext-jm}} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 \newtheorem{condition}{Condition} % 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})} \pagestyle{plain} \begin{document} %% Here begins the main text \title{Formalising Generalised Substitutions} \author{ Jeremy E.\ Dawson\inst{1}\inst{2}} \institute{ Logic and Computation Program, NICTA \thanks{National ICT Australia is funded by the Australian Government's Dept of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia's Ability and the ICT Centre of Excellence program.} \and Automated Reasoning Group, \\ Australian National University, Canberra, ACT 0200, Australia \\ \url{http://users.rsise.anu.edu.au/~jeremy/} } \date{\today} %% Title \maketitle \begin{abstract} We use the theorem prover Isabelle to formalise and machine-check results of the theory of generalised substitutions given by Dunne and used in the B method. We describe the model of computation implicit in this theory and show how this is based on a compound monad, and we contrast this model of computation and monad with those implicit in Dunne's theory of abstract commands. Subject to a qualification concerning frames, we prove, using the Isabelle/HOL theorem prover, that Dunne's results about generalised substitutions follow from the model of computation which we describe. \\ {\bf Keywords}: general correctness, generalised substitution \end{abstract} \section{Introduction} \label{s-id} In \cite{dunne-abstr-cmds} Dunne gave an account of general correctness, which combines the concepts of partial correctness and total correctness, arguing for its utility in analysing the behaviour of programs. He defined a language of ``abstract commands'', giving several basic abstract commands and operators for joining them, for which he gave rules in terms of weakest liberal preconditions and termination conditions. In \cite{dawson-fgc} we considered this abstract command language and described the operational interpretation of the abstract commands, showing how it is based on a compound monad. We used the automated theorem proving system Isabelle to prove that the operational interpretation implies the rules given by Dunne. In \cite{chartier-b-hol} Chartier formalised the operations of the B method of Abrial \cite{abrial-b-book} in Isabelle/HOL. He formalised generalised substitutions as an abstract type comprising the \trm\ and \prd\ functions and a list of variables involved in the substitution. Defining the generalised substitution operations in terms of \trm\ and \prd, he proved that these definitions are equivalent to those of Abrial's definitions in terms of the weakest precondition functions. In \cite{dunne-gen-subs} Dunne considered the generalised substitutions used in the B~method. He developed the notion of the frame of a substitution, the variables ``involved'' in it, and defined generalised substitution operations in terms of frames and weakest preconditions. He then proved a number of properties of these generalised substitutions. In contrast to \cite{dunne-abstr-cmds}, this theory is based on total correctness. In this paper we formalise this theory of generalised substitutions, using a similar approach to our work on abstract commands % and general correctness in \cite{dawson-fgc}, and using some of its results. That is, we develop a model of computation and define the theory in terms of it. We then find that this enables us to derive the previous definitions and results as consequences of our formulation. These results are proved using the Isabelle/HOL theorem prover, see \cite{dawson-fgc-files}. We have also performed, in Isabelle, proofs of other results of Dunne in \cite{dunne-gen-subs}, of which details are in the Appendix. % XX We find that the model of computation we use is also based on a compound monad, and provides an interesting example of a distributive law for monads. Furthermore, this distributive law is also a monad morphism from the monad of \cite{dawson-fgc} to the monad described in this paper. \section{The Operational Models} \label{s-om} In \cite{dunne-abstr-cmds} Dunne argued that general correctness provides a better framework for program refinement than either total or partial correctness, and its relative simplicity is supported by the results at the end of \cite[\S 3.2]{dawson-fgc}. However the theory of generalised substitutions as used in the B method is based on total correctness, so that when two generalised substitutions with the same frame are equivalent in total correctness, they are regarded as the same, although they may not be equivalent in terms of general correctness. So we need to model program (statements) in such a way that two such generalised substitutions are equal. So we describe the two operational models. Firstly, we review the operational model of \cite{dawson-fgc}, which we used for \emph{abstract commands}, based on \emph{general correctness}. % used to describe abstract commands and general correctness. % Using this model enables us to re-use results of that paper. Then we describe the model, on which this paper is based, which fits the \emph{total correctness} framework of \emph{generalised substitutions}. We describe these models, at first without reference to frames, which we discuss in \S\ref{s-fvn}. Furthermore, where we state that we have proved a result of Dunne \cite{dunne-gen-subs}, this will usually refer to the result as modified by deleting reference to the frames of the substitutions. \subsection{The General Correctness Operational Model} \label{s-gcm} To express that a command can either terminate in a new state or fail to terminate, in \cite{dawson-fgc} we considered command \emph{outcomes}, where an outcome is either termination in a new state or non-termination. Then we model a command as a function, of type $\state \to \outcome\ \set$, from states to sets of outcomes. Commands are equal if the corresponding functions are equal: that is, we have an extensional definition of equality. This model can distinguish between a command which (when executed in a particular given state) must fail to terminate from one which may or may not fail to terminate. Since Dunne's treatment of {abstract commands} \cite{dunne-abstr-cmds} distinguished between two such commands, this model was effective in considering {abstract commands}. However a theory of total correctness, using weakest preconditions (which are satisfied only when a command is guaranteed to terminate), does not distinguish between two such commands. \subsection{The Total Correctness Operational Model} \label{s-tcom} For the total correctness model, we model a generalised substitution as a function returning either the tag \NonTerm, indicating possible non-termination, or \Term\ $S$, indicating guaranteed termination in one of the states contained in the set $S$. Note that this implies an extensionsal definition of equality: substitutions are equal iff they are equal considered as functions of the appropriate type. To do this we declare the Isabelle datatype \begin{center} \tt datatype $\sigma$ TorN = NonTerm | Term $\sigma$ \end{center} where $\sigma$ is a type variable. This means that a value of the type $\sigma$ \TorN\ is either the tag \NonTerm\ or a member of the type $\sigma$, tagged with the tag \Term. (Thus the type \outcome\ of \cite{dawson-fgc} is \state\ \TorN). % We then define the type \tcres\ to be \state\ \set\ \TorN, that is, either non-termination, or termination in (one of) a set of states. (As in Isabelle, we write a type constructor after the type.) Then we model a generalised substitution as a function of type $\state \to \tcres$. For a generalised substitution $C$, we define $[C]$ (or $\wp\ C$, the weakest precondition of $C$) for post-condition $Q$ and initial state $s$, as follows. Then, from it, we define total correctness refinement $\sqsubseteq_{tc}$. By $P \longrightarrow Q$ % (\verb|P ---> Q|) we mean $\forall s.\ P\ s \rightarrow Q\ s$. \begin{align*} [C]\ Q\ s & = \exists S.\ (\forall x \in S.\ Q\ x) \land C\ s = \Term\ S \\ A \sqsubseteq_{tc} B & = \forall Q.\ [A]\ Q \longrightarrow [B]\ Q \end{align*} \begin{verbatim} "wp_tc C Q s == EX S<=Collect Q. C s = Term S" "ref_tc A B == ALL Q. wp_tc A Q ---> wp_tc B Q" \end{verbatim} The definition makes it clear that refinement is a preorder. We then obtain a direct characterisation of refinement, and, from it, we show (as \verb|ref_tc_antisym|) that two generalised substitutions $A,B$ (of type $\state \to \tcres$) are refinement-equivalent if and only if they are equal in our operational model. Thus refinement is a partial order. This confirms that the operational model above is appropriate for total correctness refinement and equivalence. The related result \verb|wp_tc_inj| is useful for proving the equality of two generalised substitutions. \begin{verbatim} ref_tc_alt = "ref_tc A B == ALL s SA. A s = Term SA --> (EX SB<=SA. B s = Term SB)" ref_tc_antisym = "[| ref_tc A B; ref_tc B A |] ==> A = B" wp_tc_inj = "wp_tc A = wp_tc B ==> A = B" \end{verbatim} \subsection{The Total Correctness Compound Monad} \label{s-tcmon} In \cite[\S 3.1]{dawson-fgc} we showed that the general correctness operational monad gave a monad, which we will call the \emph{outcome set} monad. See \cite[\S 3.1]{dawson-fgc} for a brief discussion of monads, or Wadler \cite{Wadler-essence} for further information. We now find that the type \tcres, relative to the type \state, is a monad, % which we will call the \emph{total correctness} monad. To define a monad $M$, we need to define the unit and extension functions, of the types shown. The unit function models the command which does nothing (\skp) and the extension function is used to model sequencing of commands since \ext\ $A$ models the action of command $A$ on the output of a previous command. We then need to show that the unit and extension functions satisfy the following rules required for a monad. \begin{align*} \unit &: \alpha \to \alpha M \\[-0.5ex] \ext &: (\alpha \to \beta M) \to (\alpha M \to \beta M) \end{align*} \begin{align} \label{E1} \ext\ f \oo \unit & = f \\[-0.5ex] \label{E2} \ext\ \unit & = \unit \\[-0.5ex] \label{E3} \ext\ (\ext\ g \oo f) & = \ext\ g \oo ext\ f \end{align} As a standard result (see \cite{Wadler-essence}), a monad can be characterised either by the three functions \unit, \map\ and \join, and seven axioms involving these functions, or the functions \unit\ and \ext\ and the three axioms shown above. % So proving the three rules above % shows that the unit and extension functions \unittc\ and \exttc\ % form a monad. Rule \eqref{E3} lets us define sequencing of commands, $A;B$ (or $\seq\ A\ B$) $ = \ext\ B \circ A$, and, as in \cite[\S 3.1]{dawson-fgc}, the associativity of \seq\ (which obviously ought to hold!) follows from \eqref{E3}. We have that \tcres\ = \state\ \set\ \TorN. Each of the type constructors \set\ and \TorN\, with their associated unit and extension functions, is a monad. It does not follow, however, that \tcres\ (relative to \state) is a monad. To prove that the total correctness monad is in fact a monad, we used the results of Dawson \cite{dawson-cmkc}, which develop those of Jones \& Duponcheel \cite{jd-cm}. As in \cite{jd-cm}, we consider the composition of two monads $M$ and $N$, but as in Isabelle, we write a type constructor after the type, so the compound monadic type is $\alpha N M$. We write \extNM, \extM, \extN\ for the extension functions of $NM, M$, $N$. % respectively. To get a compound monad, we need the function \extNM, which ``extends'' a function $f$ from a ``smaller'' domain, $\alpha$, to a ``larger'' one, $\alpha N M$. Consider, therefore, a ``partial extension'' function which does part of this job: \begin{align*} \extNM &: (\alpha \to \beta N M) \to (\alpha N M \to \beta N M) \\[-0.5ex] \pext &: (\alpha \to \beta N M) \to (\alpha N \to \beta N M) \end{align*} The following rules and definitions are sufficient to define a compound monad using such a function \pext. % and we also show the definition of \unitNM\ and \extNM\ % for the compound monad in terms of \pext. % \begin{align} \label{E1K'} \pext\ f \oo \unitN & = f \\[-0.5ex] \label{E2K} \pext\ \unitNM & = \unitM \\[-0.5ex] \label{E3'K_o} \pext\ (\extNM\ g \oo f) & = \extNM\ g \oo pext\ f \\ \label{EC} \extNM\ g & = \extM\ (\pext\ g) \\[-0.5ex] \label{UC} \unitNM & = \unitM \oo \unitN \end{align} % We now give the definitions for our particular monads $N = \set$ and $M = \TorN$, the suffix \tc\ indicating the total correctness monad. % These definitions use some auxiliary functions. \begin{align*} \unittc & : \state \to \tcres \\[-0.5ex] \prodtc & : tcres\ \set \to tcres \\[-0.5ex] \pexttc & : (\state \to \tcres) \to \state\ \set \to \tcres \\[-0.5ex] \exttc & : (\state \to \tcres) \to \tcres \to \tcres \end{align*} \begin{align} \unittc\ s & = \Term\ \{s\} \\[-0.5ex] \prodtc\ S & = \NonTerm & \mbox{if $\NonTerm \in S$}\\[-0.5ex] \prodtc\ (\Term ` S) & = \Term\ (\textstyle \bigcup S) \\[-0.5ex] \pexttc\ A\ S & = \prodtc\ (A ` S) \\[-0.5ex] \exttc\ A\ S & = \exto\ (\pexttc\ A)\ S \end{align} % where $\exto$ is the extension function of the $\TorN$ monad (see \cite{dawson-fgc}), given by \begin{align} \exto\ f\ \NonTerm & = \NonTerm \\[-0.5ex] \exto\ f\ (\Term\ s) & = f\ s \end{align} % and $f ` S$ is Isabelle notation for $\{f\ s \,|\, s \in S\}$. % the set obtained by applying the % function $f$ to each member of the set $S$. We have proved, in Isabelle, the following result. We did this by proving rules (\ref{E1K'}) to (\ref{E3'K_o}), noting that (\ref{EC}) and (\ref{UC}) follow directly from our definitions. \begin{theorem} $\sigma\ \set\ \TorN$ is a compound monad. \end{theorem} \comment{ We have proved (see \S \ref{s-tc-pfs}) that these functions satisfy the monad axioms: $$ \begin{array}{rcl@{\qquad \qquad \qquad \qquad}r} \exttc\ k \circ \unittc & = & k & \mbox{(Left Unit)} \\ \exttc\ \unittc & = & id & \mbox{(Right Unit)}\\ \exttc\ (\exttc\ h \circ k) & = & \exttc\ h \circ \exttc\ k & \mbox{\hfill (Assoc)} \end{array} $$ } \subsection{Relation to the outcome set monad} \label{s-tc-pfs} Jones \& Duponcheel \cite{jd-cm} also use a function $\swap : \alpha M N \to \alpha N M$ to define a compound monad. As they show, when such a function \swap\ can be defined, satisfying certain conditions S(1) to S(4), then the compound monad $\alpha N M$ can be constructed. Equivalently, the function $\swap$ is a distributive law for monads, see Barr \& Wells \cite[\S 9.2]{bwttt}. Jones \& Duponcheel also use the function \textit{prod} as above, and give conditions for defining a compound monad in terms of \textit{prod}. % The definition of \swap\ depends on the particular monads $M$ and $N$. In fact the total correctness monad can be defined using \swap. In this case $M$ is the outcome monad, and $N$ is the set monad, and \swap\ is a function \begin{align} \swaptc & : \sigma\ \TorN\ \set \to \sigma\ \set\ \TorN \notag \\ \label{swap_NT} \swaptc\ S & = \NonTerm & \mbox{if $\NonTerm \in S$}\\[-0.5ex] \swaptc\ (\Term ` S) & = \Term\ S \end{align} Here, definition \eqref{swap_NT} reflects the fact that, in total correctness, a command that \emph{may} fail to terminate is equivalent to one which \emph{will} fail to terminate. % as it will not satisfy any post-condition. Our Isabelle proofs included the conditions S(1) to S(4) of \cite{jd-cm}, and so we also have shown that $\swaptc$ is a distributive law for the monads. The function $\swaptc : \sigma\ \TorN\ \set \to \sigma\ \set\ \TorN$ is also a \emph{monad morphism} from the \emph{outcome set} monad to the \emph{total correctness} monad. We have proved the following theorems (which characterise a monad morphism), where \unitos\ and \extos\ are the unit and extension functions for the outcome set monad, as defined in \cite[\S 3.1]{dawson-fgc}: \begin{align*} \unitos & : \state \to \outcome\ \set \\[-0.5ex] \extos & : (\state \to \outcome\ \set) \to \outcome\ \set \to \outcome\ \set \end{align*} \begin{align} \unittc\ a & = \swaptc\ (\unitos\ a) \\[-0.5ex] \exttc\ (\swaptc\ \oo f)\ (\swaptc\ x) & = \swaptc\ (\extos\ f\ x) \end{align} Since this monad morphism is surjective, we could use the fact that the {outcome set} monad satisfies the monad axioms to give an alternative proof to show that the {total correctness} monad also satisfies them. Often, where two monads can be composed to form another monad, the construction depends on one of them, and the other may be arbitrary. Thus, as discussed in \cite[\S 3.1]{dawson-fgc}, the \TorN\ monad % (ie, the type \emph{outcome} relative to the type \emph{state}) can be composed with any other monad $M$ to give a compound monad, which gave the \emph{outcome set} monad. \comment{ In \cite[\S 3.1]{dawson-fgc}, we discussed how, although two monads cannot in general be composed to form another monad, but the \TorN\ monad (ie, the type \emph{outcome} relative to the type \emph{state}) can in general be composed with any other monad to give a compound monad. We used this fact to compose it with the set monad to form the {outcome set} monad. } % In this case we have that the type $\sigma\ \set\ \TorN$ is a monad (relative to $\sigma$), but it does not seem to be an example of a more general construction, in that for an arbitrary monad $M$, neither $\sigma\ M\ \TorN$ nor $\sigma\ \set\ M$ is in general a monad. We also proved the following theorem about abstract commands. Dunne's treatment of general correctness in \cite{dunne-abstr-cmds} includes a definition of total correctness refinement, which is referred to as \verb|totcref| in the result below. This result also confirms that the operational model of \S\ref{s-tcom} is appropriate for total correctness. For two abstract commands $A,B$ (of type $\state \to \outcome\ \set$) the left-hand side says $A \sqsubseteq B$ according to the total-correctness refinement relation for abstract commands, as defined and discussed in \cite{dunne-abstr-cmds} and \cite[\S 3.2]{dawson-fgc}. The right-hand side says that the refinement relation for generalised substitutions holds of the projections of $A$ and $B$ into the type $\state \to \tcres$. % \begin{verbatim} ref_tc_swap = "totcref A B = ref_tc (swap_tc o A) (swap_tc o B)" \end{verbatim} % Often in this work, we drew upon \cite{dawson-fgc}, using the fact that if two abstract commands are equal, then so are their projections into the total correctness monad. \section{The Generalised Substitutions} \label{s-gs} \subsubsection{Frames} Dunne has also defined that each substitution has a \emph{frame}. Loosely, this is the set of variables which ``might'' be affected. Note, however, that $\frm (x := x) = \{x\}$. Also, from any command a new command may be defined which has an enlarged frame but is otherwise the same. Stating the frame of a command does not contribute to a description of what the command, considered in isolation, does. Thus when we show, for example, that two commands behave the same way, we do so without considering their frames. Indeed, the substitution \skp\ and $x := x$ behave the same way, but have different frames. Likewise, it is impossible to deduce the frame of a substitution from its behaviour. The work in this section proceeds on this basis. Therefore the results are therefore subject to the proviso that two generalised substitutions are in fact distinct if their frames differ. On the other hand, the specified frame of a substitution does have an effect in that the parallel composition $S \| T$ depends on the frames of $S$ and $T$ --- that is, if the frames of $S$ or $T$ are extended, then that changes $S \| T$. \subsubsection{Variables} Indeed, for many generalised substitution operations, we do not need to consider variables at all: rather, we can consider a machine state abstractly. For others, we need to consider a state as a map from variables (variable names) to values. As discussed at greater length in \cite{dawson-fgc}, where $Q$ is a predicate on states, we may use the notation $Q[x := E]$ to mean $Q$, with occurrences of $x$ replaced by $E$, when $Q$ is written in the command language, or some similar notation. This is found in the \wp\ rule for assignment, and in the related Hoare logic rule. $$\wp (x := E, Q) = Q[x := E] \qquad \{Q[x := E]\}\ (x := E) \ \{Q\}$$ In fact we could take $Q[x := E]$ to be defined as follows. Considering expression $E$ as a function from states to values, $Q[x := E]\ s = Q\ (s[x := E\ s])$ where, for state $s$, $s[x := E\ s]$ means the function $s$, changed at the domain point $x$. (though using this as a \emph{definition} makes the \wp\ rule above rather trivial, since assignment will be defined to take state $s$ to state $s[x := E\ s]$). \subsection{Meaning of Commands} \label{s-mng} \subsubsection{skip, magic, abort} \cite[\S 3.1, \S 3.3]{dunne-gen-subs} \skp\ is the command which is feasible, terminates and does nothing to the state. It is exactly the function \unittc. It follows immediately from the monad laws \eqref{E1} and \eqref{E2} that \skp\ is an identity for the binary function \seqtc. These are proved in Isabelle as \verb|seq_tc_unitL|/\verb|R|. % and \verb|seq_tc_unitR|. % In \cite{dawson-fgc} we defined \magic\ and \abort\ as shown. %Applying \swaptc\ to these, we get appropriate definitions %for the total-correctness versions, \magictc\ and \aborttc. % \begin{verbatim} % magic st == {} % abort st == {NonTerm} % \end{verbatim} % Applying \swaptc\ to these, we get definitions % for the total-correctness versions. % \begin{verbatim} % "magic_tc s == Term {}" % "abort_tc s == NonTerm" % \end{verbatim} We \emph{define} \magic\ and \abort\ in terms of the operational model, as \verb|magic_tc_def| and \verb|abort_tc_def|; then with these definitions, we then \emph{prove} Dunne's definitions, as \verb|magic_alt| and \verb|abort_alt| (using \verb|precon_tc| and \verb|guard_tc|, see below). % Note that the definition of \abort\ differs from the corresponding % definition in \cite{dunne-abstr-cmds}. As \abort\ always fails to terminate, it fails to satisfy any post-condition. On the other hand, \magic\ is always \emph{infeasible}: while not suffering non-termination, it cannot produce any result which fails to satisfy any given post-condition, so it satisfies every post-condition. % (It is useful as a building-block for more complex substitutions). So we also prove that \magic\ and \abort\ are the top and bottom members in the lattice of generalised substitutions \cite[\S 7]{dunne-gen-subs}. \begin{verbatim} magic_tc_def = "magic_tc s == Term {}" abort_tc_def = "abort_tc s == NonTerm" magic_alt = "magic_tc = guard_tc (%s. False) unit_tc" abort_alt = "abort_tc = precon_tc (%s. False) unit_tc" top_magic_tc = "ref_tc C magic_tc" bot_abort_tc = "ref_tc abort_tc C" \end{verbatim} \subsubsection{preconditioned command, guarded command} \cite[\S 3.1]{dunne-gen-subs} The preconditioned command $P | A$ is the same as $A$ except that, if $P$ does not hold, then $P | A$ need not terminate. The guarded command $P \Longrightarrow A$ is the same as $A$ if $P$ holds, but is \emph{infeasible} (it cannot reach any outcome, that is, it cannot run) if $P$ does not hold. Dunne defines both of these by giving the formula for their weakest precondition. We define them using \verb|precon_tc_def| and \verb|guard_tc_def|, and then prove Dunne's definitions as \verb|precon_wp_tc'| and \verb|guard_wp_tc|. \begin{verbatim} precon_tc_def = "precon_tc P C s == if P s then C s else NonTerm" guard_tc_def = "guard_tc P C s == if P s then C s else Term {}" precon_wp_tc' = "wp_tc (precon_tc P C) Q s = (P s & wp_tc C Q s)" guard_wp_tc = "wp_tc (guard_tc P C) Q s = (P s --> wp_tc C Q s)" \end{verbatim} \subsubsection{termination, feasibility} \cite[\S 5]{dunne-gen-subs} We define \begin{verbatim} "trm_tc C s == C s ~= NonTerm" "fis_tc C s == C s ~= Term {}" \end{verbatim} % NO SPACE HERE We can then prove Dunne's definition of \textit{trm} and \textit{fis}, and his results in \cite[\S 5]{dunne-gen-subs}: \begin{verbatim} trm_alt = "trm_tc C = wp_tc C (%s. True)" fis_alt = "fis_tc C = Not o wp_tc C (%s. False)" pc_trm_tc = "precon_tc (trm_tc A) A = A" fis_guard_tc = "guard_tc (fis_tc A) A = A" strongest_guard = "(guard_tc g A = A) = (fis_tc A ---> g)" strongest_pc = "(precon_tc pc A = A) = (trm_tc A ---> pc)" \end{verbatim} \subsubsection{sequencing} \cite[\S 3.1]{dunne-gen-subs} As mentioned earlier, we define sequencing of commands using \exttc, as shown in \verb|seq_tc_def|. Dunne defines it by giving the weakest precondition of $A ; B$, and we prove this result, as \verb|seq_wp_tc|, from our definition. \begin{verbatim} seq_tc_def = "seq_tc A B == ext_tc B o A" seq_wp_tc = "wp_tc (seq_tc A B) Q = wp_tc A (wp_tc B Q)" \end{verbatim} \subsubsection{choice} \label{s-choice} In \cite[\S 3.1]{dunne-gen-subs} Dunne defines a binary operator, $A \Box B$, for \emph{bounded choice}: $A \Box B$ is a command which can choose between two commands $A$ and $B$. Again, Dunne defines this by giving its weakest precondition. This is a special case of choice among an arbitrary set of commands. In the total correctness setting, where \choice\tc\ $\Cs$ can fail to terminate if any $C \in \Cs$ can fail to terminate, we define \choice\tc\ as shown below. As the definition is rather unintuitive, we show the types of some of its parts. % constituent parts. Recall that if the type $\sigma$ represents the machine state, then a command has type $\sigma \to \sigma\ \set\ \TorN$. The definition is unintuitive perhaps because where \pext\ is used (indirectly) in defining sequencing of commands, the types $\alpha$ and $\beta$ are both the state type $\sigma$. But in the use of \pext\ below, $\alpha$ is the type of commands. % \begin{align*} \choice\tc\ \Cs\ s & = \pext\ (\lambda C.\ C\ s)\ \Cs \\ \choice\tc & : (\sigma \to \sigma\ \set\ \TorN)\ \set \to \sigma \to \sigma\ \set\ \TorN \\[-0.5ex] \pext\ & : (\alpha \to \beta\ \set\ \TorN) \to \alpha\ \set \to \beta\ \set\ \TorN \\[-0.5ex] \lambda C.\ C\ s & : (\sigma \to \sigma\ \set\ \TorN) \to \sigma\ \set\ \TorN \\[-0.5ex] \pext\ (\lambda C.\ C\ s) & : (\sigma \to \sigma\ \set\ \TorN)\ \set \to \sigma\ \set\ \TorN \end{align*} % When the definition is expanded (\verb|choice_tc_def''| in the Isabelle proofs), it shows that if $\{C\ s \,|\, C \in \Cs\}$ contains \NonTerm\ then $\choice\tc\ \Cs\ s = \NonTerm$; if $\{C\ s \,|\, C \in \Cs\} = \{\Term\ S_C \,|\, C \in \Cs\}$, then $\choice\tc\ \Cs\ s = \Term (\bigcup_{C \in \Cs} S_C)$. We obtained the following results, relating the distribution of sequencing over choice. The theorem \verb|seq_choice_tcL| was obtained as an easy corollary of rule \eqref{E3'K_o}, obtained in the course of the proofs about the total correctness monad. We also proved a result giving the weakest precondition of \choice\tc, which is the generalisation of Dunne's definition of $A \Box B$, and from which it easily follows that $\choice\tc\ \Cs$ is the glb of the set $\Cs$. Proposition~7 of \cite[p288]{dunne-gen-subs} follows. \begin{verbatim} seq_choice_tcL = "seq_tc (choice_tc Cs) B = choice_tc ((%C. seq_tc C B) ` Cs)" seq_choice_tcR = "Cs ~= {} ==> seq_tc A (choice_tc Cs) = choice_tc (seq_tc A ` Cs)" choice_wp_tc = "wp_tc (choice_tc Cs) Q s = (ALL C:Cs. wp_tc C Q s)" choice_glb_tc = "ref_tc A (choice_tc Cs) = (ALL C:Cs. ref_tc A C)" \end{verbatim} % pext_tc_fun = "pext_tc (ext_tc g o f) = ext_tc g o pext_tc f" \comment{ \subsubsection{sequencing} \cite[\S 3.1]{dunne-gen-subs} As mentioned earlier, we define sequencing of commands using \exttc, as shown in \verb|seq_tc_def|. Dunne defines it by giving the weakest precondition of $A ; B$, and we prove this result, as \verb|seq_wp_tc|, from our definition. \begin{verbatim} seq_tc_def = "seq_tc A B == ext_tc B o A" seq_wp_tc = "wp_tc (seq_tc A B) Q = wp_tc A (wp_tc B Q)" \end{verbatim} } \comment{ \subsubsection{termination, feasibility} \cite[\S 5]{dunne-gen-subs} We define \begin{verbatim} "trm_tc C s == C s ~= NonTerm" "fis_tc C s == C s ~= Term {}" \end{verbatim} % NO SPACE HERE We can then prove Dunne's definition of \textit{trm} and \textit{fis}, and his results in \cite[\S 5]{dunne-gen-subs}: \begin{verbatim} trm_alt = "trm_tc C = wp_tc C (%s. True)" fis_alt = "fis_tc C = Not o wp_tc C (%s. False)" pc_trm_tc = "precon_tc (trm_tc A) A = A" fis_guard_tc = "guard_tc (fis_tc A) A = A" strongest_guard = "(guard_tc g A = A) = (fis_tc A ---> g)" strongest_pc = "(precon_tc pc A = A) = (trm_tc A ---> pc)" \end{verbatim} } We note that for many generalised substitutions, the definition may be obtained by translation from the definitions in \cite{dawson-fgc} for abstract commands. For example, for \choice\tc\ we could have defined \choice\tc\ \Cs\ in terms of \choice\ \As\ for any set \As\ of abstract commands corresponding to the set \Cs\ of generalised substitutions. % Alternatively, we can relate our definitions to the definitions of the corresponding abstract commands, where % \verb|magic|, \verb|abort|, \verb|precon|, \verb|guard|, \verb|choice|, % \verb|trmm| and \verb|fis| are the corresponding operations \verb|seq|, \verb|precon|, \verb|guard| and \verb|choice| are the corresponding operations on abstract commands: \cite[\S 3.4]{dawson-fgc}. \begin{verbatim} seq_tc = "seq_tc (swap_tc o A) (swap_tc o B) = swap_tc o seq A B" precon_tc = "precon_tc P (swap_tc o A) = swap_tc o precon P A" guard_tc = "guard_tc P (swap_tc o A) = swap_tc o guard P A" choice_tc = "choice_tc (op o swap_tc ` As) = swap_tc o choice As" \end{verbatim} where \verb|(op o swap_tc ` As)| means $\{\swaptc\ \circ\ A \;|\; A \in As\}$ (We have similar results for \verb|magic_tc|, \verb|abort_tc|, \verb|trm_tc| and \verb|fis_tc| also). These results enable us to prove many results for generalised substitutions from the corresponding results for abstract commands. In some cases, such as for the theorem \verb|choice_wp_tc|, this provided much simpler proofs in Isabelle. \subsection{Monotonicity} \label{s-mon} For developing a program by starting with a generalised substitution (expressing a program specification), and progressively refining it to a concrete program, it is important that the generalised substitution constructors are monotonic with respect to the refinement relation ($\sqsubseteq$). % All the constructors mentioned are monotonic. We proved these results in Isabelle as (for example) \begin{verbatim} seq_tc_ref_mono = "[| ref_tc A1 B1; ref_tc A2 B2 |] ==> ref_tc (seq_tc A1 A2) (seq_tc B1 B2)" rephat_ref_mono = "ref_tc A B ==> ref_tc (rephat A) (rephat B)" \end{verbatim} \comment{ \subsubsection{concert} COULD ABBREVIATE OR DELETE In \cite[\S 12]{dunne-abstr-cmds} Dunne describes the command $A \# B$, which represents $A$ and $B$ executing independently, on separate copies of the state: whichever of $A$ or $B$ terminates first gives the effect of $A \# B$. We now describe why the total correctness framework does not accommodate a corresponding generalised substitution. As a command producing outcome sets, the possible outcomes of $A \# B$ are: \begin{itemize} \item \verb|Term| $s$, if it is an outcome of $A$, \item \verb|Term| $s$, if it is an outcome of $B$, \item \NonTerm, if it is an outcome of \emph{both} $A$ and $B$. \end{itemize} When we try to translate this into the total correctness framework, the only plausible definition is that $A \# B$ equals \begin{itemize} \item \Term\ $(S_A \cup S_B)$, if $A\ s = \Term\ S_A$ and $B\ s = \Term\ S_B$, \item \Term\ $S_A$, if $A\ s = \Term\ S_A$ and $B\ s = \NonTerm$, \item \Term\ $S_B$, if $A\ s = \NonTerm$ and $B\ s = \Term\ S_B$, \item \NonTerm, if $A\ s = B\ s = \NonTerm$ \end{itemize} We define \verb|concert_ct| in this way. However, this definition fails to account for a command $A$ (or $B$) which can (from a particular state $s$) either terminate or fail to do so. For in such a case, the set of states in which it can terminate do not appear in the definition of the result. This command illustrates the greater expressive power of general correctness as compared with total correctness alone, as argued by Dunne \cite{dunne-abstr-cmds}. Thus we cannot get a result corresponding to \verb|choice_tc|. However we can get a weaker result, where we obtain $A \# B$ by making a particular choice of abstract commands $A'$ and $B'$ corresponding to the generalised substitutions $A$ and $B$. The abstract commands we choose are the ones which, for a given start state, either terminate or not --- they cannot non-deterministically choose whether to terminate or not: $A' = \swapi \circ A$ and $B' = \swapi \circ B$ where $$\swapi\ \NonTerm = \{\NonTerm\} \qquad \swapi\ (\Term\ S) = \Term\ `\ S$$ and $\Term\ `\ S$ is Isabelle notation for $\{\Term\ s \,|\, s \in S\}$. Then the result is, where \verb|conc| is the concert operation for abstract commands, \begin{verbatim} concert_tc = "concert_tc A B = swap_tc o conc (swapi o A) (swapi o B)" \end{verbatim} Note that \swapi, which is a one-sided inverse of \swaptc, is not a monad morphism, but it does satisfy the axioms for a swap function, and can be used to define the compound monad for the general correctness case. We also find that \verb|concert_tc| is not monotonic. The following theorem shows a counterexample. \begin{verbatim} conc_tc_not_ref_mono = "[| A2 = magic_tc; B2 = magic_tc; A1 = abort_tc; B1 = unit_tc |] ==> ~ (ref_tc A1 B1 --> ref_tc A2 B2 --> ref_tc (concert_tc A1 A2) (concert_tc B1 B2))" \end{verbatim} } \subsection{Repetition and Iteration for the General Correctness Model} \label{s-rigc} In \cite[\S 7]{dunne-abstr-cmds} Dunne defined $A^0 = \skp$ and $A^{n+1} = A ; A^n$, and we proved that $A^{n+1} = A^n ; A$. From this we defined $\repall\ A\ s = \bigcup_n A^n s$, that is, $\texttt{repall}\ A$ is the (unbounded) choice of any number $n$ of repetitions of $A$; % The termination condition for $\texttt{repall}\ A$ is that it terminates iff for every $n$, $A^n$ terminates (proved as \verb|repall_term|). In \cite[\S 12]{dunne-abstr-cmds} Dunne defined the \emph{repetitive closure} $A^{*}$ of $A$, where the outcomes of $A^{*}$ are those of \verb|repall|, augmented by \NonTerm\ in the case where it is feasible to execute $A$ infinitely many times sequentially (calling this an ``infinite chain''). Thus, in \cite[\S 3.5]{dawson-fgc} we defined a function \infch, where $\infch\ A\ s$ means that it is possible to execute $A$ infinitely many times sequentially, starting in state $s$. So we had the following definition, from which we proved various results from \cite{dunne-abstr-cmds}, including characterisations of \verb|repall| and \verb|repstar| as fixpoints. \begin{verbatim} repstar C state == repall C state Un (if infch C state then {NonTerm} else {}) \end{verbatim} % \begin{description} % \item[\texttt{seq\_repstar} :] $A^* ; A = A ; A^*$ % \end{description} \subsubsection{A Coinductive Definition} In \cite[\S 3.5]{dawson-fgc} we defined the concept of an infinite chain explicitly, in terms of the existence of an infinite sequence of states through which the executing program can pass. Some of these Isabelle proofs involving this definition were quite difficult. Subsequently we used Isabelle's coinductive definition facility to give a more elegant definition of an equivalent notion: $\infchs\ A$ is the set of states from which it is possible to execute $A$ infinitely many times sequentially. We also defined inductively a set $\icnt\ A$, which we showed is equivalent to $\{s \,|\, \NonTerm \in A^*\ s\}$. The Isabelle definitions are: \begin{verbatim} coinductive "infchs A" intros I : "Term ns : A s ==> ns : infchs A ==> s : infchs A" coinductive "icnt A" intros NTI : "NonTerm : A s ==> s : icnt A" icI : "Term ns : A s ==> ns : icnt A ==> s : icnt A" \end{verbatim} This defines $\infchs\ A$ to be the unique maximal set satisfying $$ \infchs\ A = \{s \,|\, \exists s'.\ \Term\ s' \in A\ s \land s' \in \infchs\ A\} $$ Then Isabelle's coinductive definition facility provides a coinduction principle: $$ \frac {a \in X \qquad \forall z. z \in X \Rightarrow \exists s'. \Term\ s' \in A\ z \land s' \in X \cup \infchs\ A} {a \in \infchs\ A} $$ and similarly for \icnt. We then proved that $s \in \infchs\ A$ if and only if $\infch\ A\ s$ holds, and that $s \in \icnt\ A$ if and only if $\NonTerm \in A^*\ s$. This made some other proofs considerably easier than before. \subsection{Repetition and Iteration for the Total Correctness Model} \label{s-ritc} For the total correctness model we used analogous definitions. We used a coinductive definition to define $\infchs\tc\ C$, the set of states from which it is possible to execute $C$ infinitely many times sequentially and an inductive definition for $\reachnt\ C$, the set of states from which \NonTerm\ is reachable. \begin{verbatim} coinductive "infchs_tc C" intros "C s = Term S ==> ns : S ==> ns : infchs_tc C ==> s : infchs_tc C" inductive "reach_NT C" intros "C s = NonTerm ==> s : reach_NT C" "C s = Term S ==> ns : S ==> ns : reach_NT C ==> s : reach_NT C" \end{verbatim} Then we define $\icnt\tc\ C$, using the same introduction rules as for $\reachnt\ C$, but in a coinductive definition, not an inductive definition. We then prove that $\icnt\tc\ C = \reachnt\ C \cup \infchs\tc\ C$, and can relate \icnt\tc\ to \icnt. \begin{verbatim} icnt_alt = "icnt_tc C = reach_NT C Un infchs_tc C" icnt_tc = "icnt_tc (swap_tc o A) = icnt A" \end{verbatim} Also using an inductive definition, we define \texttt{treach A s} to be the set of states reachable from \verb|s| using \verb|A| repeatedly. In \cite[\S 8.2]{dunne-gen-subs} Dunne defines the generalised substitution $C^\wedge$. He \emph{defines} it as the least fixed point in the refinement ordering $\mu X.\ (C ; X) \Box \skp$. For us to define it in that way would require showing that the least fixed-point exists: in \cite[\S 8.1]{dunne-gen-subs} Dunne discusses why this result holds. Rather than proving this result in Isabelle, we \emph{define} $C^\wedge$ using the operational interpretation (suggested in \cite[\S 8.2]{dunne-gen-subs}) that the result of $C^\wedge$ is the states reachable by repeating $C$, % represents any feasible number of repetitions of $C$, but with the result \NonTerm\ either if \NonTerm\ is reachable by repeating $C$ or if an infinite sequence of executions of $C$ is possible. We then \emph{proved} that $C^\wedge$, defined thus, is in fact the least fixed-point of $\lambda X.\ (C ; X) \Box \skp$. The proofs were more difficult than the corresponding ones for abstract commands, mentioned in \cite{dawson-fgc}, and it was necessary to use a range of lemmas, including some of those mentioned in \S \ref{s-tcmon}. We can relate the total correctness repetition constructs to those for general correctness, using \swap\tc\ (for example, \verb|rephat_star| below). We proved Dunne's examples, $\magic^\wedge$ and $\skp^\wedge$. % We also defined functions \verb|rep_tc| and \verb|repall_tc|, % used to show that $C^\wedge$ could instead have been defined analogously % to $A^{*}$ (see \S\ref{s-rigc}). % We also showed that $C^\wedge$ could instead have been defined analogously % to $A^{*}$ (see \S\ref{s-rigc}); % to do this we defined a function \verb|repall_tc|, analogous to \repall. We also defined a function \verb|repall_tc|, analogously to \repall\ (see \S\ref{s-rigc}), and showed that $C^\wedge$ could instead have been defined, analogously to $A^{*}$, using it. Among the following, \verb|rephat_def| and \verb|fprep_tc_def| are definitions. \begin{verbatim} rephat_def = "rephat C state == if state : icnt_tc C then NonTerm else Term (treach C state)" fprep_tc_def = "fprep_tc A X == X = choice_tc {seq_tc A X, unit_tc}" rephat_isfp = "fprep_tc A (rephat A)" rephat_is_lfp = "fprep_tc A Y ==> ref_tc (rephat A) Y" rephat_star = "rephat (swap_tc o A) s = swap_tc (repstar A s)" rephat_magic = "rephat magic_tc = unit_tc" rephat_skip = "rephat unit_tc = abort_tc" \end{verbatim} Dunne then defines the \iif\ and \while\ constructs as follows \cite[\S 9]{dunne-gen-subs}: \begin{eqnarray*} \iif\tc\ G\ \then\ S\ \els\ T\ \eend & \equiv & (G \Longrightarrow S) \,\Box\, (\lnot G \Longrightarrow T) \\ % \iif\tc\ G\ \then\ S\ \eend & \equiv & % (G \Longrightarrow S) \,\Box\, (\lnot G \Longrightarrow \skp) \\ \while\tc\ G\ \ddo\ S\ \eend & \equiv & (G \Longrightarrow S)^\wedge \,;\, \lnot G \Longrightarrow \skp \end{eqnarray*} From these we are then able to prove an alternative definition for \iif\ and the usual programming definition for \while: \begin{verbatim} if_tc_prog = "if_tc G A B s = (if G s then A s else B s)" ifthen_tc_prog = "ifthen_tc G A s = (if G s then A s else Term {s})" while_tc_prog = "while_tc G A = ifthen_tc G (seq_tc A (while_tc G A))" \end{verbatim} \subsection{The \prd\ predicate} \cite[\S 5]{dunne-gen-subs} \label{s-prd} The ``before-after'' predicate \prd\ relates the values of the variables in the frame before execution of the command to their values after the command. It is defined in \cite[\S 5]{dunne-gen-subs} as $\prd\ (S) \equiv \lnot [S] (s \not = s')$ where $s = \frm(S)$ and $s'$ are new (logical) variables corresponding to the program variables $s$. Implicitly, $\prd\ (S)$ depends on $s'$; $(s \not = s')$ is a post-condition on the values of $s$ after executing $S$. First we define \verb|prd_tc| which assumes that the frame consists of all variables. Then, for the analysis of \verb|prd_tc|, it is possible to treat the state as abstract. \begin{verbatim} "prd_tc s' C == Not o wp_tc C (%s. s ~= s') \end{verbatim} where \verb|s'|, of type \textit{state}, represents the values $s'$. We note a difference between the definitions of \cite[\S 6]{dunne-gen-subs} and \cite[\S 10]{dunne-abstr-cmds}: in the former, if $S$ does not terminate from state $s$, then $\prd(S) s$ \emph{does} hold. As a sort of inverse to this definition, we derived \verb|wp_prd_tc|, an expression for \wp\ in terms of \prd, namely $[S] Q = \trm\ S \land \forall s'.\ \prd (S) \to Q$. This was suggested by a similar result in \cite[\S 10]{dunne-abstr-cmds}. We also derived \cite[\S 13, p287, Proposition~7]{dunne-gen-subs} as \verb|ref_tc_prdt|. \begin{verbatim} wp_prd_tc = "wp_tc A Q s = (trm_tc A s & (ALL s'. prd_tc s' A s --> Q s'))" ref_tc_prdt = "ref_tc A B = ((trm_tc A ---> trm_tc B) & (ALL s'. prd_tc s' B ---> prd_tc s' A))" \end{verbatim} \subsection{The least upper bound} \cite[\S 7]{dunne-gen-subs} \label{s-lub} In \S \ref{s-choice} we showed that, in the refinement ordering, the greatest lower bound of a set of commands is given by the \choice\ command. To describe the least upper bound $\lub\ S\ T$ of $S$ and $T$ is more difficult. We might expect that $[\lub\ S\ T]\ Q = [S] Q \lor [T] Q$ but this is not so. For if $S\ x = \Term\ \{y_S\}$ and $T\ x = \Term\ \{y_T\}$, where $y_S \not= y_T$, then $(\lub\ S\ T)\ x = \Term\ \{\}$ and so $[\lub\ S\ T]\ Q\ x$ holds. But if neither $Q\ y_S$ nor $Q\ y_T$ hold, then $([S] Q \lor [T] Q)\ x$ does not hold. However in \cite[\S 7]{dunne-gen-subs} Dunne gives a characterisation of the least upper bound of the set of generalised substitutions on a given frame: we prove this result, applied to a set of abstract states, as \verb|lub_tc|. As a corollary of this general result, we get \verb|ACNF_tc|, giving Dunne's normal form, \cite[\S 11, Proposition~4]{dunne-gen-subs}, again in terms of abstract states. These results use the functions \verb|at_tc| and \verb|pc_aux|. The function \verb|at_tc| is analogous to \verb|atd| of \cite[\S 4.2]{dawson-fgc}, and is used to express Dunne's unbounded choice over a set of logical variables. The function \verb|pc_aux_tc| is used here and in \S 7, and $\pcaux\ \Cs\ s = \Term\ S$, where $S$ consists of those states which every $C \in \Cs$ can reach from initial state $s$ % (our Isabelle result stating this is \verb|pc_aux_alt2|). (we proved this in Isabelle as \verb|pc_aux_alt2|). \begin{verbatim} at_tc_def = "at_tc Ad == choice_tc (range Ad)" pc_aux_def = "pc_aux Cs == at_tc (%s'. guard_tc (%s. ALL C:Cs. prd_tc s' C s) (%s. Term {s'}))" lub_tc = "ref_tc (precon_tc (%s. EX C:Cs. trm_tc C s) (pc_aux Cs)) A = (ALL C:Cs. ref_tc C A)" ACNF_tc = "A = precon_tc (trm_tc A) (at_tc (%s'. guard_tc (prd_tc s' A) (%s. Term {s'})))" \end{verbatim} % pc_aux_alt2 = % "pc_aux Cs s = Term (Inter (sts_of_ocs ((%C. C s) ` Cs)))" %MAY NOT WANT TO INCLUDE THIS LOT Having found the least upper bound of a set of generalised substitutions using the function \verb|pc_aux|, we now derive an expresson for weakest precondition of \verb|pc_aux| \Cs\ in terms of $\{[C] \,|\, C \in \Cs\}$, using a function we called \verb|lub_pt|. We then proved that \verb|lub_pt| gives the least upper bound % (or greatest lower bound, depending on how you define the ordering) of a set of predicate transformers, provided that they are conjunctive (and so monotonic). This is not enough to deduce that \verb|pc_aux| \Cs\ is the least upper bound of \Cs\ since weakest precondition functions fail to be conjunctive, where non-termination is involved. % but only conjunctive in relation to non-empty sets of postconditions. Thus the theorem \verb|lub_tc| contains the termination precondition. In \S\ref{s-hc} we discuss how generalised substitutions correspond to predicate transformers satisfying the non-empty conjunctivity condition. Here \verb|mono_pt| $T$ means that $T$ is monotonic. and \verb|conj_pt| $T$ \Qs\ $s$ means that $T$ is conjunctive in relation to a given set \Qs\ of predicates and state $s$. % (Including \verb|Qs| and \verb|s| in the definition makes it easier to % apply these results, since the weakest precondition predicate transformer % is conjunctive only for non-empty sets of predicates, % or where the generalised substitution in question terminates.) The results \verb|lub_pt_lub|, \verb|lub_pt_ub| and \verb|lub_pt_is_conj|, together show that, among conjunctive predicate transformers, \verb|lub_pt| gives the least upper bound. \begin{verbatim} pc_aux_wp = "wp_tc (pc_aux Cs) = lub_pt (wp_tc ` Cs)" lub_pt_def = "lub_pt Ts Q x == ALL Q':Qcs Q. EX T:Ts. T Q' x" Qcs_def = "Qcs Q == (%y x. x ~= y) ` (- Collect Q)" lub_pt_lub = "[| ALL Qs. conj_pt T Qs s; ALL U:Us. ALL Q. U Q s --> T Q s; lub_pt Us Q s |] ==> T Q s" lub_pt_ub = "[| mono_pt T; T : Ts |] ==> T Q ---> lub_pt Ts Q" lub_pt_is_conj = "conj_pt (lub_pt Ts) Qs s" conj_pt_def = "conj_pt T Qs s == T (%s. ALL Q:Qs. Q s) s = (ALL Q:Qs. T Q s)" \end{verbatim} \subsection{Parallel Composition} \cite[\S 6]{dunne-gen-subs} \label{s-pc} Here we describe this in the case where the frames of the commands are the set of all program variables. This enables us to treat the machine state abstractly. We define the parallel composition according to Dunne's informal description: $S || T$ can terminate in a state $s$ only if both $S$ and $T$ can terminate in $s$ (but we define parallel composition of an arbitrary set of generalised substitutions). The ``\verb|else|'' part of \verb|pcomprs_tc| amounts to % \verb|pcomprs_tc| $\{\Term\ S \,|\, S \in \Ss\} = \Term\ (\bigcap\ \Ss)$. \verb|pcomprs_tc| $(\Term\ ` \Ss) = \Term\ (\bigcap\ \Ss)$. From this we then derive Dunne's definition, \verb|pcomp_tc_alt|. We then derive the further results given in \cite[\S 6]{dunne-gen-subs}, and also \verb|prd_pcomp_tc|, a variant of his expression for $\prd(S||T)$ which generalises directly to give the parallel composition of an arbitrary set of generalised substitutions. \begin{verbatim} pcomp_tc_def = "pcomp_tc Cs s == pcomprs_tc ((%C. C s) ` Cs)" pcomprs_tc_def = "pcomprs_tc rs == if NonTerm : rs then NonTerm else Term (Inter (sts_of_ocs rs))" pcomp_tc_alt = "pcomp_tc Cs == precon_tc (%s. ALL C:Cs. trm_tc C s) (pc_aux Cs)" trm_pcomp_tc = "trm_tc (pcomp_tc Cs) s = (ALL C:Cs. trm_tc C s)" prd_pcomp_tc = "prd_tc s' (pcomp_tc Cs) s = (trm_tc (pcomp_tc Cs) s --> (ALL C:Cs. prd_tc s' C s))" prd_pcomp_tc2 = "prd_tc s' (pcomp_tc {A, B}) s = ((trm_tc B s --> prd_tc s' A s) & (trm_tc A s --> prd_tc s' B s))" pcomp_choice_tc = "pcomp_tc {B, choice_tc (insert A As)} = choice_tc ((%a. pcomp_tc {B, a}) ` insert A As)" \end{verbatim} \subsection{Healthiness Conditions and positive conjunctivity} \cite[\S 10.1]{dunne-gen-subs} \label{s-hc} Dunne asks whether any choice of frame and predicate transformer gives a generalised substitution. He gives three necessary conditions, that is, properties of generalised substitutions. Of these, (GS1) is relevant only when the definitions of $\frm(S)$ and $[S]$ are given at a syntactic level --- they must then be well-defined at the semantic level. Here we are working at the semantic level. Condition (GS3) in effect says that a generalised substitution has no effect outside its frame. However, we look at condition (GS2) which says that a generalised substitution $[S]$ distributes through all non-empty conjunctions (of post-conditions): we prove this as \verb|wp_tc_gen_conj|. Given a predicate transformer $T$, the result \verb|ACNF_tc| enables us to determine the generalised substitution $C$ such that, if $T$ is a weakest precondition, then $T = [C]$. This gives us the definition \verb|gs_of_pt_def| and the theorem \verb|gs_of_pt|. We then prove (as \verb|pt_gc_gs|) that if $T$ is any predicate transformer satisfying the non-empty conjunctivity condition, then $T = [\texttt{gs\_of\_pt}\ T]$. That is, the generalised substitutions correspond to the predicate transformers satisfying the non-empty conjunctivity condition. \begin{verbatim} wp_tc_gen_conj = "Q : Qs ==> wp_tc C (%s. ALL Q:Qs. Q s) s = (ALL Q:Qs. wp_tc C Q s)" gs_of_pt_def = "gs_of_pt T == precon_tc (T (%s. True)) (at_tc (%s'. guard_tc (Not o T (%st. st ~= s')) (%s. Term {s'})))" gs_of_pt = "T = wp_tc C ==> C = gs_of_pt T" pt_gc_gs = "[| ALL Q Qs s. Q : Qs --> conj_pt T Qs s; C = gs_of_pt T |] ==> T = wp_tc C" \end{verbatim} \subsection{Properties of Substitutions} \label{s-ps} We proved the results of Proposition~1 of \cite[\S 10.2]{dunne-gen-subs}, and of Proposition~2 (shown). \begin{verbatim} trm_or_prd_tc = "trm_tc S s | prd_tc s' S s" prd_tc_imp_fis = "prd_tc s' S ---> fis_tc S" fis_or_wp_tc = "fis_tc S s | wp_tc S Q s" wp_imp_trm_tc = "wp_tc S Q ---> trm_tc S" \end{verbatim} % OMIT NEXT SENTENCE TO SAVE SPACE Our Isabelle proofs of other results of Dunne \cite{dunne-gen-subs} are listed in the Appendix. \section{Frames and Variable Names} \label{s-fvn} So far, we have viewed a command as a function from a state to either \NonTerm\ or a set of new states, and a condition as a predicate on states. In this treatment, the view of a state was abstract. However, as in \cite[\S 4]{dawson-fgc}, we also need to discuss frames, and the values of program variables. % In this section we discuss those abstract command constructors which % require us to address these issues. In our Isabelle model, as in \cite[\S 4]{dawson-fgc}, the program variable names are of type \verb|'n| (eg, strings) and they take values of type \verb|'v|, where \verb|'n| and \verb|'v| are Isabelle type variables. As a state is an assignment of variables to values, we have the type definition $\state = \name \to \val$, or, in Isabelle, \verb|state = "'n => 'v"|. % \subsection{Frames} \label{s-fr} In Dunne's formulation \cite[\S 7]{dunne-abstr-cmds}, each generalised substitution comes decorated with a frame, and the frame of the new command is defined individually for each generalised substitution constructor: for example $$\frm\ (A \Box B) = \frm\ (A || B) = \frm(A) \cup \frm(B)$$ However we are unable to give an exact semantic meaning to the frame in a similar sense to the meaning we have given to commands so far. The frame may be thought of as a set of variables ``potentially'' set by a command, but it can be larger than the set of variables actually set by the command. The frame may be smaller than the set of variables read by the command, and two commands which have the same operational behaviour can have different frames. This means that whereas we can deduce the weakest precondition of a generalised substitution from its operational behaviour, we cannot deduce its frame. (We could confirm that it does not change variables outside its defined frame, but this seems straightforward, and we have not done it in Isabelle). Certain of Dunne's results involving frames can be seen to follow easily from the results earlier which treat the state abstractly. Thus, to see Proposition~4 in its full generality, you consider the state as consisting of only the variables in the frame, and apply the theorem \verb|ACNF_tc|. Similarly to get Dunne's characterisation of the lub of two generalised substitutions with the same frame $u$, you just apply \verb|lub_tc| to the state consisting only of the variables in $u$. We now describe how to express some of Dunne's other results involving frames, and prove them. The condition $x \setminus Q$ is defined to mean that no variable of $x$ appears free in $Q$. Since we view $Q$ semantically rather than syntactically, we defined \verb|indep| $x$ $Q$ to be the condition that changing the value, in a state $s$, of a variable in $x$ does not change $Q\ s$. In proving these results we also rely on the fact that a generalised substitution $S$ does not change variables outside $\frm(S)$. So we defined \verb|frame_tc| $S$ $F$ to mean that $F$ \emph{could} be the frame of $S$, ie, that $S$ does not change variables outside $F$. In this way we proved the frame circumscription result \cite[\S 10.1, (GS3)]{dunne-gen-subs}, and \cite[Proposition~3]{dunne-gen-subs}. Note that $(Q\ \texttt V\ R)\ s \equiv Q\ s \lor R\ s$ and $(Q\ \texttt{\&\&}\ R)\ s \equiv Q\ s \land R\ s$. \begin{verbatim} GS3 = "[| frame_tc S F; indep F Q |] ==> wp_tc S Q s = (trm_tc S s & (fis_tc S s --> Q s))" prop3 = "[| frame_tc S F; indep F R |] ==> wp_tc S (Q V R) = (wp_tc S Q V trm_tc S && R)" \end{verbatim} \comment{ FOLLOWING FROM CATS PAPER \subsubsection{parallel composition} \cite[\S 12]{dunne-abstr-cmds} This is the only abstract command operator whose meaning depends on the frames of its operands. The command $A || B$ executes $A$ and $B$, independently, each on its own copy of the variables in its frame, and waits until both have terminated. (Thus, non-termination is a possible outcome of $A || B$ if it is possible for either $A$ or $B$). We say a new state resulting from $A$ is \emph{compatible} with a new state resulting from $B$ if these new states agree on the values they give to the variables in $\fram (A) \cap \fram (B)$. Then, for each $(s_A, s_B)$, where $s_A$ and $s_B$ are compatible new states resulting from $A$ and $B$ respectively, there is an outcome $\texttt{Term}\ s_{AB}$ of $A || B$, where $s_{AB}$ is given by: \begin{itemize} \item the new values of variables in $\fram (A) \cap \fram (B)$ are as in $s_A$ (or $s_B$), \item the new values of variables in $\fram (A) \backslash \fram (B)$ are as in $s_A$, and \item the new values of variables in $\fram (B) \backslash \fram (A)$ are as in $s_B$. \end{itemize} Dunne defines $A || B$ by \begin{eqnarray*} \trm (A || B) & = & \trm (A) \land \trm (B) \\ \prd (A || B) & = & \prd (A) \land \prd (B) \end{eqnarray*} but the latter formula contains an implicit reference to the frames of the commands. It is interesting to note that if $A$ is infeasible, and $B$ is feasible but does not terminate, then $A || B$ is feasible but does not terminate. We consider first a version of this command for which the frame is the entire set of variables, defined by \verb|pcomp_def| and \verb|pcomprs_def| ; for these, we prove the formulae just mentioned, as \verb|pcomp_prd| and \verb|pcomp_trm|. We also prove as, \verb|pcomp_wlp|, a result (communicated by Dunne) $$\wlp\;(A || B)\;Q\;s = \exists Q_1 \;Q_2. (\forall t. Q_1\;t \land Q_2\;t \Rightarrow Q\;t) \land \wlp(A,Q_1)\;s \land \wlp(B,Q_2)\;s$$ Unusually, we have explicitly referred to states $s$ and $t$ in this statement of the result to emphasize that the choice of $Q_1$ and $Q_2$ depends on the state $s$. % % \begin{verbatim} % pcomp_def = "pcomp A B state == % pcomprs (A state) (B state)" % % pcomprs_def = "pcomprs cr1 cr2 == % cr1 Int cr2 Un {NonTerm} Int (cr1 Un cr2)" % \end{verbatim} The following definition of $A || B$ takes into account the frames of $A$ and $B$. Firstly, \verb|pccomb| combines two states (resulting from $A$ and $B$) if they are compatible. \begin{verbatim} "pccomb frA frB initst (stA, stB) = (let compat = ALL str:frA Int frB. stA str = stB str; combst = %str. if str : frA then stA str else if str : frB then stB str else initst str in if compat then {Term combst} else {})" "pcompfr frA A frB B state == let tsA = {st. Term st : A state}; tsB = {st. Term st : B state}; nont = {NonTerm} Int (A state Un B state) in nont Un UNION (tsA <*> tsB) (pccomb frA frB state)" \end{verbatim} Here \verb|(tsA <*> tsB)| means the set product of \verb|tsA| and \verb|tsB|. We have a result \verb|pcomp_chk| which is a sanity check that, where the frames of $A$ and $B$ are the set of all variable names, this definition is equivalent to the one mentioned in the previous paragraph (a useful check, since our first attempt at the definition above was erroneous). Noting that Dunne's formula $\prd (A || B) = \prd (A) \land \prd (B)$ implicitly refers to the frames of the commands, we prove it as \verb|pcompfr_prd|, as follows: \begin{verbatim} pcompfr_prd = "prds (fA Un fB) primed (pcompfr fA A fB B) = (prds fA primed A && prds fB primed B)" \end{verbatim} } \section{Conclusion} \label{s-concl} We have formalised a computational model suggested by the notion of total correctness underlying the B method, and have proposed definitions for the generalised substitution operators in terms of this model. We have shown that this model and these definitions do in fact imply the characterisations of these operators in terms of weakest preconditions. We have proved these results in Isabelle \cite{dawson-fgc-files}, and have also proved the other results of Dunne in \cite{dunne-gen-subs} (although not dealing explicitly with frames). Thus we have used formal verification to confirm a body of theory underlying a widely used program development methodology. We have shown how the computational model is derived from a compound monad, and have compared this model and monad with those arising from Dunne's theory of abstract commands in \cite{dunne-abstr-cmds}. We have shown how the monad arises from a distributive law, % and that this distributive law is in fact a monad morphism. which is in fact a monad morphism. \paragraph{Acknowledgements} Finally, I would like to thank Steve Dunne and some anonymous referees for some very helpful comments. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Here begins the end matter %\vspace*{-1em} \bibliographystyle{plain} \begin{thebibliography}{1} \bibitem{abrial-b-book} J-R~Abrial. The B-Book: Assigning Programs to Meanings. CUP, Cambridge, 1996. % Cambridge University Press, 1996. \bibitem{bwttt} Michael Barr and Charles Wells. Toposes, Triples and Theories. Springer-Verlag, 1983, or see \url{http://www.cwru.edu/artsci/math/wells/pub/ttt.html} \bibitem{chartier-b-hol} Pierre Chartier. Formalisation of B in Isabelle/HOL. In Recent Advances in the Development and Use of the B Method, % (B'98), Second International B Conference (B'98), % LNCS 1393, Springer 1998, 66--83. Lecture Notes in Computer Science 1393, Springer 1998, 66--83. \bibitem{dawson-cmkc} Jeremy~E~Dawson. {Compound Monads and the Kleisli Category}. Unpublished note. \url{http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/} \bibitem{dawson-fgc-files} Jeremy~E~Dawson. Isabelle files, at \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/fgc/} \bibitem{dawson-fgc} Jeremy~E~Dawson. {Formalising General Correctness}. In Computing: The Australasian Theory Symposium (2004), % Electronic Notes in Theoretical Computer Science \textbf{91} (2004), % 21--42. ENTCS \textbf{91} (2001), 21--42. {\url{http://www.elsevier.com/locate/entcs}} \bibitem{dunne-abstr-cmds} Steve Dunne. {Abstract Commands: A Uniform Notation for Specifications and Implementations}. In Computing: The Australasian Theory Symposium (2001), % Electronic Notes in Theoretical Computer Science \textbf{42} (2001), % 104--123. ENTCS \textbf{42} (2001), 104--123. {\url{http://www.elsevier.com/locate/entcs}} \bibitem{dunne-gen-subs} Steve Dunne. A Theory of Generalised Substitutions. In Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, 2002 (ZB 2002), Lecture Notes in Computer Science 2272, Springer 2002, 270--290. \bibitem{jd-cm} Mark P~ Jones \& Luc Duponcheel. Composing Monads. Research Report YALEU/DCS/RR-1004, Yale University, December 1993 \bibitem{Wadler-essence} Wadler, Philip, The Essence of Functional Programming. In Symposium on Principles of Programming Languages (POPL'92), 1992, 1--14. \end{thebibliography} \comment{ \newpage \appendix NOTE - APPENDIX NOT FOR PUBLICATION IN THE PROCEEDINGS \section{Results of Dunne \cite{dunne-gen-subs} and our Isabelle proofs} Here we set out the definitions and results of Dunne in \cite{dunne-gen-subs} and our related results proved using the Isabelle/HOL prover, based on our computational model and definitions. We show the name of the Isabelle theorem in the Isabelle files \cite{dawson-fgc-files} and, for results discussed in this paper, a reference to the relevant section. \begin{center} \begin{tabular}{l@{\quad} l@{\quad} l@{\quad} l@{\quad}} in \cite{dunne-gen-subs} & Dunnes's result & our Isabelle theorem & see \\ \S 3.1 & Table 1 & note \ref{n-tab1} & \\ \S 3.3 & Table 2 & \verb|magic_alt|, \verb|abort_alt| & \S \ref{s-mng} \\ \S 5 & \emph{trm} & \verb|trm_alt|, \verb|pc_trm_tc| & \S \ref{s-mng} \\ \S 5 & \emph{fis} & \verb|fis_alt|, \verb|fis_guard_tc| & \S \ref{s-mng} \\ \S 6 & \emph{trm} & \verb|trm_pcomp_tc| & \S \ref{s-pc} \\ \S 6 & \emph{prd} & \verb|prd_pcomp_tc2| & \S \ref{s-pc} \\ \S 6.1 & & \verb|pcomp_choice_tc| & \S \ref{s-pc} \\ \S 7 & \emph{lub} & \verb|lub_tc| & \S \ref{s-lub} \\ \S 8.2 & $S^\wedge$ & \verb|rephat_isfp|, \verb|rephat_is_lfp| & \S \ref{s-ritc} \\ \S 10.1 & GS1 & note \ref{nGS1} & \\ \S 10.1 & GS2 & \verb|wp_gen_conj| & \\ \S 10.1 & GS3 & \verb|GS3| & \S \ref{s-fvn} \\ \S 10.2 & Prop 1, (1.1) & \verb|wpm_mono_cond| & \\ \S 10.2 & Prop 1, (1.1) & \verb|wpm_mono_cond_alt| \ref{n-mono} & \\ \S 10.2 & Prop 1, (1.2) & \verb|wpm_weak_disj| & \\ \S 10.2 & Prop 2, (2.1) & \verb|trm_or_prd_tc| & \S \ref{s-ps} \\ \S 10.2 & Prop 2, (2.1) & \verb|trm_or_prdf_tc| \ref{n-prdf} & \\ \S 10.2 & Prop 2, (2.2) & \verb|prd_tc_imp_fis| & \S \ref{s-ps} \\ \S 10.2 & Prop 2, (2.2) & \verb|prdf_tc_imp_fis| \ref{n-prdf} & \\ \S 10.2 & Prop 2, (2.3) & \verb|fis_or_wp_tc| & \S \ref{s-ps} \\ \S 10.2 & Prop 2, (2.4) & \verb|wp_imp_trm_tc| & \S \ref{s-ps} \\ \S 10.2 & Prop 3 & \verb|prop3| & \S \ref{s-fvn} \\ \S 11 & Prop 4 & \verb|ACNF_tc| & \S \ref{s-lub} \\ \S 13 & Prop 7, p 287 & \verb|ref_tc_prdt| & \S \ref{s-prd} \\ \S 13 & Prop 7, p 288 & \verb|choice_ref_tc| & \S \ref{s-choice} \\ & & & \end{tabular} \end{center} Notes: \begin{enumerate} \item \label{n-tab1} \verb|ass_wp_tc|, \verb|precon_wp_tc|, \verb|guard_wp_tc|, \verb|choice_wp_tc|, \verb|seq_wp_tc| \item \label{nGS1} implicit from our definition of a generalised substitution \item \label{n-mono} proved from conjunctivity, as in \cite{dunne-gen-subs} \item \label{n-prdf} result uses \verb|prdf_tc|, a variant of \verb|prd_tc| specifying a particular frame \end{enumerate} } \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: