text:
\section{}
\label{}

\section{}
\label{}

\section{Introduction}
\label{sec:intro}
\input{sec/intro.tex}

\section{Preliminaries}
\label{sec:prelim}
\input{sec/prelim.tex}

\section{Reactive Relations and Conditions}
\label{sec:rrel}
\input{sec/rrel.tex}

\section{Reactive Design Contracts}
\label{sec:contracts}
\input{sec/contracts.tex}

\section{Automated Verification using Contracts}
\label{sec:mondex}
\input{sec/mondex.tex}

\section{Theory of Generalised Reactive Designs}
\label{sec:grd}
\input{sec/grd.tex}

\section{Mechanised Proof with Isabelle/UTP}
\label{sec:mech}
\input{sec/mech.tex}

\section{Related Work}
\label{sec:related}
\input{sec/related.tex}

\section{Conclusions}
\label{sec:conclusion}
\input{sec/conclusions.tex}

\section*{Acknowledgements}

This research is funded by the CyPhyAssure project\footnote{CyPhyAssure Project:
  \url{https://www.cs.york.ac.uk/circus/CyPhyAssure/}}, EPSRC grant EP/S001190/1, the RoboCalc project\footnote{RoboCalc
  Project: \url{https://www.cs.york.ac.uk/circus/RoboCalc/}}, EPSRC grant EP/M025756/1, and the EU Horizon 2020 project
``INTO-CPS'', grant agreement 644047~\footnote{INTO-CPS Project Website: \url{http://projects.au.dk/into-cps/}.}. We
would like to thank our colleagues on this project, particularly those from Peter Gorm Larsen's group at {\AA}rhus
University, for their collaboration over the past three years, without which this work could not have come to
fruition. We also thank the anonymous reviewers of this article, whose suggestions have greatly improved the
presentation of our work.

\bibliographystyle{spmpsci}      %

\subsection{Repository Overview}

\subsection{Isabelle/UTP}

All definitions and theorems have been mechanised in our UTP theorem prover, Isabelle/UTP~\cite{Foster16a,Zeyda16},
which is a semantic embedding of the UTP predicate and relational calculus in Isabelle/HOL~\cite{Isabelle}. We will here
give a brief overview of the mechanisation, and highlight some key technical details which have be thus far
elided.

Broadly speaking the syntax mirrors that of the mathematical account presented in this paper, with a few notable
exceptions. In particular, the handling of alphabets utilises the Isabelle type system to ensure well-formedness of
expressions, but requires insertion of explicit alphabet coercions. Moreover, for our UTP expression model we sometimes
want to reuse operator names already defined in HOL such as $+$, $\le$, and $=$. Sometimes this can be achieved through
polymorphic overloading, as is the case for $+$ and also numerical representations, which are both handled through the
type class mechanism. This does not work for $\le$ as the type does not fit the polymorphic pattern, and so we have to
add a subscript: $x \le_u y$. This is also true of several other operators, including $=$ which becomes $=_u$ so as not
to clash with HOL's operator which we often use for expressing algebraic laws.

Alphabetised predicates are modelled by a parametric type
$\alpha\ \upred \defs (\alpha \Rightarrow \mathbb{B})$, where $\alpha$ is the alphabet type. A predicate is thus a
function that states whether a particular state binding of the alphabet satisfies it. For example,
$\true \defs \lambda x @ \mathit{True}$, where $\mathit{True}$ is HOL's true, since any binding satisfies it. All the
propositional logic operators of the UTP's predicate calculus are obtained by similar lifting of HOL equivalents, for
example $P \land Q \defs \lambda x @ P(x) \land_{\tiny H} Q(x)$, where the right-hand side has the HOL operator. Our
predicate model is thus inherently \textbf{alphabet polymorphic}: predicates are open to extension and proven laws can
be instantiated to a variety of alphabets. This is important for our unifying theory of contracts where additional
variables such as $ref'$ may or may not be present, but generic laws still apply. Alphabetised relations are simply
predicates whose alphabet is a product space:
$$(\alpha, \beta)\ \urel \defs (\alpha \times \beta)\ \upred$$

Variables are modelled using lenses~\cite{Foster09,Foster16a}; these are projections that identify a particular region
of the alphabet. A lens $x : \tau \lto \alpha$ shows how to project the variable data of type $\tau$ out of the alphabet
$\alpha$. The behaviour of a lens is constrained by a number of algebraic laws~\cite{Foster16a}. Lenses can be tested
for observational equivalence using $x \lequiv y$, for $x : \tau_1 \lto \alpha$ and $y : \tau_2 \lto \alpha$ (i.e. with
potentially different view types, but the same source), containment using the sublens relation $x \lsubseteq y$, and
observational difference using $x \lindep y$, which we call lens independence.

Relational variables, with a product alphabet, can be constructed using lens compositions. The initial value of $x$ is
obtained by $\lfst \lcomp x$, and the final value by $\lsnd \lcomp x$. Lenses $\lfst$ and $\lsnd$ select the first and
second part of a product, respectively, and the composition operator $\lcomp$ is analogous to function composition. In
Isabelle/UTP initial and final variables are written as \verb|$x| and \verb|$x`|, respectively. Also useful for dealing
with relational lenses is the product lens $a \lprod b$ that point-wise composes $a : \alpha \lto \gamma$ and
$b : \beta \lto \delta$, to produce a lens of type $\alpha \times \beta \lto \gamma \times \delta$.

One can also check whether a given predicate $P$ depends on a particular lens $x$ using the unrestriction predicate
$\unrest{x}{P}$, which means that $P$'s truth-valuation is unchanged if $x$ is changed. Unrestriction thus effectively
gives us a semantic characterisation of whether a variable is present in a predicate or not. It distributes through
the predicate operators as expected, for example $$\unrest{x}{P} \land \unrest{x}{Q} \implies \unrest{x}{(P \land Q)}$$

Since types are used to model alphabets, modification by adding or removing variables means that we must perform a type
coercion. We implement two operators in Isabelle/UTP: alphabet extrusion ($P \aext a$) and alphabet restriction
($Q \ares a$), for $a : \beta \lto \alpha$, $P : \beta\ \upred$, and $Q : \alpha\ \upred$. Lens $a$ shows how one
alphabet $\beta$ can be embedded into another alphabet $\alpha$. Thus alphabet extrusion modifies $P$, whose alphabet is
$\beta$ to have the ``larger'' alphabet $\alpha$, and restriction is the converse of this. Alphabet extrusion is a
lossless operation, whereas restriction can potentially lose information about removed portions of the
alphabet. Following an extrusion, $P \aext a$, it is guaranteed that an lens independent of $a$ is unrestricted. This is
because $P$ exclusively talks about alphabet $\beta$, and not other parts of the larger $\beta$:
$$x \lindep a \implies \unrest{x}{(P \aext a)}$$

For reactive designs, we use alphabet extrusions to impose constraints such as ``$ok$ and $wait$ are not
mentioned''. This is done through our own \textbf{alphabet} command in Isabelle -- an extension of the record package
that also creates a lens for each field. Moreover, like the record package, we utilise parametric polymorphism and the
associated subtyping mechanism such that alphabets can be extended by the addition of field lenses. The alphabet of
designs is described by the type $\alpha\,\textit{des}$, which consists of the single lens
$ok : \mathbb{B} \lto \alpha\ \textit{des}$. Parameter $\alpha$ can be used to extend the alphabet with further
variables.

In this way, we create the extended alphabet type $(\sigma, \mathcal{T}, \alpha) \textit{rsp}$ for stateful reactive
processes, where $\sigma$ is the variable state-space, $\mathcal{T}$ is a trace algebra type, and $\alpha$ permits
further extension. In addition to $ok$ it also has lenses
\begin{itemize}
  \item $wait : \mathbb{B} \lto (\sigma, \mathcal{T}, \alpha)\ \textit{rsp}$;
  \item $tr : \mathcal{T} \lto (\sigma, \mathcal{T}, \alpha)\ \textit{rsp}$; and
  \item $st : \sigma \lto (\sigma, \mathcal{T}, \alpha)\ \textit{rsp}$.
\end{itemize}

State variables will all be sublenses of $st$, meaning they exclusively observe that portion of the state-space. Thus,
if we have a homogeneous relation $R$ on state variables only of type $(\sigma, \sigma)\ \urel$, then we can lift this
into a relation on the alphabet $(\sigma, \mathcal{T}, \alpha) \textit{rsp}$ via alphabet extrusion
$P \aext (st \lprod st)$, which we give the notation $\lceil R \rceil_S$. This predicate has $ok$, $wait$, $tr$ etc. all
unrestricted, and thus we are using the type system to encode alphabet provisos. Similarly, we provide such lifting
operators for preconditions on the state-space, $\lceil P \rceil_{S<}$, where $P : \sigma\ \upred$.

\begin{figure}
  \includegraphics[width=11.8cm]{figures/Pay_contract}

  \caption{Calculating the contract of $Pay$ in Isabelle/UTP}
  \label{fig:PayContract}
\end{figure}

Thus, in many of the mechanised versions of the reactive design laws such coercions must be manually inserted. For
example, in Theorem~\ref{thm:mondexcontract}, where we calculate the contract of the $Pay$ action, the last disjunct of
postcondition $P_3$, the assignment where the accounts are debited and credited, actually has
$$\lceil accts := accts(i \mapsto accts(i) - n, j \mapsto accts(j) + n) \rceil_S$$ in the mechanisation. This is
illustrated in the screenshot in Figure \ref{fig:PayContract}. Here, $accts$ is actually a lens of type
$\textit{int}\,\textit{list} \lto \textit{st-mdx}$ in Isabelle, where \textit{st-mdx} is the state-space type, and thus
must be lifted.

\subsection{Parallel-by-Merge}

Mechanisation of parallel-by-merge posed some specific technical challenges, and thus we will summarise how it
works. Since alphabets are types in Isabelle/UTP, the type of each variable is sensitive to alphabet extension which
introduces some notational issues. When constructing a parallel composition ($P \parallel_M Q$) it is necessary to
extend the alphabet to include three copies of the variables: indexed varieties for $P$ and $Q$, and the initial value
of variables. If $P$ and $Q$ are both homogeneous relations of type $(\alpha, \alpha)\,\urel$ then the merge predicate
$M$ essentially has type $(\alpha \times \alpha \times \alpha, \alpha)\,\urel$, since it merges three copies of the
state. For reasons of convention, the initial state is the first $\alpha$, and the indexed states are the second and
third, respectively.

Unfortunately, that means that unlike in mathematical UTP we cannot refer to the initial values of variables using the
standard undecorated variable notation (\verb|$x|), as such as construction has type $\alpha \lto (\alpha \times
\alpha)$, when we actually want to project from a source type $\alpha \times \alpha \times
\alpha$. Thus we have to introduce three notations, \verb|$x|$_<$, \verb|$0-x|, and \verb|$1-x|, for the three
components. We also implement the renaming notations $\psep{P}{0}$ and $\psep{Q}{1}$ that both perform alphabet
extrusion, converting both to have type $(\alpha, \alpha \times \alpha \times \alpha) \urel$ to match the output with
the input of the merge predicate. The final representation of $P \parallel_M Q$ is
$(\psep{P}{0} \land \psep{Q}{1} \land v' = v_<) \relsemi M$ which has type $(\alpha, \alpha)\,\urel$ as expected.

This technicality also has an impact on the formalisation of the healthiness conditions for merge predicates. In
mathematical UTP, we can simply reuse $\healthy{R1}$, $\healthy{R3}_h$, and other healthiness conditions. Here, we have
to create variants that refer to the explicit initial variables instead, which we give names like $\healthy{R1m}$ whose
definition is $tr_{<} \le tr'$. Using these, we then prove all the laws for parallel composition and reactive
designs. These healthiness conditions, it should be stressed, are semantically equivalent modulo variable renamings. Of
course, this isn't the case for $\healthy{R2}_c$ which as we have previously showed~\cite{Foster17a} requires
modification anyway.

\subsection{Reactive Design Tactics}

One particular aim of this work has been to support a high level of automated reasoning for reactive contracts. This has
involved the creation of new tactics and utilisation of a number of existing tactics. The initial particular problem to
be solved is bridging the gap between UTP predicates and HOL predicates which are distinct types, albeit strongly
related. In particular, the majority of operators of the former are defined, via the \textbf{lifting}
package~\cite{Huffman13}, in terms of operators of the latter. The major difference is the addition of lenses which
accounts for the alphabet or state-space not implicitly present in HOL predicates.

Our approach to reasoning about alphabetised predicates and relations therefore extends the approach we first described
in~\cite{Foster14}. The basic approach is two step: firstly apply the transfer tactic to interpret a UTP predicate to a
HOL predicate, and secondly apply Isabelle/HOL's built in automated reasoning tactics, such as \textit{auto},
\textit{sledgehammer}, and \textit{nitpick}. We've now also extended this approach to provide explicit support for
lenses. Each record lens can be collapsed and rewritten to a HOL variable with a similar name. Effectively this means
that reasoning about UTP predicates and relations can often be reduced to reasoning about HOL predicates, which of
course improves automation. In particular, for relations, proof reduces to a satisfiability problem since sequential
composition boils down to existential quantification. We provide tactic \textbf{pred-auto} which uses this approach,
combined with HOL's \textbf{auto} to deal with predicate conjectures, and \textbf{rel-auto} to deal with relational
conjectures.

Reasoning about predicates and relations in this is indeed powerful, but it becomes unwieldy when dealing with very
complex definitions, particularly our reactive contracts. Each reactive contract is written in terms of the $\Rs$
healthiness condition, and the design turnstile, which adds a large overhead particularly when dealing with large
composite definitions. Thus we develop an additional tactic, based on the algebraic laws of Sections~\ref{sec:contracts}
and \ref{sec:grd}. The tactic can be used to prove (or refute) refinement conjectures of the form $P \sqsubseteq Q$ for
two reactive design contracts. Moreover, through application of antisymmetry, we can also use it to prove equality
conjectures.

The process has three stages:

\begin{enumerate}
\item \textbf{Calculate and simplify reactive design contracts}. The algebraic laws of reactive designs are applied to
  convert a composite reactive contract into a monolithic one of the syntactic form $\rc{P}{Q}{R}$. This of course
  necessitates that appropriate calculation theorems have been proved and are already available;
\item \textbf{Apply the refinement theorem}. Theorem~\ref{thm:rdesrefine} is applied to break the refinement conjecture
  into three proof obligations about the pre-,peri-, and postconditions.
\item \textbf{Apply relational transfer and reasoning tactic}. The three proof obligations are purely relational, do not
  refer to observational variables $ok$ and $wait$, and thus are much more lightweight in nature. Thus we can now apply
  \textbf{rel-auto}, and potentially other HOL tactics, to try and complete the proof. Of course, we can also at this
  point try to generate a counterexample, which can be traced back to a fault in the pre-,peri-, or postcondition.
\end{enumerate}

We have found this approach extremely useful for automated reasoning, and it has been used to valid all the example
calculations, in particular those related to the MiniMondex example\footnote{See
  \url{https://github.com/isabelle-utp/utp-main/blob/master/tutorial/utp_csp_mini_mondex.thy} for our complete
  mechanised theory}.

\subsection{Contracts and Refinement}
\label{sec:contref}

Reactive program components normally proceed through three phases during execution:

\begin{enumerate}
  \item \textbf{pre-execution} -- the program waits for its predecessor to terminate and does not contribute any
    observable behaviour.
  \item \textbf{intermediate execution} -- the program begins the main body of its execution, which includes
    communication with other concurrent processes, and updates to its state. During this time state updates are, however,
    hidden from its successor.
  \item \textbf{termination} -- the program ceases interaction with the environment, reveals its final state to the
    successor, and signals permission for it to begin. Since reactive programs often do not terminate, this phase may
    never be reached.
\end{enumerate}

\noindent In this view, we largely assume that parallel programs do not directly share state but, as is typical in
process algebras, they must explicitly communicate using a suitable mechanism such as channels. All other activity, such
as state updates, is internalised to the sequential behaviour of the process, though it is possible to merge the state
of several terminated parallel processes~\cite{Oliveira&09}. Shared variables can, nevertheless, be modelled by encoding
them within traces.

Reactive programs can also diverge~\cite{Roscoe2005}, meaning they exhibit erroneous behaviour, such as engaging in an
infinite sequence of internal activity without any communication. Divergence corresponds to violation of a contract's
assumptions. A reactive design contract is a triple~\cite{Canham15} of the form
$$\rc{P(\state, \trace, r)}{Q(\state, \trace, r, r')}{R(\state, \state', \trace, r, r')}$$ the three parts of which are:

\begin{enumerate}
\item the \textbf{precondition} $P$, with assumptions the contract makes before it executes, violation of which
  corresponds to a programmer error such as divergence. It is a reactive condition, and can therefore refer to the
  initial state $\state$, the trace contribution $\trace$, and potentially other (unprimed) observational variables in the
  alphabet ($r$), but not observational variables $ok$ or $wait$, or primed variables other then $tr'$. Access
  to $tr'$ is usually indirect through $\trace$.
\item the \textbf{pericondition} $Q$, with commitments the contract guarantees to fulfil during its intermediate
  execution steps. Often, it used to represent ``quiescent'' observations, where the program is awaiting interaction with
  it environment. It is a reactive relation only on the initial states, $\trace$, and any other variables ($r, r'$).
  \item the \textbf{postcondition} $R$, with commitments that are fulfilled should the program terminate. It is a
    reactive relation that can additionally refer to the final state $\state'$, unlike the pre and pericondition.
\end{enumerate}

\noindent Such contracts can be used both as specifications, for encoding assumptions and guarantees for a subsystem, or
alternatively as a means to encode the semantics of a reactive programming language.  A reactive design contract has the
following definition.
\begin{definition}[Reactive Design Contract] \label{def:rcontract} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L492}
 $$\rc{P_1}{P_2}{P_3} ~~\defs~~ \rtdes{P_1}{P_2}{P_3} \quad \text{where $P_1 \is \healthy{RC}$, and $P_2$ and $P_3$ are both $\healthy{RR}$}$$
\end{definition}
\noindent This definition assumes that $P_1$, $P_2$, and $P_3$ are as specified above. This is formalised by requiring
that $P_1$ is a reactive condition, and $P_2$ and $P_3$ are both reactive relations, using the theory developed in
Section~\ref{sec:rrel}. The reactive contract is a form of UTP design which is made reactive using $\Rs$. In previous
work~\cite{Oliveira&09}, reactive designs are often written in just two parts ($\Rs(P \shows Q)$), the assumption and
guarantee, with the intermediate and final behaviours intertwined. Here, we adopt the triple notation first developed in
\cite{Canham15} as it allows us to consider these separately and simplifies many laws. The diamond
$P_2 \wcond P_3$~\cite{Canham15} is simply an abbreviation for $\conditional{P_2}{wait'}{P_3}$, which distinguishes
intermediate and final non-divergent observations.

Our theory supports contract refinement, which is characterised by the following theorem:
\begin{theorem}[Reactive Design Refinement] \label{thm:rdesrefine} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L846}
  $$\rc{P_1}{P_2}{P_3} \refinedby \rc{Q_1}{Q_2}{Q_3} \iff [P_1 \implies Q_1] \land (P_2 \refinedby (Q_2 \land P_1)) \land (P_3 \refinedby (Q_3
  \land P_1))$$
\end{theorem}
\noindent This is not a definition, but a theorem of the UTP refinement operator from Definition~\ref{def:refinement}
that is supported by the UTP theory (elaborated in Section~\ref{sec:grd}). Theorem~\ref{thm:rdesrefine} shows that
contract refinement reduces to three proof obligations:
\begin{enumerate}
  \item the precondition is weakened ($P_1 \implies Q_1$);
  \item the pericondition of the first contract ($P_2$) is strengthened by the pericondition of the second ($Q_2$),
    conjoined with the precondition of the first ($P_1$);
  \item the postcondition of the first contract ($P_3$) is strengthened by the postcondition of the second ($Q_3$),
    conjoined with the precondition of the first ($P_1$).
\end{enumerate}
Such a weakening of the assumption and strengthening of the guarantees, of course, is a defining feature of most
contract theories~\cite{Meyer92,Back1998,Benveniste2007,Benvenuti2008}. The particular value of this theorem in our
case is to provide a foundation for a standard verification procedure for contract-based reactive languages. If a
language can be given a contractual denotational semantics, meaning that every operator can be assigned a reactive
contract, then we can solve a verification problem, $\rc{\!P_1\!}{\!P_2\!}{\!P_3\!} \refinedby Q$, for a specification
$P$ and reactive program $Q$.

We first calculate the program's contact $Q = \rc{\!Q_1\!}{\!Q_2\!}{\!Q_3\!}$, and then use Theorem~\ref{thm:rdesrefine}
to produce the three proof obligation predicates. Then, we can utilise theorem proving technology for relational
calculus in Isabelle/UTP~\cite{Foster14,Foster16a} to attempt discharge of the proof obligations. In Isabelle/HOL, this
can be supported by the \textsf{sledgehammer} proof method~\cite{Blanchette2011} that harnesses external automated
theorem provers. Consequently, our theorem of contracts can be used to support an automated verification technique for
reactive programs. This allows us, in particular, to support verification of programs and models with a very large or
infinite state space, since the calculated contracts are symbolic rather than explicit entities, which allows us to
overcome the state explosion problem. This, then, is the utility of the complex theory that follows.

In addition to the refinement law, we also have a similar theorem for proving equivalences:
\begin{theorem}[Reactive Design Equivalence] \label{thm:rdesequiv} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L909}
  $$\rc{P_1}{P_2}{P_3} = \rc{Q_1}{Q_2}{Q_3} \iff (P_1 = Q_1) \land ((P_2 \land Q_1) = (Q_2 \land P_1)) \land ((P_3 \land Q_1) = (Q_3 \land P_1))$$
\end{theorem}

\noindent This theorem is a consequence of Theorem~\ref{thm:rdesequiv} and the fact that refinement is
antisymmetric. Two reactive contracts are equivalent if, and only if, (1) their preconditions are equivalent, and (2)
their peri- and postconditions are equivalent modulo the precondition. With this theorem we can similarly automate
proving equivalences.

\subsection{Denoting Reactive Programs}

A crucial requirement of the verification strategy outlined above is that the target language is equipped with a
denotational semantics in terms of reactive contracts. We illustrate the use of contracts in giving a denotational
semantics to a reactive language by denoting several of the operators from the \Circus
language~\cite{Woodcock2001-Circus,Oliveira&09}. For this, we first need to specialise the semantic model to
failure-divergences~\cite{Roscoe2005}. We thus specialise the trace algebra to finite sequences,
$tr : \seq\,\textit{Event}$, for some suitable set of events, and add the observational variable
$\refu' : \power\,\textit{Event}$, as usual~\cite{Cavalcanti&06}. This allows us to record the set of events which are
refused when an action is in a quiescent state, or equivalently the set of events that the action is willing to engage
in. It is equivalent to encoding CSP failure traces~\cite{Roscoe2005}, which consist of a sequence of events and a
refusal set. Adding observational variables is possible because the alphabet of the reactive design theory is
extensible; consequently our verification strategy is effectively parametric in a specialised semantic model.

We begin with the example of \Circus event prefix~\cite{Oliveira&09}, which is denoted by a reactive design triple:
\begin{example}[Event Prefix Reactive Design] \label{ex:prefix} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/sf_rdes/utp_sfrd_prog.thy\#L591}
  $$a \then \Skip ~~\defs~~ \rc{\truer}{a \notin \refu' \land \trace = \langle\rangle}{\state' = \state \land \trace = \langle a \rangle}$$

  \noindent This simple event prefix represents a program that, when enabled, waits for the environment to permit an $a$
  event, and following this, terminates. It is denoted by a contract with a true precondition since it can never
  diverge; every environment is a valid context. Its pericondition encodes a single quiescent observation: the event $a$
  is not refused and no events has been contributed to the trace as yet. The postcondition states that, when the program
  terminates, the state is unchanged by the event, and the trace is extended with $a$. In \Circus one can use this
  definition to represent the more general prefix construct using sequential composition:
  $a \then P ~~\defs~~ (a \then \Skip) \relsemi P$. \qed
\end{example}
Other examples are the $\Skip$ action, which represents a terminating process, and the $\Stop$ action, which represents a
deadlock.
\begin{example}[Terminated and Deadlocked Actions] \label{ex:termdead} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/sf_rdes/utp_sfrd_healths.thy\#L69}
  \begin{align*}
    \Skip ~~\defs~~& \rc{\truer}{\false}{\trace = \langle\rangle \land \state' = \state} \\
    \Stop ~~\defs~~& \rc{\truer}{\trace = \langle\rangle \land \refu' \subseteq \textit{Event}}{\false}
  \end{align*}

  \noindent The terminated action $\Skip$ has a true precondition. It has no intermediate observations, so the
  pericondition is $\false$, as it is essentially instantaneous and never pauses for interaction. In the postcondition,
  it is specified that the action makes no contribution to the trace, and leaves the state variables unchanged. The
  deadlocked action ($\Stop$) likewise has a true precondition. No state is a final state, indicated by the $\false$
  postcondition, since the process does not terminate. In the quiescent states it is simply required that the trace is
  unchanged, and any refusal set is observable, since no event is enabled.
  \qed
\end{example}

Our final example is external choice over a contract indexed by set $A$.

\begin{example}[External Choice] \label{ex:extchoice} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/sf_rdes/utp_sfrd_extchoice.thy\#L124}
  \begin{align*}
    &\Extchoice i \in A @ \rc{P_1(i)}{P_2(i)}{P_3(i)} = \\[.5ex]
    &\qquad \rc{\bigwedge_{i \in A} P_1(i)}{\conditional{\left(\bigwedge_{i \in A} P_2(i)\right)}{\trace = \langle\rangle}{\left(\bigvee_{i \in A} P_2(i)\right)}}{\bigvee_{i \in A} P_3(i)}
  \end{align*}

  \noindent This is the first example of a contract composition law: it shows how a collection of contracts, in this
  case an indexed set, can be composed in a single contract. Such composition laws can then be combine with definitions,
  like those in Examples~\ref{ex:prefix} and \ref{ex:termdead} for contract calculation. The overall contract permits
  internal activity in the choice branches, but the choice itself is not resolved until an external event occurs. The
  precondition requires that the preconditions of all branches of the external choice hold in the initial state. In the
  pericondition, while the trace has not changed and thus no event has occurred ($\trace = \langle\rangle$), all
  periconditions of the choice hold simultaneously. Once an event has occurred only one of the periconditions need
  hold. This is the reason why the pericondition does not refer to final states, as these are concealed until
  termination or observation. Finally, in the postcondition, one of the choice branch postcondition holds. \qed
\end{example}
Though the three example definitions look different from the standard presentation of \Circus~\cite{Oliveira&09}, they
are largely equivalent. Indeed, the definitions given above are largely theorems of the original \Circus definitions,
and therefore our encoding is conservative. The exception is event prefix, in which we conceal the state whilst waiting
for the event, following previous work~\cite{BGW09}.

We now have a contractual denotational semantics for simple \Circus actions. For verification, we also need to specify
properties for reactive programs using specification contracts. A common desirable property of \Circus actions and CSP
processes is deadlock-freedom~\cite{Roscoe2005}, which states that a process never reaches a quiescent state where no
event is enabled. It can be specified using the following reactive contract:

\begin{definition}[Deadlock-freedom Contract] $\ckey{CDF} \defs \textstyle\rc{\truer}{\exists e @ e \notin \refu'}{\truer}$ \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/sf_rdes/utp_sfrd_fdsem.thy\#L425}
\end{definition}

This reactive contract has a $\truer$ precondition, which by Theorem~\ref{thm:rdesrefine}, means that the precondition
of the implementation contract must also be $\truer$. This is because we must weaken the precondition, and $\truer$ is
the weakest possible reactive condition. Intuitively, this means that to refine $\ckey{CDF}$, a reactive program must
also be free of divergence. The postcondition is also $\truer$, but since we must strengthen the postcondition, any
postcondition for the implementation is admitted. The pericondition contains the main specification formula; it states
that in every quiescent observation there must be an event which is not being refused. In other words, only programs
that do not admit the observation $\refu' = \textit{Event}$ are deadlock-free.

We can show, for example, that $a \then \Skip$ is deadlock-free:

\begin{example}[$\ckey{CDF} \refinedby a \then \Skip$]
  Since the precondition of $a \then Skip$ is $\truer$, it suffices to consider the pericondition, and show that the
  following refinement holds: $$(\exists e @ e \notin \refu') \refinedby a \notin \refu' \land \trace = \langle\rangle$$
  Recall that refinement is reverse implication. Therefore, we need to show that
  $a \notin \refu' \implies (\exists e @ e \notin \refu')$, which straightforwardly holds when we set $e =
  a$. Consequently, we have proved deadlock-freedom.

  Conversely, we cannot show that $\Stop$ is deadlock-free, because its pericondition includes
  $\refu' \subseteq \textit{Event}$, which allows the possibility of refusing everything. \qed
\end{example}

\subsection{Calculational Laws}

Though language-specific operators like those above for \Circus can be expressed, many core contract operators can be
introduced generically. We can therefore develop a large body of laws for calculating contracts that do not depend on a
particular semantic model, but can be instantiated with any trace algebra $\tset$, and additional observational
variables. We begin by denoting some basic reactive operators for this generic theory.
\begin{theorem}[Reactive Design Core Operators] \label{thm:rdescore} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L492}
\begin{align*}
  \IIsrd &~=~ \rc{\truer}{\false}{\IIr} \\[.3ex]
  \assignsR{\sigma} &~=~ \rc{\truer}{\false}{\assignsr{\sigma}} \\[.3ex]
  \Miracle &~=~ \rc{\truer}{\false}{\false} \\[.3ex]
  \Chaos &~=~ \rc{\false}{\false}{\false}
\end{align*}
\end{theorem}
\noindent Operator $\IIsrd$ is reactive design identity. It has a true precondition, and a false pericondition,
indicating that it has no intermediate states and so is essentially instantaneous. The postcondition defines that it
contributes nothing to the trace, and simply identifies the before and after states. Since the alphabet at this point is
open, by using $\IIr$ as a postcondition, we also add the conjunct $r' = r$ which is shorthand for saying all additional
variables are unchanged. This distinguishes $\IIsrd$ from the \Circus-specific $\Skip$ operator from
Example~\ref{ex:termdead}, which leaves $\refu'$ unconstrained.

Operator $\assignsR{\sigma}$ is a generalised assignment, again similar to Back's update action~\cite{Back1998}, where
$\sigma : \Sigma \to \Sigma$ is a function on the state space. Its postcondition defines an update of the state by
applying $\sigma$ to it using the reactive relational assignment. The more specific assignment $\assignR{x}{v}$ can be
expressed as $\assignsR{\{x \mapsto v\}}$. The generalised assignment also enables us to easily define multiple-variable
assignment constructs.

$\Miracle$ is the miraculous reactive design. It has a true precondition, but has no intermediate or final states, and
thus is effectively impossible to execute. It is the top element of the refinement lattice:
\begin{theorem} $\rc{P_1}{P_2}{P_3} \refinedby \Miracle$ \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_healths.thy\#L545}
\end{theorem}
\noindent This follows, by Theorem~\ref{thm:rdesrefine}, since the precondition $\truer$ is the least reactive
condition, and $\false$ is the greatest reactive relation. $\Chaos$, in contrast to $\Miracle$, is the contract with an
unsatisfiable precondition and thus always yields a program error. It is the bottom of the refinement lattice, and is
the least deterministic contract:
\begin{theorem} $\Chaos \refinedby \rc{P_1}{P_2}{P_3}$ \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_healths.thy\#L545}
\end{theorem}
$\Chaos$ can be used to identify interactions that are erroneous, and thus the context should avoid them, as illustrated by
the following example.
\begin{example}[Divergent Process] \label{ex:divproc}
  \begin{align*}
    &a \then \Chaos \extchoice b \then \Skip = \\[.5ex]
    &\qquad \rc{\negr (\langle a \rangle \le \trace)}{\trace = \langle\rangle \land a \notin ref' \land b \notin ref'}{\trace = \langle b \rangle \land st' = st}
  \end{align*}

  \noindent Here, we have utilised Examples~\ref{ex:prefix} and \ref{ex:extchoice}, together with
  Definition~\ref{thm:rdescore} to calculate the composite contract. This \Circus action allows either an $a$ or $b$
  event, but if the environment chooses $a$ then it diverges. The precondition therefore defines the assumption that the
  environment does not extend the trace by $a$, using a reactive condition of the form illustrated in
  Example~\ref{ex:constrprf}. If the program performs $a$, then the behaviour is unpredictable. The pericondition states
  that the trace has not yet been extended, and the action does not refuse $a$ or $b$. However, though it is not
  refused, $a$ can never lead to a terminating state as defined in the postcondition, which specifies that the trace is
  extended by $b$ and leaves the state unchanged. \qed
\end{example}
Contracts can also be constructed using the programming and specification operators of UTP's relational calculus. This
effectively means that relational laws of programming can be directly imported for use in proofs about contracts. We
have proved a number of theorems that show the results of composing contracts.  \allowdisplaybreaks
\begin{theorem}[Reactive Design Compositions] \label{thm:rdes-comp} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L983}
\begin{align}
  \rc{P_1}{P_2}{P_3} \intchoice \rc{Q_1}{Q_2}{Q_3} &~=~ \rc{P_1 \land Q_1}{P_2 \lor Q_2}{P_3 \lor Q_3} \\[2.5ex]
  \bigsqcap_{i\in I} \rc{P_1(i)}{P_2(i)}{P_3(i)} &~=~ \rc{\bigwedge_{i \in I} P_1(i)}{\bigvee_{i \in I} P_2(i)}{\bigvee_{i \in I} P_3(i)} \label{thm:rdes-comp-inf} \\[2.5ex]
  \rc{P_1}{P_2}{P_3} \sqcup \rc{Q_1}{Q_2}{Q_3} &~=~
     \rc{
         \begin{array}{c}
           P_1 \ \\
           \lor Q_1
         \end{array}
         }{
         \begin{array}{c}
           P_1 \rimplies P_2 \land \!\! \\
           Q_1 \rimplies Q_2
         \end{array}
         }{
         \begin{array}{c}
           P_1 \rimplies P_3 \land \\
           Q_1 \rimplies Q_3
         \end{array}} \\[2.5ex]
  \conditional{\rc{P_1}{P_2}{P_3}}{b}{\rc{Q_1}{Q_2}{Q_3}} &~=~
     \rc{\begin{array}{c}
          P_1 \\
          \infixIf b \infixElse \\
          Q_1
         \end{array}
     }{\begin{array}{c}
          P_2 \\
          \infixIf b \infixElse \\
          Q_2
       \end{array}
     }{\begin{array}{c}
          P_3 \\
          \infixIf b \infixElse \\
          Q_3
       \end{array}
     } \\[2.5ex]
  \rc{P_1}{P_2}{P_3} \relsemi \rc{Q_1}{Q_2}{Q_3} &~=~
     \rc{\begin{array}{c}
           P_1 \land \\
           P_3 \wpR Q_1
         \end{array}
        }{\begin{array}{c}
           P_2 \lor \\
           P_3 \relsemi Q_2
          \end{array}
        }{P_3 \relsemi Q_3} \label{thm:rdes-seq} \\[2.5ex]
  \rc{P}{Q}{R}^{n+1} &~=~ \rc{\bigwedge_{i \le n} \left(R^i \wpR P\right)}{\bigvee_{i \le n} R^i \relsemi Q}{R^{n+1}} \label{thm:rdes-comp-pow}
\end{align}
\end{theorem}
\noindent These are theorems, rather than definitions, since they formulate the semantics of contracts that are composed
by the UTP operators defined previously in Definition~\ref{def:utp-prog}. We do not need to redefine them for our theory
of reactive designs, but rather prove laws that show how to calculate composite contracts. This is a key contribution of
our work, since it means the existing theorems of operators like $\relsemi$ and $\sqcap$ can be directly imported into
our theory of reactive designs, and applied to algebraic reasoning.

The internal choice of two contracts, ($P \intchoice Q$), yields a contract that assumes both preconditions
hold, and yields the combined intermediate and final states by disjunction. The preconditions are conjoined since the
choice is non-deterministic, and thus there must be no possibility of divergence in any of the possible
branches. Internal choice can, alternatively, be viewed as a disjunction operator for contracts similar to that
in~\cite{Benveniste2007}. Similarly, an internal choice over a set of basic actions indexed by a set $I$ conjoins all
the preconditions, and disjoins the peri- and postconditions. Dual to disjunction, the conjunction of two contracts
($P \sqcup Q$) requires that one of the preconditions holds, and takes the conjunction of the corresponding intermediate
and final states. The conditional $\conditional{P}{b}{Q}$, where $b$ is a predicate on $st$ alone, can be distributed
through the pre-, peri-, and postconditions of the respective reactive designs.

Sequential composition $P \relsemi Q$, where $P = \rc{P_1}{P_2}{P_3}$ and $Q = \intchoice \rc{Q_1}{Q_2}{Q_3}$, is a
little more involved. The combined precondition conjoins the precondition of $P$ with a predicate requiring that the
postcondition of $P$ does not violate the precondition of $Q$. The latter is specified using the reactive weakest
precondition operator, $P \wpR Q$. The pericondition states that either $P$ is in an intermediate state, and thus $P_2$
holds, or else $Q$ is in intermediate state, $P$ having terminated, and thus $P_3 \relsemi Q_2$ holds. Finally, the
postcondition states that both $P$ and $Q$ have terminated, that is, $P_3 \relsemi Q_3$.

As a corollary, we prove the law for finite iteration of a reactive design, $P^{n+1}$, assuming at least one execution,
that is, for $\rc{P}{Q}{R} \relsemi \rc{P}{Q}{R} \relsemi \cdots \relsemi \rc{P}{Q}{R}$. This law can be applied to
calculate the contract for a recursive reactive program. The precondition requires that after $i \le n$ iterations of
the postcondition $R$, the precondition $P$ is not violated. The pericondition states that postcondition $R$ has been
established a number of times $i \le n$, followed by the pericondition $Q$ holding. In other words, one of the
iterations is still in an intermediate state. Finally, the overall postcondition states that $R$ has been established
$n + 1$ times.

Finally we present a law for calculating the contract of a tail-recursive program of the form
$\thlfp{R}\, X @ P \relsemi X$, where $\thlfp{R}$ is the weakest fixed-point operator, which allows us to formulate
iterative contracts. This is subject to $P$ being a productive~\cite{Coquand1993} contract, that is, one that extends
the trace when it terminates.

\begin{definition} \label{def:productive} $\rc{P_1}{P_2}{P_3}$ is said to be productive if $P_3$ is a
  fixed-point of $\ckey{R4}(P) \defs P \land tr < tr'$, that is if we establish termination then it is necessary that
  the trace strictly increases. \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_productive.thy\#L12}
\end{definition}

For example, $a \then \Skip$ is productive because it always produces an $a$ event upon termination. Its postcondition
is $\healthy{R4}$ healthy because it contains the conjunct $\trace = \langle a \rangle$, which strictly increases the
trace ($tr < tr'$). On the other hand, $\assignsR{\sigma}$ is not productive because it contributes no events to the
trace. Productivity is related to, but not the same as the common notion of ``guardedness''~\cite{Hoare&98}, which, as
explained in Section~\ref{sec:recurse}, applies to a function on contracts rather than a contract itself. If a
contract's postcondition is productive, then we have the following theorem.

\begin{theorem}[Recursive Reactive Design] \label{thm:rdes-rec}

  \noindent If $R$ is $\healthy{R4}$ healthy, then
  \begin{align*}
  \thlfp{R}\, X @ \rc{P}{Q}{R} \relsemi X &= \rc{\bigwedge_{i \in \nat} \left(R^i \wpR P\right)}{\bigvee_{i \in \nat} R^i \relsemi Q}{\false}
\end{align*}
\end{theorem}

\noindent Such a recursive contract has a false postcondition, since it does not terminate. The precondition requires
that, no matter how many times postcondition $R$ is established, it does not violate the contract's precondition
$P$. The pericondition is where the main behaviour of the contract is specified. It states $R$ is executed some number
of times, and then the pericondition holds. In other words, the contract has executed its body and terminated into a
final state of the body several times, but then finally the contract always lands in an intermediate state, since it
does not terminate itself.

We now give some of the algebraic laws of reactive design contracts.
\begin{theorem}[Reactive Design Laws]
  \begin{align*}
    \Miracle \intchoice \rc{P_1}{P_2}{P_3} &~~=~~ \rc{P_1}{P_2}{P_3} \tag{RD1} \label{law:RD1} \\
    \Chaos \intchoice \rc{P_1}{P_2}{P_3} &~~=~~ \Chaos \tag{RD2} \label{law:RD2} \\
    \IIsrd \relsemi \rc{P_1}{P_2}{P_3} &~~=~~ \rc{P_1}{P_2}{P_3} \tag{RD3} \label{law:RD3} \\
    \rc{P_1}{P_2}{P_3} \relsemi \IIsrd &~~=~~ \rc{P_1}{P_2}{P_3} \tag{RD4} \label{law:RD4} \\
    \rc{P_1}{P_2}{\false} \relsemi \rc{Q_1}{Q_2}{Q_3} &~~=~~ \rc{P_1}{P_2}{\false} \tag{RD5} \label{law:RD5} \\
    \Miracle \relsemi \rc{P_1}{P_2}{P_3} &~~=~~ \Miracle \tag{RD6} \label{law:RD6} \\
    \Chaos \relsemi \rc{P_1}{P_2}{P_3} &~~=~~ \Chaos \tag{RD7} \label{law:RD7} \\
    \rc{\false}{P_2}{P_3} &~~=~~ \Chaos \tag{RD8} \label{law:RD8} \\
    \rc{P_1}{P_2}{P_3} \relsemi \Miracle &~~=~~ \rc{P_1}{P_2}{\false} \tag{RD9} \label{law:RD9} \\
    \rc{P_1}{P_2}{P_3} \relsemi \Chaos   &~~=~~ \rc{P_1 \land (P_3 \wpR \false)}{P_2}{\false} \tag{RD10} \label{law:RD10}
  \end{align*}
\end{theorem}
\noindent All of these laws can be proved by calculation using the definitions in Theorem~\ref{thm:rdescore} and laws in
Theorem~\ref{thm:rdes-comp}. \ref{law:RD1} establishes that a choice between a $\Miracle$ and $P$ yields $P$, since
$\Miracle$ is the top of the lattice. Similarly, \ref{law:RD2} establishes that a choice between $\Chaos$ and $P$ yields
$\Chaos$. The reactive skip is a left and right identity for any contract $P$, as this is stated by \ref{law:RD3} and
\ref{law:RD4}, respectively.

Law \ref{law:RD5} states that any non-terminating contract -- that is where the postcondition is $\false$ -- is a left
zero for sequential composition, as clearly then the successor is unreachable. Thus, in particular $\Miracle$ and
$\Chaos$ are both left zeros for sequential composition, as shown by \ref{law:RD6} and \ref{law:RD7}. Moreover,
\ref{law:RD7} shows that any reactive contract with a $\false$ precondition is $\Chaos$.

Law \ref{law:RD9} is a property first observed in \cite{Woodcock08}: placing a $\Miracle$ after a reactive design
eliminates final states, and yields a non-terminating process. Since it is impossible to reach a miraculous state,
inserting one prunes transitions that lead to it.

Finally, \ref{law:RD10} is a similar law for $\Chaos$, which likewise removes final states. Crucially, however, the
behaviour of $\Chaos$ is not impossible, but simply undesirable or unpredictable. Thus the composition additionally
inserts an assumption $P_3 \wpR \false$, which effectively states that postcondition $P_3$ should not be established,
because otherwise chaos will ensue. This explains Example~\ref{ex:divproc}: the left branch of the choice,
$a \then \Chaos$ is equivalent to $(a \then \Skip) \relsemi \Chaos$. The postcondition of $a \then \Skip$ is
$st' = st \land \trace = \langle a \rangle$.  The occurrence of $\Chaos$ mandates that this postcondition should not be
established, which means that trace extension is negated and added to the assumption, yielding the reactive condition
$\negr (\langle a \rangle \le \trace)$. This important distinction illustrates the difference between $\Miracle$ and
$\Chaos$ -- usually the latter is used to encode behaviour that should be prevented by the environment.

The next theorem gives the laws of reactive assignment.
\begin{theorem}[Reactive Assignment Laws] \label{thm:rea-asn}
  \begin{align*}
    \assignsR{id} &~=~ \IIsrd \tag{RA1} \label{law:RA1} \\
    \assignsR{\sigma} \relsemi \rc{P_1}{P_2}{P_3} &~=~ \rc{\substapp{\sigma}{P_1}}{\substapp{\sigma}{P_2}}{\substapp{\sigma}{P_3}} \tag{RA2} \label{law:RA2} \\
    \assignsR{\sigma} \relsemi \assignsR{\rho} &~=~ \assignsR{\rho \circ \sigma} \tag{RA3} \label{law:RA3} \\
    \assignsR{\sigma} \relsemi \Miracle &~=~ \Miracle \tag{RA4} \label{law:RA4} \\
    \assignsR{\sigma} \relsemi \Chaos &~=~ \Chaos \tag{RA5} \label{law:RA5}
  \end{align*}
\end{theorem}
\noindent Law \ref{law:RA1} establishes that an assignment using the identity function $id$ yields the reactive
skip. \ref{law:RA2} captures the effect of precomposing a reactive contract with an assignment; the assignment function
is applied as a substitution in the pre-, peri-, and postconditions. \ref{law:RA3} states that composition of two
assignments yields a single assignment built by composition of the individual assignment functions. Laws \ref{law:RA4}
and \ref{law:RA5} establish that $\Miracle$ and $\Chaos$ are both right zeros for assignment. This is because they both
remove final states, but, since assignments have no intermediate states, this eliminates all observable behaviours.

\subsection{Parallel Contracts}
\label{sec:parcontract}

\begin{figure}
  \centering\includegraphics[width=.5\linewidth]{figures/parallel-by-merge}

  \caption{Parallel-by-merge Dataflow}
  \label{fig:pbm}

\end{figure}

The final operator we tackle in this section is parallel composition, written $P \rcpar{M} Q$. Our definition of
parallel composition, elaborated in Section~\ref{sec:parallel}, uses the parallel-by-merge scheme developed as part of
UTP~\cite{Hoare&98}. Since different concurrency schemes are possible for reactive contracts, depending on the
underlying notion of trace, we cannot define a single parallel composition operator and so $P \rcpar{M} Q$ is parametric
over $M$. This is a merge predicate that defines how the state, traces, and any other observational variables should be
merged following execution of $P$ and $Q$.

We illustrate parallel-by-merge in Figure~\ref{fig:pbm}, where we assume the programs act on three variables, $x$, $y$,
and $z$. Parallel-by-merge splits the observation space into three identical segments: one for $P$, one for $Q$, and a
third that is identical to the original input. Relation $M$ then takes the outputs from $P$, $Q$, and the original
inputs, and merges them into a single output.

For reactive designs, the variables we need to merge are the state variables ($\state$), trace ($\trace$), and any
additional observational variables $r$. As an example, we present below the merge predicate for interleaving the events
of two \Circus processes~\cite{Hoare&98,Oliveira2005-PHD}.
\begin{example}[Interleaving Merge] \label{ex:interleave}
  \begin{align*}
    M_c ~~~\defs~~~& \trace \in (0.\trace \interleave_t 1.\trace) \land ref' \subseteq 0.\refu \cap 1.\refu \quad\mbox{where} \\[1ex]
    \langle\rangle \interleave_t xs ~~~=~~~ & xs \interleave_t \langle\rangle ~~~=~~~ \{xs\} \\
    \langle x \rangle \cat xs \interleave_t \langle y \rangle \cat ys ~~~=~~~
                 & \left\{\langle x \rangle \cat zs ~~ \middle| ~~ zs \in (xs \interleave_t \langle y \rangle \cat ys) \right\} ~\cup~ \\
                 & \left\{\langle y \rangle \cat zs ~~ \middle| ~~ zs \in (\langle x \rangle \cat xs \interleave_t ys) \right\} \\[1ex]
    P \interleave Q ~~~\defs~~~ & P \rcpar{M_c} Q
  \end{align*}

  \noindent In the definition of $P \rcpar{M} Q$, the trace and refusal variables are decorated with an index $0$ or $1$
  that determine whether the quantity originates from $P$ or $Q$, respectively. The binary operator $\interleave_t$
  interleaves two traces; it is a recursive function on sequences, returning a set of possible traces. The merge
  predicate, $M_c$, firstly constructs the overall trace $\trace$ as one of all possible interleavings, and secondly
  states that an event is only refused if it is refused by both processes. Our merge predicate leaves the state variable
  $\state$ unspecified as the \Circus interleaving operator hides any internal state, since they can not in general be
  merge without further machinery for shared variables. We then define the interleaving operator $P \interleave Q$ using
  the parametric reactive design parallel composition operator $\rcpar{\cdot}$, which is formally defined in
  Section~\ref{sec:parallel}. \qed
\end{example}
For the purpose of generic laws, we assume that any merge predicate yields well-formed traces, and furthermore is
symmetric. Symmetry in this context means that the merge predicate has no bias towards either of its operands and yields
the same result if they are swapped. This is clearly the case in Example~\ref{ex:interleave}, since both the traces and
refusals are composed by symmetric operators, namely $\interleave_t$ and $\cap$. The following theorem describes the
result of composing two contracts.
\begin{theorem}[Reactive Design Parallel Composition] \label{thm:rdespar} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/rea_designs/utp_rdes_parallel.thy\#L769}
  \begin{align*}
    &\rc{P_1}{P_2}{P_3} \rcpar{M} \rc{Q_1}{Q_2}{Q_3} = \\[.5ex]
    & \qquad \rc{\begin{array}{l}
          (P_1 \rimplies P_2) \wppR{M} Q_1 \land \\
          (P_1 \rimplies P_3) \wppR{M} Q_1 \land \\
          (Q_1 \rimplies Q_2) \wppR{M} P_1 \land \\
          (Q_1 \rimplies Q_3) \wppR{M} P_1
       \end{array}}{\begin{array}{l}
          P_2 \rcmergee{M} Q_2 ~\lor~ \\[1ex]
          P_3 \rcmergee{M} Q_2 ~\lor~ \\[1ex]
          P_2 \rcmergee{M} Q_3
       \end{array}
       }{P_3 \parallel_{\text{\tiny $M$}} Q_3}
  \end{align*}
\end{theorem}
\noindent The precondition is expressed in terms of a reactive condition combinator $\wppR{M}$. This is a form of
weakest rely condition: $A \wppR{M} B$ describes the weakest context in which reactive relation $A$ does not violate
reactive condition $B$. This is necessary because in a composition like $P \rcpar{M} Q$, the reactive processes $P$ and
$Q$ interfere and this can lead to the violation of their preconditions. Thus, the overall precondition of a parallel
composition itself assumes that such interferences do not occur. Interferences cannot occur in
Example~\ref{ex:interleave}, since there is no synchronisation, but, in general, of course it can happen when more
specialised merge predicates are employed. The definition of $\wppR{M}$ is elided for now, as it requires further
elaboration of the UTP theory, but is given in Section~\ref{sec:grd}, Definition~\ref{def:wppR}. It obeys several
theorems that are shown below:

\begin{theorem}[Weakest Rely Laws] \label{thm:wrlaws} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/rea_designs/utp_rdes_parallel.thy\#L720}
  $$ \false \wppR{M} P = \truer \qquad
    P \wppR{M} \truer = \truer \qquad
    \left(\bigsqcap_{i \in I} ~ P(i)\right) \wppR{M} Q = \left(\bigwedge_{i \in I} ~ (P(i) \wppR{M} Q)\right)
  $$
\end{theorem}

The laws show, respectively, that (1) a miraculous reactive relation satisfies any precondition, (2) any reactive
relation satisfies a true precondition, and (3) the weakest rely condition of a disjunction of relations is the
conjunction of their weakest rely conditions.

The parallel composition precondition in Theorem~\ref{thm:rdespar} states that the respective preconditions of the two
contracts, $P_1$ and $Q_1$, are not violated, neither by the opposing periconditions -- respectively $Q_2$ and $P_2$ --
under their respective preconditions, or the opposing postconditions -- respectively $Q_3$ and $P_3$. The pericondition
of the parallel reactive contract is written in terms of operator $P \rcmergee{M} Q$ that merges the traces but not the
states, since this is concealed in intermediate observations. A parallel process is in an intermediate state if either
of the composed processes is. Finally, the postcondition merges the final trace and state of each process, directly using
the parallel by merge operator ($\parallel_M$). We formally define all these operators in Section~\ref{sec:parallel}.

We can use Theorems~\ref{thm:rdespar} and \ref{thm:wrlaws} to prove the following theorem; for illustration we elaborate
the complete calculation.
\begin{theorem} \label{thm:miracle-anhil} $\Miracle \rcpar{M} P = \Miracle$ \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/rea_designs/utp_rdes_parallel.thy\#L813} \end{theorem}
\begin{proof}
  \begin{align*}
    \Miracle \rcpar{M} P
    &= \rc{\truer}{\false}{\false} \rcpar{M} \rc{P_1}{P_2}{P_3} \\
    &= \rc{\begin{array}{l}
        (\truer \rimplies \false) \wppR{M} P_1 \land \\
        (\truer \rimplies \false) \wppR{M} P_1 \land \\
        (P_1 \rimplies P_2) \wppR{M} \truer \land \\
        (P_1 \rimplies P_3) \wppR{M} \truer
      \end{array}}{
      \begin{array}{l}
        \false \rcmergee{M} P_2 ~\lor~ \\
        \false \rcmergee{M} P_2 ~\lor~ \\
        \false \rcmergee{M} P_3
      \end{array}
    }{\false \parallel_{\text{\tiny M}} P_3} & [\ref{thm:rdespar}] \\
    &= \rc{\begin{array}{l}
        \false \wppR{M} P_1 \land \false \wppR{M} P_1 \land \\
        \truer \land \truer
      \end{array}}{
      \begin{array}{l}
        \false ~\lor~  \false ~\lor~ \false
      \end{array}
    }{\false} & [\ref{thm:wrlaws}] \\
    &= \rc{\begin{array}{l}
        \truer \land \truer
      \end{array}}{
      \begin{array}{l}
        \false
      \end{array}
    }{\false} & [\ref{thm:wrlaws}] \\
    &= \rc{\truer}{\false}{\false} \\
    &= \Miracle & \qedhere
  \end{align*}
\end{proof}
\noindent This law shows that composition of any predicate with a miracle always yields a miracle, regardless of the
merge predicate. The intuitive property that $\Chaos$ is similarly an annihilator depends on the form of merge
predicate, and so this cannot be proved in general. We perform a further example calculation using the interleaving
operator from Example~\ref{ex:interleave}.

\begin{example}[Interleaving Calculation] \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/tutorial/utp_csp_ex.thy}
\begin{align*}
  & \quad~~ a \then \Skip \interleave b \then \Stop \\[.5ex]
  & = \rcs{a \notin \refu' \land \trace = \snil}{\state' = \state \land \trace = \langle a \rangle} \interleave
    \rcs{a \notin \refu' \land \trace = \snil \lor \trace = \langle b \rangle}{\false} \\[.5ex]
  & = \rcs{
    \begin{array}{l}
      (a \notin \refu' \land \trace = \snil) \rcmergee{M_C} (b \notin \refu' \land \trace = \snil) \lor \\
      (a \notin \refu' \land \trace = \snil) \rcmergee{M_C} (\trace = \langle b \rangle) \lor \\
      (\state' = \state \land \trace = \langle a \rangle) \rcmergee{M_C} (b \notin \refu' \land \trace = \snil) \lor \\
      (\state' = \state \land \trace = \langle a \rangle) \rcmergee{M_C} (\trace = \langle b \rangle)
    \end{array}}{(\state' = \state \land \trace = \langle a \rangle) \parallel_{\text{\tiny $M$}} \false} \\
  & = \rcs{
    \begin{array}{l}
      (a \notin \refu' \land b \notin \refu' \land \trace = \snil) \lor \\
      (a \notin \refu' \land \trace \in \{\snil, \langle b \rangle\}) \lor \\
      (b \notin \refu' \land \trace \in \{\snil, \langle a \rangle\}) \lor \\
      (\trace = \langle a, b \rangle)
    \end{array}}{\false} \\
  & = \rcs{\conditional{(a \notin \refu' \land b \notin \refu')}{\trace = \snil}{\left(\begin{array}{l} a \notin \refu' \land \trace = \langle b \rangle \\ \lor b \notin \refu' \land \trace = \langle a \rangle \\ \lor \trace = \langle a, b \rangle} \end{array}\right)}{\false} \\
  & = a \then b \then \Stop \extchoice b \then a \then \Stop
\end{align*}
\noindent We use the abbreviation $\rcs{P_2}{P_3}$ for a contract with a $\truer$ precondition. In the first step, we
calculate the meaning of the two sequential processes using Examples~\ref{ex:prefix} and \ref{ex:termdead}, with Theorem
\ref{thm:rdes-comp}. We then employ Theorem~\ref{thm:rdespar} to expand out the overall parallel reactive
contract. There is no possibility of divergence, so the preconditions remain trivial. For the pericondition we need to
merge each quiescent observation with every opposing quiescent or final observation. The result is the four conjuncts
displayed. In the postcondition, we have to merge the two overall postconditions. The overall postcondition becomes
$\false$, because $\Stop$ prevents the overall operator from successfully terminating. In the pericondition, we
calculate the four merged quiescent observations. These characterise the states when (1) no event has yet occurred, and
we are accepting $a$ or $b$; (2) either $\snil$, or else $\langle b \rangle$ has occurred and $a$ remains enabled, which
includes the situation when the right hand action has performed a transition; (3) the symmetric case to (2) with $a$
potentially having occurred; and (4) both events have occurred and no event is enabled: the refusal set is
unconstrained. In common with the semantics of CSP\cite{Roscoe2005}, we observe that the set of possible refusals is
downward closed under $\subseteq$ for every trace combination. We can then in fact show that this contract is
equivalent to an external choice using the definition given in Example~\ref{ex:extchoice}. \qed
\end{example}

This completes our exposition of the calculational laws for our reactive contract theory. All the theorems presented
have been mechanically checked, as we discuss in Section~\ref{sec:mech}. In the next section we illustrate their use in
verification.

\subsection{Unifying Theories of Programming}

Programming and modelling languages often encompass a number of paradigms that are used to variously abstract the
world. Whilst general purpose languages exist which allow programming in any paradigm, such as object oriented,
concurrent, real-time, hybrid, and functional, domain specific languages are more conservative, encapsulating only one
or two. Unifying Theories of Programming (UTP) is a framework for formalisation and combination of theories that
underlie the foundational semantics of programming languages. A UTP theory, in this context, encapsulates a set of laws
that characterise a particular paradigmatic aspect of a language. For instance, one can identify a UTP theory for
real-time programs where a clock can be observed that provides information about the duration of a
computation.

In UTP, programs and models are encoded using a language of alphabetised predicates, following the
``programs-as-predicates'' philosophy. Reasoning about the behaviour of a program thus reduces to deduction in formal
logic, which provides us with a way of proving the laws of programming. UTP is therefore fundamentally denotational in
nature, since every programming language construct can be formally defined in terms of logical constructs, such as
conjunction, negation, and quantification. For example, it is well known that the imperative programming operators of
assignment, sequential composition, and the if-then-else conditional (written here in infix notation) can be logically
denoted as below:

\begin{definition}[Imperative programming constructs]
  \label{def:imper}
  \begin{align*}
    x := v       & ~~\triangleq~~ x' = v \land y_1' = y_1 \land \cdots \land y_n' = y_n \\[.5ex]
    P \relsemi Q & ~~\triangleq~~ \exists x_0 @ P[x_0/x'] \land Q[x_0/x] \\[.5ex]
    \conditional{P}{b}{Q} & ~~ \triangleq~~ (b \wedge P) \vee (\neg b \wedge Q)
  \end{align*}
\end{definition}

Such definitions give us a natural model for the algebraic laws of programming~\cite{Hoare87}, which can then be
employed in building programming verification tools~\cite{Armstrong2015}. Indeed programs-as-predicates is a very
natural fit to theorem proving since proof about a program reduces to a problem in Higher-Order Logic, which can often
be discharged using automated theorem proving, a fact we harness in our Isabelle-based UTP theorem prover,
Isabelle/UTP~\cite{Foster16b}. All the algebraic laws presented in this paper have been verified in Isabelle/UTP.

Going beyond simple imperative programs require that we consider UTP theories, that enrich the language of relations.
Concretely, a UTP theory consists of (1) a set of observational variables $A$ (the alphabet); (2) a set of healthiness
conditions; and (3) a signature. In order to exemplify, we will create a simple UTP theory of time $\theory{T}$. The
alphabet denotes the aspects of the world we wish to observe in the particular abstract setting. For example, theory
$\theory{T}$ could have variables $time, time' : \mathbb{R}$ that give the time before and after a
computation. Conversely, there are often situations when we may wish to abstract time, and may want to elide such a
variable. This is essence of the UTP's empirical approach: isolating aspects of the universe that we are interested in
to solve a particular problem.

The healthiness conditions denote invariants on the observational variables that define the correct behaviour of the
universe. Continuing our example, a possible healthiness condition is $time \le time'$, which means that the clock
cannot run backwards, which reflects our intuition of how time behaves. The signature of the theory consists of
constructs for building models that are healthy theory elements. For example, we might have a construct
$$\textbf{Wait}(n) \defs time' = time + n \land \II_{A \setminus \{time\}}$$ which introduces a delay of $n$ seconds.

Healthiness conditions, $\healthy{H}$, in UTP are expressed on functions on predicates, which should usually be (1)
idempotent and (2) monotone. Such a healthiness function when applied to a predicate yields a ``healthy'' predicate,
that is a valid element of the UTP theory. A predicate which satisfies $P = \healthy{H}(P)$ is called
$\healthy{H}$-healthy: it is a fixed point of $\healthy{H}$. Idempotence, defined as $\healthy{H} \circ \healthy{H} =
\healthy{H}$, means that application of a healthiness function need only be done once, and the resulting predicate
cannot be made more healthy. Monotonicity, defined as $P \sqsubseteq Q \implies \healthy{H}(P) \sqsubseteq
\healthy{H}(Q)$, means that the healthiness function preserves the refinement order on the original predicate. In our
theory of time, we can define our healthiness condition as $HT(P) = time \le time' \land P$, the application of which
restricts a predicate to healthy behaviours. $HT$ is both idempotent, since $time \le time' \land time \le time' \land P
= time \le time' \land P$, and also monotone since $\land$ is monotone.

\subsection{Design-by-Contract}

Design-by-Contract~\cite{Meyer92,Jones2003,Bauer2012} (DbC) is a compositional program construction and verification
technique. In DbC, one demonstrates composite system level properties by decomposing them into a number of contracts for
each component subsystem. Each contract specifies the guarantees that the subsystem will make about its behaviour, under
certain specified assumptions on the subsystem's environment. Meyer~\cite{Meyer92} coined the term when arguing the need
for precisely specified behavioural assertions about a program's behaviour to ensure reliability of component based
software systems. These assertions come in three forms: preconditions, postconditions, and invariants.

Meyer's work has its foundation in the work of Floyd~\cite{Floyd67} and Hoare~\cite{Hoare69} on proving correctness of
programs in terms of the commonly known Hoare triple $\lamporttriple{p}{Q}{r}$. This asserts that if program $Q$ is
started in a state satisfying predicate $p$ then, provided the program terminates, the final state will satisfy
predicate $r$. Effectively the Hoare triple is setting up a primitive contract for $Q$ that mandates a particular
relationship between inputs and outputs.

DbC is perhaps even more clearly seen in the work on refinement calculus~\cite{Mor1990}. Here, a programming language is
extended with a specification statement $w:[pre, post]$, where $pre$ is the precondition, $post$ the postcondition, and
$w$ the ``frame'' -- that is the set of variables that are allowed to change. A specification statement is to be
converted into a block of executable code through a series of correctness preserving refinements that variously divide
the specification into constituent parts, and eventually to atomic commands. Both Hoare logic and the refinement
calculus can be unified either algebraically~\cite{Gomes2016} or else denotationally using the UTP theory of
designs~\cite{Hoare&98}, which we discuss in Section~\ref{sec:designs}.

Moving beyond imperative programs to concurrent and reactive behaviours, where assumptions and guarantees range over the
entire history of interaction and not simply initial and final states, requires a richer form of
contract~\cite{Benveniste2007,Bauer2012,Champion2016}. Benveniste et al.~\cite{Benveniste2007} describe contracts
denotationally as pairs of predicates $C \defs (A, G)$ where $A$ is the assumption, and $G$ is the guarantee. $A$ and
$G$ both characterise the set of program variable traces that prescribe valid behaviours of the context and given
component, respectively. They define a notion of refinement, $C_1 \preceq C_2$ called dominance --- to distinguish it
from refinement to implementation -- which requires that the assumption be weakened and guarantee be strengthened. They
also define an algebra for contracts including parallel composition $C_1 \parallel C_2$, disjunction $C_1 \sqcap C_2$,
and conjunction $C_1 \sqcup C_2$. Works building on this framework~\cite{Cimatti2012,Cimatti2015} allow step-wise
refinement of contracts, and verification based on temporal logic properties. It is this notion of reactive contract
that our work speaks into.

\subsection{Designs}
\label{sec:designs}

The UTP theory of designs~\cite{Hoare&98,Cavalcanti&06} allows the specification of programs in a contractual manner in
terms of assumptions and guarantees, which we also call commitments. The theory has two observational variables,
$ok, ok' : \Bool$, flags that denote whether a program was started and whether it terminated, respectively. The
signature of the theory of designs consists of the operator $\design{P}{Q}$, that means that if a program is started and
the state satisfies assumption $P$, then it will terminate and satisfy commitment $Q$. This is denoted as follows:
\begin{definition}{Designs}
  \begin{align*}
    \design{P}{Q}   ~~\defs~~& (ok \land P) \implies (ok' \land Q)
  \end{align*}
\end{definition}
\noindent Here, $P$ and $Q$ are both relations on variables excluding $ok$ and $ok'$. Effectively this encoding allows a
pair of predicates to be encoded as a single predicate, such that designs effectively implement Benveniste's contract
framework~\cite{Benveniste2007}. We can thus define functions $\preD{D}$ and $\postD{D}$ that extracts the assumptions
and commitments, respectively, from a design, such that

$$\preD{P \shows Q} = P \quad\textrm{and}\quad \postD{P \shows Q} = (P \implies Q)$$

Designs are closed under sequential composition, disjunction, and conjunction, the latter of which give rise to near
identical operators present in~\cite{Benveniste2007}. Indeed, it is possible to prove the definitions of their operators
as theorems. Moreover, refinement of two designs $\design{P_1}{P_2} \refinedby \design{Q_1}{Q_2}$ requires that we can
demonstrate $P_1 \implies Q_1$ and $Q_2 \land P_1 \implies P_2$, that is we weaken the assumption and strengthen the
commitment. The theory of designs is therefore a very natural contract theory.

The healthiness conditions of designs characterise the associated UTP theory, and are given
below~\cite{Hoare&98,Cavalcanti&06}.
\begin{definition}{Design Healthiness Conditions}
  \begin{align*}
    \healthy{H1}(P) ~~\defs~~& (ok \implies P) \\
    \healthy{H2}(P) ~~\defs~~& P \relsemi \ckey{J} \\
    \ckey{J}        ~~\defs~~& ((ok \implies ok') \land \II_{A \setminus \{ok\}}) \\
    \healthy{H3}(P) ~~\defs~~& P \relsemi \IID \\
    \IID            ~~\defs~~& \design{\true}{\II} \\
    \healthy{H} &= \healthy{H1} \circ \healthy{H2} \\
    \healthy{N} &= \healthy{H1} \circ \healthy{H3}
  \end{align*}
\end{definition}
Designs are fixed-points of the healthiness condition $\healthy{H}$ which is composed of $\healthy{H1}$ and
$\healthy{H2}$. $\healthy{H1}$ states that until a design has been given permission to execute via $ok$, no observations
are possible. $\healthy{H2}$ states that no design can require non-termination. A more intuitive form that characterises
fixed-points is $P[false/ok'] \implies P[true/ok']$: every non-terminating behaviour for which $ok' = false$ has an
equivalent terminating behaviour for which $ok' = true$. $\healthy{H3}$ designs additionally require that $P$ is a
condition: it does not refer to dashed variables. The latter subclass is useful for ``normal'' specifications where the
assumption does not refer to the final state. $\ckey{H3}$ designs, with a few notable exceptions, are the most common
form of design, and are thus sometimes known as \emph{normal designs}~\cite{Guttman2010}, as indicated by healthiness
condition $\healthy{N}$.

The following theorems then demonstrate the relationship between syntactic designs and the healthiness conditions.

\begin{theorem}{Design correspondences}
  \begin{align*}
    \healthy{H}(P) &= \design{\preD{P}}{\postD{P}} \\
    \healthy{N}(P) &= \design{(\preD{P} \relsemi \true)}{\preD{P}}
  \end{align*}
\end{theorem}

Any $\healthy{H}$ predicate can thus be written using the design turnstile, if the precondition and postcondition are
extracted. Moreover, an $\healthy{N}$ predicate is a design whose precondition has $\true$ as a right unit and thus does
it does not refer to dashed variables. Designs allow us to unify various assertional reasoning techniques, notably Hoare
logic and refinement calculus, as shown below:
\begin{align*}
  \lamporttriple{p}{Q}{r} &~~\defs~~ (\design{p}{r} \refinedby Q) \\
  w:[pre, post] &~~\defs~~ (\design{pre}{post \land \II_{A \setminus w}})
\end{align*}
\noindent Designs are therefore an extremely versatile specification mechanism providing support for a number
verification techniques.

\subsection{Generalised Reactive Processes}
\label{sec:bg-grp}

The theory of reactive processes~\cite{Hoare&98,Cavalcanti&06} unifies the semantics of different reactive
languages. Reactive languages differ from imperative programs in that they have intermediate observable states as well
as final states, where the process awaits interactions from its environment. The UTP theory of reactive processes has,
in addition to $ok$ and $ok'$, three pairs of observational variables $wait, wait' : \Bool$ that determine whether a
process (or its predecessor) is waiting for interaction with its environment or else has terminated,
$tr, tr' : \seq\,\textit{Event}$ that describes the trace before and after the process' execution, and
$ref, ref' : \power \textit{Event}$ that describe the events being refused during an intermediate state, as required by
the failures model of CSP~\cite{Hoare85}.

In our previous work~\cite{Foster17a} we have shown how the UTP theory of reactive processes can be generalised by
characterising the trace model with an abstract algebra, called a \emph{trace algebra}. From these algebraic foundations
we have reconstructed the complete theory of reactive processes, including its healthiness conditions and associated
laws, in particular those for sequential and parallel composition.

\begin{definition}[Trace algebra] \label{def:tralg} A trace algebra $(\tset, \tcat, \tempty)$ is a cancellative monoid
  satisfying the following the axioms:
\begin{align*}
  x \tcat (y \tcat z) &~=~ (x \tcat y) \tcat z \tag{TA1} \\
  \tempty \tcat x = x \tcat \tempty &= x \tag{TA2} \label{law:tunit} \\
  x \tcat y = x \tcat z ~~\implies~~  y &= z \tag{TA3} \label{law:tcancl1} \\
  x \tcat z = y \tcat z ~~\implies~~  x &= y \tag{TA4} \label{law:tcancl2} \\
  x \tcat y = \tempty  ~~\implies~~  x &= \tempty \tag{TA5} \label{law:tnai}
\end{align*}
\end{definition}

\noindent Operator $s \tcat t$ denotes trace concatenation, and $\tempty$ the empty trace. From these definitions and
axioms the usual operations of trace prefix ($s \le t$) and subtraction ($s - t$) can be derived and usual algebraic
laws proved as theorems~\cite{Foster17a}. Naturally, sequences are a model of the trace algebra, as are, for example,
piecewise continuous trajectories that are the basis of the denotational semantics of hybrid systems. From the trace
algebra we recreate the three reactive healthiness conditions.
\begin{definition} Reactive healthiness conditions
  \begin{align*}
    \healthy{R1}(P) & \defs P \land tr \le tr' \\
    \healthy{R2}_c(P) & \defs \conditional{P[\tempty, tr' \tminus tr/tr, tr']}{tr \le tr'}{P} \\
    \healthy{R3}(P) & \defs \conditional{\II}{wait}{P} \\
    \healthy{R} & \defs \healthy{R3} \circ \healthy{R2}_c \circ \healthy{R1}
  \end{align*}
\end{definition}
$\healthy{R1}$ states that $tr$ is monotonically increasing; processes are not permitted to undo past
events. $\healthy{R2}_c$ states that a process must be history independent: the only part of the trace it may constrain
is $tr' \tminus tr$, that it, the portion since the previous observation $tr$. Specifically, if the history is deleted,
by substituting $\tempty$ for $tr$ and $tr' - tr$ for $tr'$, then the behaviour of the process is unchanged. Our
formulation of $\healthy{R2}_c$ deletes the history only when $tr \le tr'$, which ensures that $\healthy{R2}_c$ does not
depend on $\healthy{R1}$, and thus commutes with it. Finally, $\healthy{R3}$ states that if a prior process is
intermediate ($wait'$) then the current process must identify all variables. We then compose the three to yield
$\healthy{R}$, the overall healthiness condition of reactive processes.

\subsection{Reactive Designs}

The UTP theory of reactive designs is an important foundation for reactive contracts that we will extend and elaborate
in this work. A reactive design is essentially a predicate that has all the healthiness conditions for both the design
theory ($\healthy{H}$) and the reactive process theory ($\healthy{R}$). Alternatively, a reactive design can be
characterised as a design which is make reactive: $\healthy{R}(\design{P}{Q})$, where $P$ is an assumption and $Q$ a
commitment, both of which can potentially refer to both state variables and the trace.

Designs and reactive processes are disjoint theories because $\healthy{H1}$ does not commute with either $\healthy{R1}$
or $\healthy{R3}$. Consequently, the order in which the healthiness conditions are applied is important: $\healthy{R3}$
must be applied first, followed by $\healthy{H1}$, and finally $\healthy{R1}$. The order of application of
$\healthy{H2}$ and $\healthy{R2}$ not important. In order to overcome the need for a specific order, the theory of
reactive designs introduces three derived healthiness conditions.

\begin{definition}
  \begin{align*}
    \healthy{CSP1}(P) ~\defs~& P \lor \neg ok \land (tr \le tr') \\
    \healthy{CSP2}(P) ~\defs~& \healthy{H2}(P) \\
    \healthy{R3}_c(P) ~\defs~& \conditional{\healthy{CSP1}(\II)}{wait}{P}
  \end{align*}
\end{definition}

\noindent $\healthy{CSP1}$ is equivalent to $\healthy{H1} \circ \healthy{R1}$, and unlike $\healthy{H1}$ does commute
with $\healthy{R1}$. Intuitively, $\healthy{CSP1}$ states that if $ok$ is not true, and thus we do not have permission
to execute, then the only predictable behaviour is that the trace must monotonically increase. Thus if a predecessor
commits erroneous behaviour ($\neg ok'$) through, for instance, having is assumption violated, then future behaviour is
unpredictable. $\healthy{CSP2}$ is simply $\healthy{H2}$, though with the alphabet extended with the reactive
observational variables. $\healthy{R3}_c$ is $\healthy{R3}$, but where the skip operator is made $\healthy{CSP1}$
healthy. In the UTP book~\cite{Hoare&98}, $\healthy{R3}_c$ is simply called $\healthy{R3}$, but their operator overloads
$\II$ to be either the operator we give here, or else the version of $\healthy{R3}$ we described in
section~\ref{sec:bg-grp}, which are both needed depending on whether one would like to handle divergence or not.

To exemplify reactive designs, consider the semantics of the simple assignment $x := f(e)$. It could be given as the
design $e \in \dom(f) \shows x' = f(e) \land y' = y$, for a program that has two programming variables $x$ and $y$. This
is not a reactive process, since it is not reactive-healthy: it executes even in its predecessor's wait-state. We can
make reactive-healthy by applying the appropriate reactive heathiness conditions. Here, we need both $\healthy{R1}$ and
$\healthy{R3}_c$. The result, $\healthy{R1} \circ \healthy{R3}_c(e \in \dom f \shows x' = f(e) \land y' = y)$, is a
reactive design. In general, we also apply $\healthy{R2}_c$ to ensure that the inner design does not attempt to observe
the trace history, though in this case $e \in \dom f \shows x' = f(e) \land y' = y$ is already $\healthy{R2}_c$
healthy. It would also be useful to go one step further and add the equality $tr' = tr$ to the postcondition before we
apply $\healthy{R}$ so that the trace is unchanged by the assignment, without this its behaviour is unpredictable beyond
$tr \le tr'$. The pay-off here is to add the theory of contracts provided by designs to the theory of reactive
processes, and in doing so extend its applicability to all the constructs found in common process algebras, including
parallel composition of processes, non-terminating recursive processes, channel communications, and abstraction
constructs including concealment of communications.

The idea of a reactive design as a semantic concept in its own right is a direct consequence of a result due to Hoare \&
He~\cite[Theorem 8.2.2]{Hoare&98}. This theorem states that CSP processes form a lattice closed under sequential
composition and containing the assignment $\healthy{R}(x:=e)$, for stored program variables $x$ and expressions $e$ over
these variables and suitable constants. The proof of the first claim is outlined by noting that $P$ is a CSP process
(that is, it satisfies the CSP healthiness conditions) iff
$$
  P = \healthy{R1}(\lnot P[false/wait,false/ok'] \shows P[false/wait,true/ok'])
$$
That is, every CSP-healthy process can be expressed as a design made reactive-healthy.

Cavalcanti \& Woodcock~\cite{Cavalcanti&06} discuss how this theorem accounts for a style of specification for CSP
processes, where the precondition of the design characterises the process's divergences and its postcondition describes
its failures (in the CSP sense). This paper also casts the semantics of some individual operators as reactive designs,
notably external choice.

The theory of reactive designs is of particular importance to the \Circus language family. \Circus is a language for
description of concurrent processes that interact via channels in a similar way to CSP~\cite{Hoare85}. Different to CSP
though, each process has encapsulated state variables that can be manipulated using assignments. The state is isolated
from other processes and the only form of data sharing remains the channels. Typical constructs of \Circus include

\begin{itemize}
  \item event prefix $a \then P$: perform event $a$ and then behave the $P$;
  \item assignment $x := v$: assign expresssion $v$ to local state variable $x$;
  \item external choice $P \extchoice Q$: pick $P$ or $Q$ depending on the offered events;
  \item the deadlocked process $\Stop$: it can make no progress and offer no events;
  \item guarded process $g \guard P$: behaves like $P$ is $b$ is true, otherwise deadlocks.
\end{itemize}

\noindent \Circus also has operators usual in a programming language like sequential composition, if-then-else, iteration, and
recursion. Moreover it has operators for parallel composition of processes, including explicit event sharing, and also
event abstraction. \Circus can properly be called a contract-based language, in as much as every construct of the
language can be described using a reactive design~\cite{Oliveira2005-PHD,Oliveira&09}.

Woodcock~\cite{Woodcock08} considers the top element of the lattice of reactive designs: miracle of reactive processes:
$\healthy{R}(\true \shows \false)$. This is the reactive design that is always guaranteed to terminate if it is started,
and when it does terminate, it achieves the impossible. He explores consequences of having such a process in combination
with some of the other operators in a process algebra. Its effect in the language is to prune away behaviour. For
example, the process
$$
  a \then \Miracle = \healthy{R}(\true \shows tr' = tr \land a \notin ref' \land wait' \land v'=v)
$$
If properly started, this process nevers refuses the event $a$, but the event never happens, since the resulting
behaviour would be miraculous. Perhaps more useful is the interaction with external choice:
$$
  a \then Skip \extchoice \Miracle =
  \healthy{R}(\true \shows \lnot wait' \land tr' = tr \cat \langle a \rangle \land v'=v)
$$
This process terminates immediately, having performed the event $a$. There is no state in which the process is waiting
for the environment to perform $a$, it simply happens instantly. Intuitively, we can think of this as an urgent
event. Woodcock suggests a couple of practical applications for miracles: ordered simultaneous events, where a second
event follows urgently on the heels of a first event
$$
  a \then (b \then Skip \extchoice \Miracle)
$$
and a hard deadline operator for timed CSP:
$$
  (a \then Skip) \timeout{10} \Miracle
$$
Here, the event $a$ is offered to the environment. If the environment fails to engage in this event before 10 seconds
have elapsed, then the process times out and behaves like a miracle. But this is impossible behaviour and there is no
alternative to meeting the deadline.

Butterfield et al.~\cite{BGW09} study the problem of state visibility in an imperative process algebra, noting that the
observation of program state is miraculous while waiting for an external choice to be resolved for $\healthy{R3}_c$
predicates. In this work he replaces the standard healthiness condition $\healthy{R3}$ with a variant called
$\healthy{R3}_h$, that causes internal state updates to be abstracted in intermediate obervations, that we shall utilise
in Section~\ref{sec:grd}.

\subsection{UTP}
\label{sec:utp}

UTP~\cite{Hoare&98} seeks to identify the fundamental computational paradigms that exist as foundations of programming
language semantics and formalises them using UTP theories. UTP theories can describe what it means for a language to be
concurrent~\cite{Hoare&98,Cavalcanti&06}, real-time~\cite{Sherif2010}, or object-oriented~\cite{SCS06}. The UTP thus
promotes reuse of theoretical building blocks that underlie programming languages.

UTP is based on an alphabetised relational calculus~\cite{Hoare&98} with operators of higher-order predicate calculus
and relation algebra. An alphabetised predicate $P$ consists of a set of typed variables $\alpha(P)$, and a predicate
which may refer to only those variables in $\alpha(P)$. Alphabetised relations are alphabetised predicates whose
alphabet consists of pairs of variables that denote initial values ($x$) and later values ($x'$). The relations are
ordered by refinement, $P \refinedby Q$, which is denoted below:

\begin{definition} $P \refinedby Q ~ \defs ~ [Q \implies P]$ \label{def:refinement} where
  $\alpha(P) = \alpha(Q)$ \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/utp/utp_pred.thy\#L141}
\end{definition}

\noindent Here, $[P]$ denotes the universal closure of $P$; if $\alpha(P) = \{x_1 \cdots x_n\}$, then
$[P] \defs (\forall x_1 \cdots x_n @ P)$. Refinement states that the predicate $Q$ implies $P$ over all variables, and
thus $P$ sets an upper bound on the possible observations exhibited by $Q$. Consequently, $\refinedby$ is a partial
order on the set of alphabetised relations.

The domain of alphabetised relations forms a number of important algebraic structures including (1) a complete
lattice~\cite{Hoare&98}, where the order is refinement ($\refinedby$), $\false$ is top, and $\true$ is bottom; (2) a
relation algebra~\cite{Tarski41,Foster14}; (3) a cylindric algebra~\cite{Tarski71,Foster16a}; and (4) a
quantale~\cite{Foster16a}, which induces (5) a Kleene algebra~\cite{Armstrong2015}. Together these provide a rich set of
base properties supporting program verification~\cite{Armstrong2015,Foster16a}.

UTP follows the ``programs-as-predicates'' approach~\cite{Hehner93}, where a program is modelled as a relation in the
alphabetised predicate calculus. For example, an assignment $x := x + 1$, which increments variable $x$ whilst leaving
all other variables unchanged, can be denoted using the predicate $x' = x + 1 \land y' = y$, where $y$ denotes the
collection of variables other than $x$. Programming operators, such as sequential composition ($P \relsemi Q$),
if-then-else conditional ($\conditional{P}{b}{Q}$), non-deterministic choice ($P \sqcap Q$), and recursion ($\mu F$),
are denoted as predicates~\cite{Hoare&98,Cavalcanti04}, as shown below.

\begin{definition}[UTP Programming Operators] \label{def:utp-prog} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/utp/utp_rel_laws.thy}
  \begin{align*}
    P \relsemi Q &\defs \exists v_0 @ P[v_0/v'] \land Q [v_0/v] & \alpha(P) = \alpha(Q) = \{v, v'\} \\
    x := v &\defs x' = v \land y' = y \land \cdots \land z' = z \\
    \II    &\defs x := x \\
    \bigsqcap_{i \in I} \, P(i)  &\defs \bigvee i \in I @ P(i) \\
    \conditional{P}{b}{Q} &\defs (b \land P) \lor (\neg b \land Q) & \alpha(P) = \{v, v'\}, \alpha(b) = \{v\} \\
    \mu F &\defs \bigsqcap \{ X | F(X) \refinedby X \}
  \end{align*}
\end{definition}

Moreover, the empty relation $\false$ is usually used to denote either a program that fails to terminate, or else is
``miraculous'', having no possible behaviours. This embedding of programs into logic naturally provides great
opportunities for verification by automated proof~\cite{Foster16a}. Moreover, the standard laws of
programming~\cite{Hoare87} are all theorems with respect to the operator denotations. We also emphasise that these
operators are all alphabet polymorphic, and can therefore be used to compose predicates of varying types, so long as the
side conditions are satisfied. A selection of theorems of Definition~\ref{def:utp-prog} is shown below.

\begin{theorem}[Relational Calculus Laws] \label{thm:rellaws} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/utp/utp_rel_laws.thy}

\noindent\begin{minipage}{.5\linewidth}
\begin{align*}
  P \relsemi \II = \II \relsemi P &= P \\
  P \relsemi \false = \false \relsemi P &= \false \\
  (P \relsemi Q) \relsemi R &= P \relsemi (Q \relsemi R) \\
  (\conditional{P}{b}{Q}) \relsemi R &= \conditional{P \relsemi R}{b}{Q \relsemi R}
\end{align*}
\end{minipage}
\begin{minipage}{.5\linewidth}
\begin{align*}
  \left(\bigsqcap_{i \in I} \, P(i)\right) \relsemi Q &= \bigsqcap_{i \in I} \, P(i) \relsemi Q \\[1ex]
  P \relsemi \left(\bigsqcap_{i \in I} \, Q(i)\right) &= \bigsqcap_{i \in I} \, P \relsemi Q(i)
\end{align*}
\end{minipage}
\end{theorem}

The relational skip ($\II$) is a left and right identity, and $\false$ is a left and right annihilator. Sequential
composition is associative, it distributes through conditional from the right (but not the left), and it distributes
through internal choice from the left and right.

UTP theories are well-defined subsets of the alphabetised relations that satisfy certain properties desirable for a
particular computational paradigm. For example, to model real-time programs, we need a way of recording how much time
has passed since execution began, and ensuring that the passage of time is well-behaved by, for instance, forbidding
reverse time travel. In UTP, this can be achieved by extending our alphabet with special observational variables, such
as $clock, clock' : \nat$, which can be used to model time, and imposing invariants, such as $clock \le clock'$. UTP
theories are therefore specified in terms of three parts:
\begin{enumerate}
\item an alphabet of typed \emph{observational variables}, which are used to encode observable semantic quantities
  important for the theory;
\item a \emph{healthiness condition} ($\healthy{HC}$), that specifies the invariants as a function from predicates to
  predicates with the above alphabet;
\item a \emph{signature}: that is, a set of constructors and operators that are healthy elements of the theory.
\end{enumerate}
A theory's alphabet is often open to extension, such that additional observational variables can be added, or
the types of variables specialised, assuming a notion of subtyping exists. This also means that UTP theories can readily
be combined by merging the alphabets and composing the healthiness conditions.

If a relation is a fixed-point of the healthiness conditions, $P = \healthy{HC}(P)$, then it is said to be
$\healthy{HC}$-healthy. For our theory of real-time, we can specify a healthiness condition
$\healthy{HT}(P) \defs (P \land clock \le clock')$, which conjoins a relation with the invariant. Then we have it that
$$\textsf{delay}(n : \nat) \defs clock' = clock + n$$ is a $\healthy{HT}$-healthy relation, since it always satisfies $clock \le clock'$, and therefore is
is a fixed-point of $\healthy{HT}$.

A UTP theory's domain is the set of healthy predicates: $\theoryset{\healthy{HC}} \defs \{P | \healthy{HC}(P) = P\}$.
For this reason, it is necessary that a healthiness function is idempotent
($\healthy{HC} \circ \healthy{HC} = \healthy{HC}$), and usually also monotonic. Monotonicity ensures that the UTP theory
forms a complete lattice, substantiated by the Knaster-Tarski theorem~\cite{Tarski55}. This gives rise to a theory top
($\thtop{T}$), a bottom ($\thbot{T}$), an infimum ($\thinf{T}\,A$), for $A \subseteq \theoryset{\healthy{HC}}$, a
supremum ($\thsup{T}\,A$), a least fixed-point operator $\thlfp{T}\,F$, for
$F : \theoryset{\healthy{HC}} \to \theoryset{\healthy{HC}}$ and a greatest fixed-point operator $\thgfp{T}\,F$. The top and
bottom can be obtained by applying the healthiness condition to $\false$ and $\true$, respectively. However, the induced
lattice does not in general share the same operators as the alphabetised predicate lattice. Thus, for our purposes, we
are interested in the stronger property of \textbf{continuity}, which gives rise to additional properties.
\begin{definition}[Continuous Healthiness Conditions] \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/utp/utp_healthy.thy\#L112}

  \noindent\healthy{HC} is said to be continuous if it satisfies $\healthy{HC}(\bigsqcap A) = \bigsqcap \{ \healthy{HC}(P) | P \in A
  \}$ for $A \neq \emptyset$.
\end{definition}
\noindent This notion of continuity, also know as universal disjunctivity, is stronger than the related notion of
Scott-continuity~\cite{Scott71}, which requires that $A$ also be directed Every continuous healthiness condition is also
monotonic and thus induces a complete lattice. Continuity also means that the theory's infimum ($\thinf{T}$) is the same
operator as the alphabetised predicate infimum ($\bigsqcap$) for non-empty sets. So, a number of additional laws can be
imported into the theory, some of which are illustrated below.
\begin{theorem}[Continuous Theory Laws] \label{thm:contthm} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/utp/utp_theory.thy}
\begin{align}
  \thbot{T} &~~=~~ \healthy{HC}(\true) \\
  \thtop{T} &~~=~~ \healthy{HC}(\false) \label{thm:utp-lattice-top} \\
  \thbot{T} \intchoice P &~~=~~ \thbot{T} & \text{if $P$ is $\healthy{HC}$-healthy} \\
  \thtop{T} \intchoice P &~~=~~ P &\text{if $P$ is $\healthy{HC}$-healthy} \\
  \thinf{T} \, A &~~=~~ \bigsqcap \, A &\text{if $A \neq \emptyset$ and $A \subseteq \theoryset{\healthy{HC}}$} \\
  \thlfp{T} X @ F(X) & ~~=~~ \mu X @ F(\healthy{HC}(X)) & \text{if}~~ F : \theoryset{\healthy{HC}} \to \theoryset{\healthy{HC}} \label{thm:contthm-lfp}
\end{align}
\end{theorem}
For the first four these identities, monotonicity of $\healthy{HC}$ is actually a sufficient assumption. Of particular
interest is \eqref{thm:contthm-lfp} that shows how a theory's weakest fixed-point operator ($\thlfp{T}$) can be
rewritten to the alphabetised-predicate weakest fixed-point ($\mu$). The requirement is that the continuous healthiness
condition $\healthy{HC}$ can be applied after each unfolding of the fixed-point to ensure that the function $F$ is only
ever presented with a healthy predicate. It should be noted that this requirement for continuous healthiness functions
does not similarly restrict fixed-point functions. Specifically, our laws apply for any monotonic function $F$ and thus
at this level there is no restriction in modelling of unbounded non-determinism. Indeed, we have encountered very few
healthiness conditions that are monotonic but not continuous.

Healthiness conditions in UTP are often built by composition of several component functions. That being the case,
continuity and idempotence properties of the overall healthiness condition can also be obtained by composition.

Though UTP was originally a purely theoretical framework for denotational semantics~\cite{Hoare&98}, more recently it
has been adapted into an implementation within the Isabelle proof assistant~\cite{Isabelle}, called
Isabelle/UTP~\cite{Foster14,Foster16a}. This proof tool can be used develop UTP theories, by defining healthiness
conditions and proving algebraic laws, in order to support mechanically verified denotational semantics. Moreover, such
a mechanised denotational semantics can be used to construction verification tools for different languages by harnessing
Isabelle's powerful automated proof facilities~\cite{Blanchette2011}. In this article, we use Isabelle/UTP to both
define and verify our UTP theory of reactive contracts, and to produce an associated verification technique.

\subsection{Designs}
\label{sec:designs}

The UTP theory of designs~\cite{Hoare&98,Cavalcanti04} has two observational variables, $ok, ok' : \Bool$, flags that
denote whether a program was started and whether it terminated, respectively. The design, $\design{P_1}{P_2}$, states
that if a program is started and the state satisfies precondition $P_1$, then it will terminate and satisfy
postcondition $P_2$. This is encoded in the following predicative definition.
\begin{definition} \label{def:design} $\design{P_1}{P_2}   ~~\defs~~ (ok \land P_1) \implies (ok' \land P_2)$ \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/designs/utp_des_core.thy\#L111}
\end{definition}
\noindent Here, $P_1$ and $P_2$ are relations on variables excluding $ok$ and $ok'$. Effectively, this encoding allows a
pair of predicates to be encoded as a single predicate. An simple example is the design
$D \defs \design{\true}{x' = 1}$, where $x : \nat$ is a program variable. If $D$ is given permission to execute
($ok = true$), then the program terminates ($ok' = true$) with $x = 1$. If the program is not given permission to
execute ($ok = false$), then $x$ can taken any value.

Designs have a natural notion of refinement which requires that the precondition is weakened, and the postcondition
strengthened within the window of the precondition, as shown by the theorem below.

\begin{theorem} $\design{P_1}{P_2} \refinedby \design{Q_1}{Q_2} ~ \iff ~ (P_1 \implies Q_1) \land (Q_2 \land P_1 \implies P_2)$ \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/designs/utp_des_core.thy\#L584}
\end{theorem}

Design relations are closed under sequential composition, disjunction, and conjunction~\cite{Hoare&98,Cavalcanti04}, all
of which retain the denotations given in Definition~\ref{def:utp-prog} with the alphabet containing $ok$ and $ok'$. The
main design healthiness conditions are \healthy{H} and \healthy{N}, which are given below~\cite{Hoare&98,Cavalcanti04}.
\begin{definition}[Design Healthiness Conditions] $ $ \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/designs/utp_des_healths.thy}

  \begin{center}
  \begin{tabular}{ccc}
  {$\begin{aligned}
    \healthy{H1}(P) ~~\defs~~& (ok \implies P) \\
    \healthy{H2}(P) ~~\defs~~& P \relsemi \ckey{J} \\
    \healthy{H3}(P) ~~\defs~~& P \relsemi \IID \\
  \end{aligned}$} & ~~ &
  {$\begin{aligned}
    \ckey{J}        ~~\defs~~& (ok \implies ok') \land v' = v \\
    \IID            ~~\defs~~& \design{\true}{\II} \\
    \healthy{H}     ~~\defs~~& \healthy{H1} \circ \healthy{H2} \\
    \healthy{N}     ~~\defs~~& \healthy{H1} \circ \healthy{H3}
  \end{aligned}$}
  \end{tabular}
\end{center}
\end{definition}
$\healthy{H1}$ states that until a design has been given permission to execute, as recorded via $ok$, no observations
are possible. $\healthy{H2}$ states that no design can require non-termination. A more intuitive characterisation of the
$\healthy{H2}$ fixed-points is $P[false/ok'] \implies P[true/ok']$: every non-terminating behaviour of $P$ for which
$ok' = false$ has an equivalent terminating behaviour for which $ok' = true$. The composition, $\healthy{H}$, precisely
characterises the set of design relations constructed using $\design{P_1}{P_2}$~\cite{Cavalcanti04}.

$\healthy{H3}$ designs additionally require that $P$ is a condition: it does not refer to dashed variables. This
subclass of designs is useful for ``normal'' specifications, where the precondition does not refer to the final
state. $\ckey{H3}$ designs, with a few notable exceptions, are the most common form of design, and are thus sometimes
known as \emph{normal designs}~\cite{Guttman2010}, as indicated by healthiness condition $\healthy{N}$. Since every
$\healthy{H3}$ predicate is also $\healthy{H2}$ healthy, in defining $\healthy{N}$, we do not need to include
$\healthy{H2}$ in the composition.

$\healthy{H}$ and $\healthy{N}$ are both idempotent and continuous, and thus the theories they define are both complete
lattices. The bottom element $\botD$ is abortive, arising, for instance due to a violated precondition, and the top
$\topD$ is miraculous. The infimum $P \sqcap Q$ is a non-deterministic choice between two designs, and refinement
reduces non-determinism: $P \sqcap Q \refinedby P$.

\subsection{Reactive Processes}

The theory of reactive processes~\cite{Hoare&98,Cavalcanti&06} unifies the semantics of different reactive
languages. The two main goals of reactive processes are to (1) embed traces into the relational calculus, which is
achieved through healthiness conditions \healthy{R1} and \healthy{R2}, and (2) introduce intermediate observations,
which is achieved through healthiness condition \healthy{R3}. In addition to $ok$ and $ok'$, the theory has three pairs
of observational variables:
\begin{enumerate}
  \item $wait, wait' : \Bool$ that determine whether a process (or its predecessor) is waiting for interaction with its
    environment, that is, it is quiescent, or else has correctly terminated;
  \item $tr, tr' : \seq\,\textit{Event}$ that describes the trace before and after the process' execution; and
  \item $\refu, \refu' : \power \textit{Event}$ that describe the events being refused during a quiescent state, as
    required by the failures-divergences model of CSP~\cite{Hoare85,Roscoe2005}. If all events are being refused, the
    process is in a deadlock situation.
  \end{enumerate}
Since reactive programs often run indefinitely, the theory of reactive processes distinguishes good and bad
non-termination, the being characterised by divergence. This is achieved by reinterpreting $ok$ to indicate
divergence. Specifically, if $ok'$ is false then a reactive process has diverged, meaning it is exhibiting
unpredictable or erroneous behaviour. If $ok'$ is true, and $wait'$ is false, the process has not terminated, but
neither has it diverged.

The theory of reactive processes is used to provide a UTP denotational semantics for both
CSP~\cite{Hoare87,Cavalcanti&06}, based on relational encoding of the failures-divergences model~\cite{Roscoe2005}, and
also the stateful process language \Circus~\cite{Woodcock2001-Circus,Oliveira2005-PHD,Oliveira&09}. \Circus provides all
the usual operators of CSP for expressing networks of communicating processes, together with state-based constructs such
as variable assignment. \Circus processes encapsulate a number of state variables, operations that act on those
variables, and actions that encode the reactive behaviour of the process using channels.

In previous work~\cite{Foster17a}, we have generalised the standard UTP theory of reactive
processes~\cite{Hoare&98}. Our generalised theory~\cite{Foster17a} removes the $\refu$ and $\refu'$ variables, which
allows us to characterise behavioural semantic models other than failures-divergences. Moreover, we add
$\state, \state' : \Sigma$ to explicitly model state as suggested by \cite{BGW09}, where $\Sigma$ is a state space
type. In our previous work~\cite{Foster17a}, we have shown how the UTP theory of reactive processes can be generalised
by characterising the trace model with an abstract algebra, called a ``trace algebra''.  We characterise traces with an
abstract set $\tset$ equipped with two operators: trace concatenation $\tcat : \tset \to \tset \to \tset$, and the empty
trace $\tempty : \tset$, which obey the following axioms~\cite{Foster17a}.
\begin{definition}\label{def:tralg} A trace algebra $(\tset, \tcat, \tempty)$ is a cancellative monoid satisfying the
  following axioms: \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/reactive/Trace_Algebra.thy}
\begin{align*}
  x \tcat (y \tcat z) &= (x \tcat y) \tcat z \tag{TA1} \label{law:tassoc} \\
  \tempty \tcat x = x \tcat \tempty &= x \tag{TA2} \label{law:tunit} \\
  x \tcat y = x \tcat z ~~\implies~~  y &= z \tag{TA3} \label{law:tcancl1} \\
  x \tcat z = y \tcat z ~~\implies~~  x &= y \tag{TA4} \label{law:tcancl2} \\
  x \tcat y = \tempty  ~~\implies~~  x &= \tempty \tag{TA5} \label{law:tnai}
\end{align*}
\end{definition}
\noindent An example model is formed by finite sequences, $\langle a, b, \cdots, c \rangle$, that is
$(\seq A, \cat, \langle\rangle)$ forms a trace algebra, where $\cat$ is sequence concatenation. Using the two trace
algebra operators, we can also define a trace prefix operator ($x \le y$), and trace difference ($x - y$), which removes
a prefix $y$ from $x$. From these algebraic foundations, we have reconstructed the complete theory of reactive
processes, including its healthiness conditions and associated laws, in particular those for sequential and parallel
composition~\cite{Foster17a}. We thus generalise the type of $tr$ and $tr'$ to be an instance of a trace algebra
$\tset$, and recreate the three reactive healthiness conditions~\cite{Hoare&98,Cavalcanti&06}.
\begin{definition}[Stateful Reactive Healthiness Conditions] \label{def:reahealths} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/reactive/utp_rea_healths.thy}
\begin{align*}
  \healthy{R1}(P)   & ~~\defs~~ P \land tr \le tr' \\
  \healthy{R2}_c(P)   & ~~\defs~~ \conditional{P[\tempty, \trace /tr, tr']}{tr \le tr'}{P} \\
  \healthy{R3}_h(P) & ~~\defs~~ \conditional{\IIsrd}{wait}{P} \\
  \IIsrd            & ~~\defs~~ \conditional{(\conditional{(\exists st @ \II)}{wait}{\II})}{ok}{\ckey{R1}(\true)} \\
  \trace            & ~~\defs~~ (tr' - tr) \\
  \healthy{R}_s     & ~~\defs~~  \healthy{R1} \circ \healthy{R2}_c \circ \healthy{R3}_h
\end{align*}
\end{definition}
$\healthy{R1}$ states that $tr$ is monotonically increasing; processes are not permitted to undo past
events. $\healthy{R2}_c$ is a version of \healthy{R2}~\cite{Hoare&98}, created to overcome an issue with definedness of
sequence difference~\cite{Foster17a}, but semantically equivalent in the context of \healthy{R1}. It states that a
process must be history independent: the only part of the trace it may constrain is $tr' \tminus tr$, that is, the
portion since the previous observation $tr$. Specifically, if the history is deleted, by substituting $\tempty$ for
$tr$, and $tr' - tr$ for $tr'$, then the behaviour of the process is unchanged. Our formulation of $\healthy{R2}_c$
deletes the history only when $tr \le tr'$, which ensures that $\healthy{R2}_c$ does not depend on $\healthy{R1}$, and
thus commutes with it. Intuitively, an $\healthy{R1}$-$\healthy{R2}_c$ healthy predicate syntactically does not
constrain the trace history ($tr$), but only the trace contribution expression ($\trace$), as the following theorem
illustrates.
\begin{theorem}[$\healthy{R1}$-$\healthy{R2}_c$ trace contribution] \label{thm:trcontr} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/reactive/utp_rea_healths.thy\#L476}
$$\healthy{R1}(\healthy{R2}_c(P)) = (\exists t @ P[\tempty,t/tr,tr'] \land tr' = tr \tcat t)$$
\end{theorem}
Finally, we have $\healthy{R3}_h$, a version of \healthy{R3} from~\cite{BGW09} that introduces the concept of
intermediate observations, whilst ensuring that state variables are not included. $\healthy{R3}_h$ states that if a
process observes $wait$ to be true, then its predecessor has not yet terminated and thus it should behave like the
reactive identity, $\IIsrd$. For example, in a composition $P \relsemi Q$, if $P$ has not terminated then $Q$, if
$\healthy{R3}_h$ healthy, will behave as $\IIsrd$.

The reactive identity maintains the present value of all variables, other than the state $st$, when the predecessor is
in an intermediate state, or behaves like $\healthy{R1}(\true)$ if $ok$ is false. The latter scenario means that the
predecessor has diverged and thus we can guarantee nothing other than that the trace increases. Intuitively, an
$\healthy{R3}_h$ process conceals the state of any predecessor in an intermediate state. This allows that several
independent state valuations are concurrently possible, yet concealed from one another, until an observation is made
through an event interaction.

For comparison, we recall the definition of healthiness condition $\healthy{R3}$, which was previously used in the
theories for both CSP~\cite{Hoare&98,Cavalcanti&06} and \Circus~\cite{Oliveira&09}.
\begin{definition}[$\healthy{R3}$ Healthiness Condition] \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/reactive/utp_rea_healths.thy\#L658}
$$\healthy{R3}(P) ~\defs~ \conditional{\IIrea}{wait}{P} \qquad \qquad
  \IIrea ~\defs~ \conditional{\II}{ok}{\ckey{R1}(\true)}$$
\end{definition}
The only difference from $\healthy{R3}_h$ is that the identity $\IIrea$ is used in intermediate states. This operator
does not give special treatment to state variables: they are simply identified in intermediate states like other
observational variables. As discussed in detail in Section~\ref{sec:grd}, $\healthy{R3}_h$ allows a simpler treatment of
state variables, supports additional algebraic laws for assignment and state substitution, and solves the problem with
external choice for which it was originally designed~\cite{BGW09}, though at the cost of losing McEwan's interruption
operator~\cite{McEwan06}. Thus, the use of $\healthy{R3}_h$ instead of $\healthy{R3}$ is a design decision based on the
particular modelling facilities of interest.

We compose the three constituents to yield $\healthy{R}_s$, the overall healthiness condition of (stateful) reactive
processes, which is idempotent and continuous.
\begin{theorem}[Reactive Process Theory Properties] \label{thm:reaprop} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/theories/rea_designs/utp_rdes_healths.thy\#L226}
  \begin{itemize}
    \item $\healthy{R}_s$ is idempotent: $\Rs(\Rs(P)) = \Rs(P)$;
    \item $\healthy{R}_s$ is continuous: $\Rs(\bigsqcap A) = \bigsqcap P \in A @ \Rs(P)$.
    \end{itemize}
  \end{theorem}
\noindent As for designs, a corollary of this theorem is that we obtain a complete lattice and the continuous theory
properties of Theorem~\ref{thm:contthm}. Thus we now have a UTP theory of stateful reactive processes to use as the
foundation for reactive design contracts.

\subsection{UTP Theory Preliminaries}

The theorems presented in Section~\ref{sec:contracts}, present reactive contracts using the syntactic form of
$\rc{P_1}{P_2}{P_3}$. It is often inconvenient to rely on such a specific syntactic form to reason about contracts, for
example when stating algebraic theorems. It is much more convenient to a reactive contract $P$ as a relation that admits
certain properties. Consequently, as usual in the UTP approach, we define healthiness conditions that characterise
well-formed contract predicates. This allows us to obtain a large number of algebraic laws from lattice theory and
related domains, and also allows us to reason about contracts without the need for the syntactic form.

In order to reason about contracts as opaque relations, we need a way of extracting the three parts from a contract. We
therefore define the following three functions:

\begin{definition}[Pre-, Peri-, and Postcondition Extraction Functions] \label{def:preperipost} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L131}
  \begin{align*}
    \preR{P} &~~\defs~~ \negr P[true,false,false/ok,ok',wait] \\
    \periR{P} &~~\defs~~ P[true,true,false,true/ok,ok',wait,wait'] \\
    \postR{P} &~~\defs~~ P[true,true,false,false/ok,ok',wait,wait']
  \end{align*}
\end{definition}

\noindent These three functions variously substitute the observational variables to obtain the respective characteristic
predicates. In order to illustrate this, we first expand out the definition of reactive contract from
Definition~\ref{def:rcontract}, and also using Definitions~\ref{def:design} and \ref{def:reahealths}:
$$\rc{P_1}{P_2}{P_3} = \healthy{R1}(\healthy{R2}_c(\conditional{\IIsrd}{wait}{((ok \land P_1) \implies (ok' \land (\conditional{P_2}{wait'}{P_3})))}))$$
\noindent From this, we can see that the crucial variables that dictate the various behaviours are $wait$, $ok$, $ok'$,
and $wait'$. Variable $wait$ flags whether a sequential predecessor is in an intermediate state or has terminated, $ok$
flags whether a predecessor diverged, and $ok'$ and $wait'$ record this information for the present relation.

The precondition ($P_1$) is $\false$ when a reactive design was started ($ok \land \neg wait$) but it
diverged ($\neg ok'$). Thus, to extract the precondition we set $ok$, $ok'$, and $wait$ to $true$, $false$, and $false$,
respectively, and negate the result using reactive negation. The pericondition is reached when the reactive design was
started and did not diverge ($ok'$), but has not yet reached its final state ($\neg wait'$), and is thus
intermediate. The postcondition is similarly obtained, but $wait'$ becomes $false$. With these definitions we can prove
theorems that allow us to extract the constituent reactive relations from a syntactic reactive contract.

\begin{theorem}[Extracting Pre, Peri, and Postconditions] \label{thm:exttrip} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L387}
  \begin{align*}
    \preR{\rc{P_1}{P_2}{P_3}} &~~=~~ P_1  \\
    \periR{\rc{P_1}{P_2}{P_3}} &~~=~~ P_1 \rimplies P_2 \\
    \postR{\rc{P_1}{P_2}{P_3}} &~~=~~ P_1 \rimplies P_3
  \end{align*}
  Provided $P_1$, $Q_1$, and $Q_2$ are all $\healthy{RR}$ healthy.
\end{theorem}

\noindent The pericondition and postcondition are viewed through the prism of the precondition being satisfied, which is
why the implications are present in the result above. This is an important assumption of reactive designs. Although it
is possible to specify behaviours in the peri and postcondition outside the precondition, once the contract is
constructed these behaviours are pruned, so that the behaviour of a contract when its precondition is violated is always
$\Chaos$.

\subsection{Stateful Reactive Designs}
\label{sec:srd}

In this section, we introduce the first of our two reactive design theories: stateful reactive designs. Motivated by the
previous work on CSP and \Circus in UTP~\cite{Hoare&98,Cavalcanti&06,Oliveira&09}, we define the following healthiness
conditions for our generalised theory of reactive designs. We generalise the previous
works~\cite{Hoare&98,Cavalcanti&06,Oliveira&09} due to the underlying abstract trace algebra, and the extensible
alphabet of our theory~\cite{Foster17a}.

\begin{definition}[Stateful Reactive Designs Healthiness Conditions] \label{def:rdhcond} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_healths.thy\#L401}
\begin{align*}
  \healthy{RD1}(P) &~~\defs~~ ok \rimplies P \\
  \healthy{RD2}(P) &~~\defs~~ P \relsemi \ckey{J} \\
  \healthy{SRD}(P) &~~\defs~~ \healthy{RD1} \circ \healthy{RD2} \circ \healthy{R}_s
\end{align*}
\end{definition}

\noindent $\healthy{RD1}$ and $\healthy{RD2}$ are analogous to $\healthy{H1}$ and $\healthy{H2}$ from the theory of
designs. Moreover, $\healthy{RD1}$ and $\healthy{RD2}$ correspond to $\healthy{CSP1}$ and $\healthy{CSP2}$ from the
theories of CSP~\cite{Hoare&98,Cavalcanti&06} and \Circus~\cite{Oliveira&09}. We rename them, firstly because our theory
has a different alphabet founded upon our trace algebra, and secondly because we do not specify the corresponding
$\healthy{CSP3}$ and $\healthy{CSP4}$, which constrain $ref$ and are thus specific to CSP and \Circus.

$\healthy{RD1}$ states, like $\healthy{H1}$, that observations are possible only after initiation, indicated by
$ok$. However, unlike $\healthy{H1}$, if $ok$ is false the resulting predicate is not $\true$, but $\truer$; that is, the
trace must monotonically increase, but the behaviour is otherwise unpredictable. $\healthy{RD2}$ is identical to
$\healthy{H2}$ and thus also $\healthy{CSP2}$.

Our overall healthiness condition for stateful reactive designs is then called $\healthy{SRD}$, which includes
$\healthy{RD1}$, $\healthy{RD2}$, and $\Rs$. Like $\healthy{RD1}$ and $\healthy{RD2}$, it is a generalisation of the
overall \Circus healthiness condition $\healthy{CSP}$~\cite{Oliveira&09}. We can next prove that $\healthy{SRD}$
relations admit a certain syntactic formulation using reactive contracts, as shown in the following theorem.

\begin{theorem}[Stateful Reactive Design Formulation] \label{thm:rdesform} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_healths.thy\#L401}
  \begin{align*}
    \healthy{SRD}(P) &= \rc{\preR{P}}{\periR{P}}{\postR{P}}
  \end{align*}
\end{theorem}

\noindent If a relation is $\healthy{SRD}$ healthy, then it takes the form of a reactive contract with a pre-, peri-,
and postcondition. Theorem~\ref{thm:rdesform} thus allows us to take an $\healthy{SRD}$ predicate and deconstruct it
into its three parts, using the functions defined in Definition~\ref{def:preperipost}, which can then be manipulated
separately. This theorem shows an equivalence between the syntactic formulation, and elements of
$\theoryset{\healthy{SRD}}$: any element of the latter can be constructed using the contract triple
notation. Conversely, a well-formed reactive design triple always yields a healthy reactive design. This is confirmed by
the following closure theorem, which is a corollary of Theorems~\ref{thm:rdesform} and \ref{thm:exttrip}.

\begin{corollary} If $P_1$, $P_2$, and $P_3$ are all $\healthy{RR}$ healthy then $\rc{P_1}{P_2}{P_3}$ is $\healthy{SRD}$
  healthy. \label{thm:rcclosure} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L568}
\end{corollary}

\noindent In order to show that a reactive contract is $\healthy{SRD}$, it suffices to show that its pre-, peri-, and
postcondition are all $\healthy{RR}$. A further corollary is the three triple extraction functions all produce healthy
reactive relations when applied to an $\healthy{SRD}$ relation.

\begin{corollary} If $P \is \healthy{SRD}$ then $\preR{P}$, $\periR{P}$, and $\postR{P}$ are all $\healthy{RR}$-healthy. \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L346}
\end{corollary}

Having defined a candidate theory for our reactive contracts, we will now explore its algebraic properties. The class of
$\healthy{SRD}$ relations admits a number of useful identities that we outline below.

\begin{theorem}[$\healthy{SRD}$ Laws] If $P$ is $\healthy{SRD}$ healthy then \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L1067}
  \begin{align}
    \IIsrd \relsemi P ~~=~~& P \\
    \Chaos \relsemi P ~~=~~& \Chaos \\
    \Miracle \relsemi P ~~=~~& \Miracle
  \end{align}
\end{theorem}

\noindent $\IIsrd$ is a left unit of any $\healthy{SRD}$ relation, and $\Chaos$ and $\Miracle$ are both left
annihilators. However, in general $\IIsrd$ is not a right unit, which the following theorem illustrates.

\begin{theorem} \label{thm:srdskip} If $P_1$, $P_2$, and $P_3$ are $\healthy{RR}$ then
  $\rc{\!P_1\!}{\!P_2\!}{\!P_3\!} \relsemi \IIsrd = \rc{\negr (\negr P_1) \relsemi \truer}{\exists \state' @ P_2}{P_3}$ \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_triples.thy\#L1079}
\end{theorem}

\noindent Right composition with $\IIsrd$ effectively imposes two additional requirements on the reactive contract: (1)
that the negated precondition does not refer to dashed variables other than $tr'$, which must be extension closed --- it
is $\healthy{RC1}$ (cf. Definition~\ref{def:RC}); and (2) that the pericondition does not refer to $\state'$, as
characterised by the existential quantifier. The latter follows as a direct consequence of $\healthy{R3}_h$~\cite{BGW09}
(cf. Definition~\ref{def:reahealths}), which requires that $\state$ must not be restricted in an intermediate
state. Thus, composition of $P$ with $\IIsrd$ has the same effect on $\state'$ in $P$ since $\IIsrd$ ignores any
intermediate states ($wait' = true$), rather than passing them forward to a successor process.

The former restriction is a direct consequence of healthiness condition $\healthy{RD1}$. To explain why, we consider the
reactive design $P \relsemi \IIsrd$ in the situation when $P$ has started ($ok \land wait$), but diverged ($\neg
ok'$). The following calculation shows the result.

\begin{example}[Divergence and $\healthy{RD1}$]
\begin{align*}
  &\quad~ (P \land ok \land \neg ok' \land \neg wait) \relsemi \IIsrd \\[.3ex]
  &= P[true, false, false/ok, ok', wait'] \relsemi \IIsrd[false/ok] & \text{[relational calculus]}  \\[.3ex]
  &= (\negr \preR{P}) \relsemi \IIsrd[false/ok] & \text{[Definition~\ref{def:preperipost}]} & \text{} \\[.3ex]
  &= (\negr \preR{P}) \relsemi (\healthy{RD1}(\IIsrd))[false/ok] & \text{[Theorem~\ref{thm:rcclosure}]} \\[.3ex]
  &= (\negr \preR{P}) \relsemi (ok \rimplies \IIsrd)[false/ok] & \text{[Definition~\ref{def:rdhcond}]} \\[.3ex]
  &= (\negr \preR{P}) \relsemi \truer & \text{[predicate calculus]}
\end{align*}
\end{example}

\noindent When $P$ diverges with $\neg ok'$, its behaviour is $\negr \preR{P}$: the precondition has been
violated. Moreover, if $ok'$ is false in $P$ then $ok$ is false in $\IIsrd$, which yields the relation
$\truer$. Actually, this follows for any $\healthy{RD1}$ relation, not just $\IIsrd$, since
$\healthy{RD1}[false/ok] = \truer$. Consequently, right composition with any $\healthy{SRD}$ relation yields the same
result: the precondition should be $\healthy{RC1}$.

Consequently, the right composition law motivates that we need to consider a refined theory for reactive contracts, in
order to support the desirable algebraic and calculational laws of Section~\ref{sec:contracts}.  This is the objective
of the following section.

\subsection{Normal Stateful Reactive Designs}
\label{sec:nsrd}

We refine $\healthy{SRD}$ by identifying the subclass of normal stateful reactive designs, $\healthy{NSRD}$, which
provides the theory domain of our reactive contracts.

\begin{definition}[Normal Stateful Reactive Designs Healthiness Conditions] \label{def:nsrddef} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L11}
\begin{align*}
  \healthy{RD3}(P) &~~\defs~~ P \relsemi \IIsrd \\
  \healthy{NSRD}(P) &~~\defs~~ \healthy{RD1} \circ \healthy{RD3} \circ \healthy{R}_s
\end{align*}
\end{definition}

\noindent $\healthy{RD3}$ is analogous to $\healthy{H3}$: it requires that skip is a right unit. This ensures that the
precondition is a reactive condition and the pericondition does not depend on $\state'$. The use of the word ``normal''
here is therefore by analogy with normal designs~\cite{Guttman2010}. $\healthy{NSRD}$ does not explicitly invoke
$\healthy{RD2}$ as it is subsumed by $\healthy{RD3}$, as the following theorem demonstrates.

\begin{theorem}[$\healthy{RD3}$ subsumes $\healthy{RD2}$] \label{thm:rd3subsumes} $\healthy{RD2}(\healthy{RD3}(P)) = \healthy{RD3}(\healthy{RD2}(P)) = \healthy{RD3}(P)$ \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L31}
\end{theorem}

\begin{proof}
  This follows since $\ckey{J} \relsemi \IIsrd = \IIsrd \relsemi \ckey{J} = \IIsrd$.
\end{proof}

\noindent Consequently, it is easy to show that every $\healthy{NSRD}$-healthy relation is also $\healthy{SRD}$-healthy,
and therefore the theorems of Section~\ref{sec:srd} remain valid. We can also prove the following theorem that follows
as a consequence of Theorems~\ref{thm:rd3subsumes} and \ref{thm:srdskip}.

\begin{theorem}[Normal Stateful Reactive Design Formulation] \label{thm:nrdesform} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L153}
  \begin{align*}
    \healthy{NSRD}(P) &= \rc{\healthy{RC1}(\preR{P})}{(\exists \state' @ \periR{P})}{\postR{P}}
  \end{align*}
\end{theorem}

In addition to ensuring that the elements of the triple of $\healthy{RR}$ healthy, $\healthy{NSRD}$ also ensures that
the precondition is a reactive condition, and that the pericondition does not refer to $\state'$.

\begin{corollary} \label{thm:nsrdintro} $P$ is $\healthy{NSRD}$ healthy provided that the following
  conditions hold: \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L304}
  \begin{enumerate}
    \item $P$ is $\healthy{SRD}$ healthy;
    \item $\preR{P}$ is $\healthy{RC}$ healthy;
    \item $\periR{P}$ does not mention $\state'$.
  \end{enumerate}
\end{corollary}

\noindent A further corollary finally justifies the syntactic formulation given in Section~\ref{sec:contracts}:

\begin{corollary}[$\healthy{NSRD}$ contract closure] $ $ \label{thm:nrcclosure} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L310}

\noindent If $P_1$ is $\healthy{RC}$, $P_2$ and $P_3$ are both $\healthy{RR}$, and $P_2$ does not refer to $\state'$, then $\rc{P_1}{P_2}{P_3}$ is $\healthy{NSRD}$ healthy.
\end{corollary}

\noindent We now, therefore, have an adequate formulation of the reactive design theory. In spite of its restrictions,
$\healthy{SRD}$ remains useful as a means of obtaining algebraic theorems. In the remainder of this section we will
therefore explore the algebraic properties of the two theories.

\subsection{Algebraic Properties}
\label{sec:grd-alg}

$\healthy{SRD}$ and $\healthy{NSRD}$ are both idempotent and continuous, and therefore both form complete lattices, as
stated in the following theorem.

\begin{theorem}[Reactive Design Lattices] $\healthy{SRD}$ and $\healthy{NSRD}$ healthy predicates form complete lattices
  with $\top_\srdes \defs \healthy{SRD}(\false) = \Miracle$ and $\bot_\srdes \defs \healthy{SRD}(\true) =
  \Chaos$. \label{thm:rdes-lattice} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L732}
\end{theorem}
\begin{proof} Standard proofs of idempotency for $\healthy{CSP1}$ and $\healthy{CSP2}$~\cite{Hoare&98,Cavalcanti&06}
  apply also to $\healthy{RD1}$ and $\healthy{RD2}$, respectively. $\healthy{RD3}$ is idempotent since
  $\IIsrd \relsemi \IIsrd = \IIsrd$. $\healthy{RD1}$ is continuous since it is disjunctive. $\healthy{RD2}$ and
  $\healthy{RD3}$ are both continuous since sequential composition distributes through infima to the left and right.
\end{proof}

\noindent We note that both $\Miracle$ and $\Chaos$, following the form given in Theorem~\ref{thm:nrcclosure}, are both
$\healthy{NSRD}$ healthy. Through the Knaster-Tarski theorem~\cite{Tarski55}, we also obtain weakest fixed-point
operators $\thlfp{R}$ and $\thlfp{N}$ for the two theories, which we will further explore in
Section~\ref{sec:recurse}. Since $\healthy{SRD}$ and $\healthy{NSRD}$ are also continuous, by Theorem~\ref{thm:contthm}
we can rewrite the weakest fixed-points to $\mu X @ F(\healthy{SRD}(X))$ and $\mu X @ F(\healthy{NSRD}(X))$,
respectively. Thus, we can reason about recursive reactive designs using the relational calculus lattice rather than the
theory specific ones. We can also show that reactive designs are closed under the standard relational calculus
operators, as the following theorems demonstrate.

\begin{theorem}[Reactive Design Composition] \label{sec:rdes-seq} If $P$ and $Q$ are $\healthy{NSRD}$ healthy then \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L346}
  \begin{align*}
  P \relsemi Q = \Rs
    \left(\begin{array}{l}
            \preR{P} \land (\postR{P} \wpR \preR{Q}) \\[.5ex]
            \shows~~ \periR{P} \lor (\postR{P} \relsemi \periR{Q}) \\[.5ex]
            \wcond~~ \postR{P} \relsemi \postR{Q}
          \end{array}\right)
  \end{align*}
\end{theorem}

\noindent Theorem~\ref{sec:rdes-seq} is essentially the same as Theorem~\ref{thm:rdes-seq}, but relies on healthiness of
$P$ and $Q$, rather than their syntactic form. As similar law holds for $\healthy{SRD}$-healthy predicates, though with
a more complex precondition and pericondition, following the form given in Theorem~\ref{thm:srdskip}. We finally show
closure of the theory under the main programming operators.

\begin{theorem}[Reactive Designs Closure]
  $\healthy{SRD}$ and $\healthy{NSRD}$ healthy predicates are closed under $\intchoice$, $\sqcup$, $\conditional{}{b}{}$,
  ~$\relsemi$~, $\IIsrd$, $\assignsR{\sigma}$, $\Miracle$, and $\Chaos$. \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_normal.thy\#L386}
\end{theorem}

\noindent This closure theorem means that we can import the algebraic laws for the relational calculus operators from
core UTP~\cite{Hoare&98}, such as several equations of Theorem~\ref{thm:rellaws}. Finally, we note that our theory
admits the following familiar laws from relational calculus for assignment.

\begin{theorem}[Reactive Design Assignment Compositions] \label{thm:rdes-asn-comp} If $P$ is $\healthy{NSRD}$ healthy,
  $x$ is a state variable, and $v$ is an expression containing only state variables, then: \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_prog.thy\#L990}
  \begin{align}
    (\assignR{x}{v})    ~ \relsemi ~ P ~~=~~& P[v/x] \label{thm:rdes-asn-comp-1} \\[.5ex]
    \assignsR{\sigma} ~ \relsemi ~ P ~~=~~& \substapp{\sigma}{P} \label{thm:rdes-asn-comp-2}
  \end{align}
\end{theorem}

\noindent Theorem~\ref{thm:rdes-asn-comp-1}, the more usual law~\cite{Hoare87}, shows that a sequential assignment can
be turned into a substitution applied to its successor. It is an instance of the more general
Theorem~\ref{thm:rdes-asn-comp-2} when $\sigma = \{x \mapsto v\}$, crucially, provided that $x$ is a state variable and
not an arbitrary UTP variable.

Theorem~\ref{thm:rdes-asn-comp} depends directly on the use of $\healthy{R3}_h$, and the resulting requirement that
periconditions do not refer to after state. It would not hold if allowed such references, for example by substituting
$\healthy{R3}_h$ with the original healthiness condition $\healthy{R3}$~\cite{Hoare&98}. In order to understand why,
consider the following corollary of Theorem~\ref{thm:rdes-asn-comp-1} involving a \Circus event prefix:

\begin{theorem}[Assignment and Events] \label{thm:asnevent}
   $$(\assignR{x}{e} \relsemi c \then P) ~~=~~ (c[e/x] \then (\assignR{x}{e} \relsemi P))$$
\end{theorem}

\noindent Theorem~\ref{thm:asnevent} allows us to push assignment through event prefixes, whilst making an appropriate
substitution.  It can be found in reactive languages like Occam~\cite{Roscoe1988}. This law does not hold in previous
\Circus semantics~\cite{Oliveira&09} as $\state'$ (there called $v'$) is revealed in intermediate states. Thus, whilst
the left hand side of this equation admits an intermediate observation where $x$ is updated to $e$, because the
pericondition does characterise state updates, the right hand side does not.

There are, however, costs to this simplification. A side effect is to prevent encoding of McEwan's \Circus interruption
operator~\cite{McEwan06}, which has the form $P \mathop{\triangle_i} Q$. This operator is similar to
$P \interleave (i \then Q)$, except that if the interruption event $i$ occurs before $P$ terminates, and whilst it is
quiescent, then the remaining behaviour of $P$ is pruned. If $P$ terminates, then conversely the behaviours of $Q$ are
lost. Crucially, the internal state of $P$ is retained following interruption~\cite{BGW09}, and is passed on to $Q$,
which is unique to McEwan's work (cf.~\cite{Sherif2010,Wei2013,Woodcock14}). For example, consider the following action:
$$(x := 5 \relsemi a \then \Skip) \mathop{\triangle_b}\, (x := x + x).$$
First, we note that the leading assignment $x := 5$ cannot be interrupted, since it does not have a quiescent
state. However, once this has occurred the left-hand side enters a quiescent state where $a$ is enabled. Through the
interruption operator, $b$ is also enabled at this point. If $a$ occurs then the entire action terminates in a final
state with $x = 5$. However, if $b$ occurs then the value of $x$ at this point is retained, and the action $x := x + x$
occurs, leading to final value of $10$ for $x$.

We see, therefore, how the value of $x$ is retained and used by the interruption action. Such a retention of the state,
however, cannot be represented in the presence of $\healthy{RD3}$ as no intermediate state variables are
recorded. Therefore, if such an interruption operator is required, the loss of Theorem~\ref{thm:asnevent} must be
accepted, and $\healthy{R3}$ used as the base of reactive designs instead. This is a design choice depending on the kind
of reasoning and expressivity needed, as $\healthy{R3}$ reactive designs carry more information and so are more
distinguishing than $\healthy{R3}_h$ reactive designs. $\healthy{R3}$ is supported in Isabelle/UTP if its use is
desired.

\subsection{Recursion}
\label{sec:recurse}
\input{sec/recurse.tex}

\subsection{Parallel Composition}
\label{sec:parallel}

In this section we introduce the parametric parallel composition operator for reactive designs, and substantiate a
number of preliminary results for the operator, including well-formedness conditions supported by a novel healthiness
condition. Parallel composition in UTP is expressed in terms of the parallel-by-merge scheme $P \mathop{\parallel_M} Q$,
whereby the final states of concurrent separated processes $P$ and $Q$ are merged by predicate $M$. We adopt a slightly
simplified definition of parallel-by-merge, originally presented in~\cite{Foster16a}, which assumes that the alphabet of
both $P$ and $Q$ is the same, but is otherwise semantically equivalent to the standard UTP definition~\cite[chapter
7]{Hoare&98}.

\begin{definition}[Parallel-by-Merge] \label{def:par-by-merge} \isalink{https://github.com/isabelle-utp/utp-main/blob/07cb0c256a90bc347289b5f5d202781b536fc640/utp/utp_concurrency.thy\#L275}
  $$P \parallel_M Q ~\defs~ (\psep{P}{0} \land \psep{Q}{1} \land v' = v) \relsemi M$$
\end{definition}

\noindent The intuition for parallel-by-merge is given in Figure~\ref{fig:pbm}. It splits the state space into three
parts, one of which is passed to $P$, the second to $Q$, and the third is simply copied from the original input
state. Assuming both $P$ and $Q$ produce an output, the merge predicate $M$ computes the overall output that should be
given by merging the three states. For imperative programs, a simple example merge predicate may pick two disjoint
subsets of the variables output by $P$ and $Q$ to produce an overall output. The value of such a scheme for parallel
composition is that different concurrency schemes can be supported, and properties of the parallel composition operator
often reduce to properties of the merge predicate~\cite[theorem 7.2.10, page 173]{Hoare&98}.

To formalise this in Definition~\ref{def:par-by-merge}, we require that $P$ and $Q$ are homogeneous relations with the
alphabet $\{v, v'\}$, where $v$ is a vector of variables. $\psep{P}{0}$ and $\psep{Q}{1}$ rename the dashed variables by
adding indices $0$ and $1$, respectively, so they can be distinguished by the merge predicate $M$\footnote{These are
  called ``separating simulations'' in~\cite[page 172]{Hoare&98}, and are denoted using special relations called $U0$
  and $U1$.}. $M$ is a heterogeneous alphabetised relation whose alphabet is $\{ 0.v, 1.v, v, v'\}$. It takes three
copies of the variables: the renamed dashed variables of $P$ and $Q$, and all undashed variables. The separated
processes are conjoined, which is acceptable because of their disjoint output alphabets, along with a predicate that
copies all initial variables ($v' = v$). The resulting conjunctive relation is then composed in sequence with $M$. This
merge predicate calculates the overall final state in terms of the initial state, and final states of $P$ and $Q$. Thus,
the overall composition $P \parallel_M Q$ has alphabet $\{v, v'\}$.

For our theory of reactive designs, the objective, as indicated by Section~\ref{sec:parcontract} is to specialise
parallel-by-merge so that it acts only on the trace, state, and other semantic observational variables (like
$\refu$). We therefore define the parametric merge predicate $\mathcal{M}_R(M)$ that merges $ok$ and $wait$ variables,
so handling divergence and intermediate observations. It defers merging of the states and traces to an ``inner merge
predicate'' $M$, such as $M_c$ described in Example~\ref{ex:interleave}. We require that $M$ does not refer to $ok$ or
$wait$ nor decorations thereof.

We define three auxiliary merge operators that construct the ``outer merge predicate'', by showing how $ok$ and $wait$
are merged, and imposition the reactive design healthiness conditions. These operators are then used to define the
reactive design parallel composition operator.

\begin{definition}[Reactive Designs Parallel Composition] \label{def:rdpar} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L107}
  \begin{align*}
    \mathcal{N}_0(M) &~\defs~ (wait' = (0.wait \lor 1.wait) \land tr \le tr' \land M) \\[1ex]
    \mathcal{N}_1(M) &~\defs~ (ok' = (0.ok \land 1.ok) \land \mathcal{N}_0(M)) \\[1ex]
    \mathcal{M}_R(M) &~\defs~ \healthy{RD3}(\healthy{RD1}(\healthy{R3}_h(\mathcal{N}_1(M)))) \\[1ex]
    P \rcpar{M} Q    &~\defs~ P \parallel_{\mathcal{M}_R(M)} Q
  \end{align*}
\end{definition}

\noindent The auxiliary merge functions $\mathcal{N}_0$ and $\mathcal{N}_1$ conjoin the inner merge predicate $M$ with
three conjuncts. $\mathcal{N}_0$ handles merging of the $wait$ variables. If either $P$ or $Q$ admits an intermediate
observation ($0.wait$ or $1.wait$), then also the composite observation is intermediate, and thus we take the
disjunction of the $wait$ variables to determine $wait'$. The third conjunct ensures the resulting merge is
$\healthy{R1}$ healthy. $\mathcal{N}_1$ handles merging of the $ok$ variables. If either $P$ or $Q$ diverges, then we
require that their composition also diverges and thus $ok'$ takes the conjunction of both $ok$ variables. Using
$\mathcal{N}_1$, we then define the overall merge predicate $\mathcal{M}_R$ by application of three healthiness
conditions to construct a stateful reactive design. The parametric merge of two reactive designs, $P \rcpar{M} Q$ with
inner merge predicate $M$, is simply a parallel-by-merge using $\mathcal{M}_R(M)$.

It remains to prove that $\healthy{NSRD}$ is closed under reactive design parallel composition. In order to prove this,
we need to restrict the form of the merge predicate using new healthiness conditions. Firstly, we need a modified
version of $\healthy{R2}_c$ that is applicable to merge predicates, first defined in~\cite{Foster17a}.

\begin{definition}[$\healthy{R2}_c$ for Merge Predicates] \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/reactive/utp_rea_parallel.thy\#L21}
  \begin{align*}
    \healthy{R2}_m(M) &\defs (P[\tempty,tr'\!-\!tr,0.tr\!-\!tr,1.tr\!-\!tr/tr,tr',0.tr,1.tr]) \infixIf tr \le tr' \infixElse P
  \end{align*}
\end{definition}

\noindent Merge predicates have three ways of accessing the trace history through the three respective copies of the
trace variable. Thus, it is necessary to delete the history in $0.tr$, $1.tr$, and $tr$ in the healthiness condition
$\healthy{R2}_m$ to ensure that this does not occur. This allows us to prove the following theorem

\begin{theorem} \label{thm:parreaclos}
  $P \parallel_M Q$ is $\healthy{R1}$ and $\healthy{R2}_c$ healthy provided that $P$ and $Q$ are both $\healthy{R1}$ and
  $\healthy{R2}_c$, and $M$ is $\healthy{R1}$ and
  $\healthy{R2}_m$. \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/reactive/utp_rea_parallel.thy\#L114}
\end{theorem}

This theorem provides the circumstances under which a parallel-by-merge constructs a healthy reactive process. From
this, we define the following healthiness condition for reactive-design inner merge predicates.

\begin{definition}[Healthy Inner Merge Predicate] \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L128}
  $$\healthy{RDM}(M) \defs \healthy{R2}_m(\exists 0.ok, 1.ok, ok, ok', 0.wait, 1.wait, wait, wait' @ M)$$
\end{definition}

\noindent $\healthy{RDM}$ contains $\healthy{R2}_m$ and additionally formalises the requirement that the inner merge
predicate does not contain $ok$, $wait$, and decorations thereof, through existential quantification. These variables
have already been handled by the outer merge predicate, and so the inner merge predicate should not refer to them. $M_c$
in Example~\ref{ex:interleave} is clearly $\healthy{RDM}$, for example, since it refers only to $0.\trace$ and
$1.\trace$, thus satisfying $\healthy{R2}_m$, and does not mention $ok$ or $wait$ in any way.

Using this definition of healthy reactive inner merges, we can then prove the following closure theorem for parallel
composition:

\begin{theorem}[Parallel Composition Closure] \label{thm:parclos} If $P$ and $Q$ are $\healthy{SRD}$ healthy, and $M$ is
  $\healthy{RDM}$ healthy, then $P \parallel_M Q$ is $\healthy{NSRD}$ healthy. \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L153}
\end{theorem}

\noindent As seen in Definition~\ref{def:rdpar}, parallel composition, like sequential composition, is not defined
explicitly as a reactive design using the contract syntax. However, in order to calculate the meaning of a parallel
reactive program it is necessary to know how to calculate a contract form for it. By Theorem~\ref{thm:parclos} we know
that parallel composition is a normal stateful reactive design ($\healthy{NSRD}$), and therefore we can invoke
Theorem~\ref{thm:nrdesform} to split it into a reactive design triple, toward substantiation of
Theorem~\ref{thm:rdespar}. It then suffices to calculate its pre-, peri-, and postcondition. In order to do this, we
need to characterise interference between parallel processes using a notion of weakest rely condition. This is the
weakest context under which two parallel composed processes do not violate one another's assumptions.

\begin{definition}[Weakest Rely Condition] \label{def:wppR} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L667}
  \begin{align*}
    P \wppR{M} Q ~~\defs~~& \negr ((\negr Q) \parallel_{\hbox{\small $M$} \relsemi \truer} P)
  \end{align*}
\end{definition}

\noindent The operator $P \wppR{M} Q$ is essentially the concurrent case of the reactive weakest precondition $\wpR$
(cf. Definition~\ref{def:wpR}). It represents the weakest context where reactive relation $P$ does not lead to the
violation of reactive condition $Q$. We achieve this by first merging the possible traces of negated $Q$ with those of
$P$ using the merge predicate $M$ composed with $\truer$. This determines all the behaviours permitted by merge
predicate $M$ that are enabled by $P$ and yet violate $Q$. The composition with $\truer$ ensures that resulting reactive
relation is extension closed. We then negate the resulting relation to obtain the overall reactive precondition.

We can show that the weakest rely condition constructor forms a reactive condition, which is essential to our using it
in the reactive contract precondition:

\begin{theorem}[Weakest Rely Condition forms a Reactive Condition] If $P$ and $Q$ are $\healthy{RR}$ healthy, and $M$ is
  $\healthy{RDM}$ healthy, then $P \wppR{M} Q$ is a reactive condition. \label{thm:wrcrc} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L711}
\end{theorem}

\begin{proof}
  By Theorem~\ref{thm:parreaclos} we can show that $P \wppR{M} Q$ is $\healthy{R1}$ and $\healthy{R2}_c$. It
  therefore suffices to show that it is also $\healthy{RC1}$ healthy, which we do below.
  \begin{align*}
    \healthy{RC1}(P \wppR{M} Q)
    =~& \healthy{RC1}(\negr ((\negr P) \parallel_{\hbox{\small M} \relsemi \truer} Q)) & \text{[$\wppR{M}$ definition]} \\
    =~& \negr ((\negr \negr ((\negr P) \parallel_{\hbox{\small M} \relsemi \truer} Q)) \relsemi \truer) & \text{[$\healthy{RC1}$ definition]} \\
    =~& \negr (((\negr P) \parallel_{\hbox{\small M} \relsemi \truer} Q) \relsemi \truer) & \text{[predicate calculus]} \\
    =~& \negr (((\negr P) \parallel_{\hbox{\small M}} Q) \relsemi \truer \relsemi \truer) & \text{[$\parallel_{\hbox{\small M}}$ definition]} \\
    =~& \negr (((\negr P) \parallel_{\hbox{\small M}} Q) \relsemi \truer) & \text{[relational calculus]} \\
    =~& \negr ((\negr P) \parallel_{\hbox{\small M} \relsemi \truer} Q) & \text{[$\parallel_{\hbox{\small M}}$ definition]} \\
    =~& P \wppR{M} Q & \text{[$\wppR{M}$ definition]}
  \end{align*}
  This essentially follows due the imposition of extension closure in the merge predicate. \qedhere
\end{proof}

\noindent We can now use the weakest rely condition to calculate the precondition for parallel composition. We enumerate
all the ways that divergence could arise from the composition, and request that this not happen using weakest rely
conditions.

\begin{theorem}[Parallel Precondition] \label{thm:parpre} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L744}
  $$\preR{P \rcpar{M} Q} =
    \left(\begin{array}{l}
      \preR{P} \wppR{M} \periR{Q} \land \preR{P} \wppR{M} \postR{Q} \land \\[.5ex]
      \preR{Q} \wppR{M} \periR{P} \land \preR{Q} \wppR{M} \postR{P}
    \end{array}\right)$$
\end{theorem}

\noindent Divergence can arise in four possible possible ways: when an intermediate or final observation of $Q$ leads to
a state where the precondition of $P$ is violated, and the converse situation for $P$ and $Q$.

The theorem for calculating the pericondition of parallel composition requires that we merge the traces, but not the
state variables as these are concealed in intermediate observations. So, we define the following derived parallel
composition operator.

\begin{definition}[Intermediate Merge] $P \rcmergee{M} Q ~~\defs~~ P \parallel_{\exists st' @ M} Q$
\end{definition}

\noindent $P \rcmergee{M} Q$ merges the traces of $P$ and $Q$, whilst hiding the merged post-state using an existential
quantifier. It is used in the following calculation of parallel pericondition.

\begin{theorem}[Parallel Pericondition and Postcondition] \label{thm:parperipost} \isalink{https://github.com/isabelle-utp/utp-main/blob/90ec1d65d63e91a69fbfeeafe69bd7d67f753a47/theories/rea_designs/utp_rdes_parallel.thy\#L437}
  \begin{align*}
    \periR{P \rcpar{M} Q} ~=~~& \preR{P \rcpar{M} Q} \rimplies
    \left(\begin{array}{l}
       \periR{P} \rcmergee{M} \periR{Q} \lor \\
       \postR{P} \rcmergee{M} \periR{Q} \lor \\
       \periR{P} \rcmergee{M} \postR{Q}
    \end{array}\right) \\[1ex]
    \postR{P \rcpar{M} Q} ~=~~& \preR{P \rcpar{M} Q} \rimplies (\postR{P} \parallel_M \postR{Q})
  \end{align*}
\end{theorem}

\noindent The merge predicate calculates the value of $wait'$ from the disjunction of $0.wait$ and $1.wait$, and so the
overall observation of a parallel composition is intermediate if either $P$ or $Q$ is. The parallel postcondition, for
the same reason, requires that both $P$ and $Q$ have reached their final states. Unlike for the pericondition, the
normal parallel by merge operator is used, since the state is no longer concealed.

We have now shown the laws for calculating the pre-, peri-, and postconditions of parallel reactive contracts. Combining
Theorems~\ref{thm:parpre} and \ref{thm:parperipost} with Theorem~\ref{thm:exttrip} allows us to finally substantiate
Theorem~\ref{thm:rdespar}. This then completes our preliminary results on parallel composition for reactive designs.

\vspace{1ex}

In this section, we have laid the foundations for our theory of reactive contracts, considering its foundations, links
to other theories, and recursion and parallel composition. We next consider its mechanisation in Isabelle/HOL, which
allowed us to mechanically prove the all of the laws previously presented.

redpajama_set_name: RedPajamaArXiv