Let the context of our discussion in this chapter be fixed with a
vocabulary $\vocab = (\myprocedure, \var, \globvar, \locvar)$, a
domain $\dom$ and a \minimp{} model $\model$.  Given a procedure
$f \in \myprocedure$, we use \textsf{body}($f$) to denote the body
statement of $f$.

The partial correctness of a MiniMP program can be specified as a
collective triple $\cotriplearg{\textsf{body}(\texttt{main})}$.  To
prove the validity of this triple in a composite and modular way, we
introduce an inference system, denoted $\corule$, in this chapter.  By
applying $\corule$ to $\cotriplearg{\textsf{body}(\texttt{main})}$,
the validity of the triple can be proved by proving a set of
collective triples, each of which specifies a smaller statement than
$\textsf{body}(\texttt{main})$.


The inference system $\corule$ is defined with a set of rules in
\S\ref{sec:minimp:spec:rule}.  \S\ref{sec:minimp:spec:rule:adaptation}
discusses about the \emph{adaptation problem} arising in practice of
the rules.  We show a derivation example of $\corule$ in
\S\ref{sec:rules:example}.  Finally, we define notations in
\S\ref{sec:extended:enter:exit}, which are used in the soundness proof
of $\corule$ in \S\ref{sec:rules:soundness}.



\section{Rules for Decomposing Collective
  Triples} \label{sec:minimp:spec:rule}

In this section, we introduce an inference system for composite and
modular verification of \minimp{} programs.  We use $\corule$ to
denote this inference system.  $\corule$ consists of four rules for
reasoning about collective triples.  With $\corule$, one is able to
decompose a collective triple $\cotriplenoloc{}$ into a set of
collective triples $\Tri$ such that $\model \models \cotriplenoloc{}$,
if $\forall{\tri \in \Tri}.\, \model \models \tri$.  Normally, proving
the validity of a $\tri \in \Tri$ is a much smaller problem than
proving the validity of the original triple.

The rules in $\corule$ involve assertions that will be explained
below.  These assertions, as well as the rules, constraint
path-requirements or guarantees.  As aforementioned, path-requirements
and guarantees can be represented by conjuncting over set
comprehensions of absence assertions.  Therefore, we define a few
operations that are similar to set operations for expressing those
assertions.  These operations shall be interpreted under a certain
context---a path, where there is exact one state for evaluating an
absence assertion involved in an operation.

\begin{defn}
  A \emph{partial evaluation}
  $\mypevaltitle\colon{} \sabsentv{_\vocab} \times \mystates{} \times \nprocs{n} \rightarrow \sabsentv{_\vocab}$
  is a function that maps an absence assertion to another absence
  assertion at a state for a process.  Given an absence assertion
  $\lambda$, a state $s$ and a process $p$, $\mypeval{\lambda}{s}{p}$
  is defined by \begin{align} \mypeval{\lambda}{s}{p} =~ & \text{let }
  p = \myeval{e_0}(s, p) \text{ in} \nonumber \\ & \text{let } q
  = \myeval{e_1}(s, p) \text{ in} \nonumber \\ & \text{let } r
  = \myeval{e_2}(s, p) \text{ in} \nonumber \\
  & \texttt{\acslabsent{\acslsend($p$, $q$)}{\acslexit($p$)}
  {\acslexit($r$)}}, \nonumber \\ & \text{if } \lambda
  = \texttt{\acslabsent{\acslsend($e_0$,
  $e_1$)}{\acslexit($e_0$)}{\acslexit($e_2$)}} \nonumber \\
  & \ldots{} \nonumber \end{align} For brevity, we do not show the
  full definition.  The omitted definition should be obvious to
  readers.  $\qed$
\end{defn}

\begin{defn}
  Let $\lambda$ be an absence assertion. Let
  $\lambda^0_a, \lambda^1_a, \ldots{}$ and
  $\lambda^0_b, \lambda^1_b, \ldots{}$ be absence assertions.  Let
  $e_a, e_b \in \sexprv_{\vocab}$.  Let $m_a, m_b$ be two positive
  integers. $\Lambda_a, \Lambda_b$ are two expressions of the
  forms: \begin{align} \Lambda_a =~~ e_a \texttt{ ==>
  } \lambda^0_a \texttt{ \&\& } \ldots{} \texttt{ \&\&
  } \lambda^{m_a-1}_a, \nonumber \\ \Lambda_b =~~ e_b \texttt{ ==>
  } \lambda^0_b \texttt{ \&\& } \ldots{} \texttt{ \&\&
  } \lambda^{m_b-1}_b. \nonumber \end{align} Let $\rho$ be a path.
  Let $s, s_a, s_b$ $\in \mypathstates(\rho)$ be the only states,
  where $\lambda$, $\Lambda_a$ and $\Lambda_b$ shall be evaluated,
  respectively.  We define \begin{align} \lambda \in_{\rho} \Lambda_a
  & \text{ iff
  } \exists{p \in \nprocs{n}}.\,\myseval{e_a}(s_a, p) = \textbf{T} \wedge{} \exists{m \in \nprocs{m_a}}.\, \lambda
  = \mypeval{\lambda^m_a}{s_a}{p} \nonumber \\
      %%%
    \Lambda_a \subseteq{_{\rho}} \Lambda_b
    &\text{ iff }
  \forall{i \in \nprocs{m_a}}.\forall{p \in \nprocs{n}}.\,
  \myseval{e_a}(s_a, p) = \textbf{T}  \Rightarrow{} \mypeval{\lambda^i_a}{s_a}{p}\in_\rho \Lambda_b \qed\nonumber
  \end{align}
\end{defn}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%    DEFINE HELPER ASSERTIONS       %%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Now we describe the assertions.  Let
Def.\ \ref{defn:guarantee:assertion}, Def.\ \ref{defn:nosend:subset},
Def.\ \ref{defn:infer:togather} and Def.\ \ref{defn:nocancel} be under the context described by the
following.  Let $C_0$ and $C_1$ be two \minimp{} substatements.
Suppose there are three triples: $\cotriplearg{C_0C_1}$,
$\mycosubtriple{0}{\psi_0}{\phi_0}{C_0}$ and
$\mycosubtriple{1}{\psi_1}{\phi_1}{C_1}$.  Let $\rho
= \pi_0 \circ{} \rho_1$ be a path such that $\pi_0$ is an execution of
$C_0$ and $\rho_1$ is a prefix of an execution of $C_1$.  Obviously,
according to the semantics of collective triples defined in
Def.\ \ref{defn:semantics:collective:triple},
$\Gamma, \Upsilon, \Gamma_0, \Upsilon_0$ shall be partially evaluated
at $\mysrc(\myhead(\rho))$, and $\Gamma_1, \Upsilon_1$ shall be
partially evaluated at $\mysrc(\myhead(\rho_1))$.

\begin{defn}
   The assertion \[\Upsilon_1~\ruleguarantee{_{\rho}}~\Gamma_0\] is
  true iff for
  every \[ \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\rho} \Gamma_0, \]
  there
  is \[ \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_{\rho} \Upsilon_1. \qed \] \label{defn:guarantee:assertion}
\end{defn}

\begin{defn}
  Let $i, j$ be two positive integers.  Let $e\in\sexprv_{\vocab}$.
  Let $\lambda_0, \lambda_1,\ldots{}$ and
  $\lambda'_0, \lambda'_1, \ldots$ be absence assertions.
  If $\Upsilon$ has such a form
  $e \texttt{ ==>
    } \lambda_0 \texttt{ \&\& } \ldots{} \texttt{ \&\&
    } \lambda_{i-1}$,
  $\nosendsubset$$(\Upsilon)$ denotes an expression of such a
  form:$ 
  e \texttt{ ==>
    } \lambda'_0 \texttt{ \&\& } \ldots{} \texttt{ \&\&
    } \lambda'_{j-1}$
  that
  \begin{enumerate}
\item  $\forall{x, y \in \nprocs{j}}.\, x \not= y \Rightarrow{} \lambda'_x \not= \lambda'_y$
\item  $\forall{y \in \nprocs{j}}.\exists{x \in \nprocs{i}}. \lambda'_y = \lambda_x$,
\item  every $\lambda'_k$ for $k \geq 0$ is of the form:
\[ \texttt{\acslguarantee{$p$}{$q$}{$r$}}.\]
\item there is no such integer $h$ that $h > j$ and 
      $  e \texttt{ ==>
    } \lambda'_0 \texttt{ \&\& } \ldots{} \texttt{ \&\&
    } \lambda'_{h-1}$ satisfies the three conditions above. $\qed$
\end{enumerate}
  \label{defn:nosend:subset}
\end{defn}      
In other words, if taking $\Upsilon$ as a set comprehension of absence
assertions, $\nosendsubset(\Upsilon)$ is the maximal subset of
$\Upsilon$ containing elements of the specific kind of absence
assertions.

\begin{defn}
  The assertion
  \[\myruleinfer{\Upsilon_0}{\Upsilon_1}{\nosendsubset(\Upsilon)}{\rho}\]
  is true iff for
  every \[ \upsilon~=~\texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_{\rho} \nosendsubset(\Upsilon), \]
  we have $\upsilon \in_{\rho} \Upsilon_0$,
  and \begin{itemize} \item \texttt{\acslwaitsfor{$p$}{$r$}}
  $\in_{\rho} \Upsilon_0$, or \item $\upsilon[x /
  r] \in_{\rho} \Upsilon_1$, if there is such $x\in\nprocs{n}$
  that\\ \texttt{\acslwaitsfor{$x$}{$r$}} $\in_\rho \Upsilon_0$,
  or \item $\upsilon \in_{\rho} \Upsilon_1~\vee{}~\upsilon[q /
  r] \in_\rho \Upsilon_1$. $\qed$ \end{itemize}
\label{defn:infer:togather}
\end{defn}

We explain Def.\ \ref{defn:infer:togather}.  An element
  $\upsilon \in_\rho \nosendsubset(\Upsilon)$ asserts that process $p$
  shall not send a message to process $q$ during in $C_0C_1$ before
  process $r$ entering $C_0C_1$.  We have $\Upsilon_0$ and
  $\Upsilon_1$ of $C_0$ and $C_1$, respectively, infer $\upsilon$, if

  \begin{itemize}
  \item[1] $\Upsilon_0$ also contains $\upsilon$.  If so, $p$ cannot
    send a message to $q$ during in $C_0$ before $r$ entering $C_0$.
  \item[2] Moreover, $p$ shall also not send a message to $q$ during
    in $C_1$ before $r$ entering $C_0$.  Hence, one of the following
    conditions must hold.

  \begin{itemize}
  \item[2.1] $C_0$ guarantees that the sender $p$ will not enter the
    following $C_1$ until $r$ enters itself;
    
  \item[2.2] If $C_0$ guarantees that some process $x$ will not enter the
    following $C_1$ until $r$ enters itself, $C_1$ shall guarantee
    that $p$ will not send a message to $q$ until $x$ enters itself.
    
  \item[2.3] $C_1$ guarantees that process $p$ will not send a message
    to $q$ until process $q$ or $r$ enters itself.
  \end{itemize}
    
  \end{itemize}

\begin{defn}
Let
\[
  \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\rho} \Gamma_0,
\]
we say $\Upsilon_1~\rulecancels{_{\rho}}~\gamma$ iff
\[
  \texttt{\acslwaitsfor{$p$}{$r'$}} \in_{\rho} \Upsilon_1,
\]
where $r' = r \vee r' = q$. $\qed$
\label{defn:nocancel}
\end{defn}
The intuitive meaning for Def.\ \ref{defn:nocancel} is that for a
$\gamma \in_\rho \Gamma_0$, if
$\Upsilon_1~\rulecancels{_\rho}~\gamma$, $C_0C_1$ no longer requires
$\gamma$.

Rules in Hoare logic is defined with respect to kinds of program
statements, such as branch or loop.  Here we define a premise of a
rule in $\corule$ that depends on the semantics instead of the
structure of \minimp{} programs.  We call this premise the
``elaboration condition'', because the complexity of proving this
premise for a substatement $C$ will be no less than elaborating all
executions in state space graphs of $C$.

\begin{defn}
  Let $\rho_0$ and $\rho_1$ be two paths.  Let $\xi_0$ and $\xi_1$ be
  two transition sequences that are the projections of $\rho_0$ and
  $\rho_1$, respectively, onto transitions associated with
  non-\myskipstmt{} actions.  We say $\rho_0$ and $\rho_1$
  are \emph{equivalent} if $\xi_0 = \xi_1$.
  $\qed$ \label{defn:path:equivalence}
\end{defn}

\begin{defn}
  Let $C$ and $C'$ be two substatements.  We say $C'$ \emph{contains
  behaviors of} $C$ \emph{under} $\psi$, denoted
  $\cocond{\psi, \emptyset}~\overrightarrow{C} \subseteq{} \overrightarrow{C'}$,
  if for every extended execution $\zeta$ of $C$ such that $\psi$
  holds on $\mysrc(\myhead(\zeta))$ for all processes, there is
  an \emph{equivalent} extended execution $\zeta'$ of $C'$.  $\qed$
\end{defn}


Now we define the rules in $\corule$.
\begin{defn}
  The
  \emph{inference system} $\corule$ for collective triples is defined
  in Fig.\ \ref{fig:triple:rules}. $\qed$
\end{defn}

\begin{figure}[t]
  \centering
  \fbox{
    \parbox{0.9\textwidth}{
  \begin{align}
    & \frac{
      \mycosubtriple{0}{\psi}{\mu}{C_0},\,\,
      \mycosubtriple{1}{\mu}{\phi}{{C_1}}
      }
      {
      \cotriplearg{C_0C_1}
      } ~~~\textit{(sequence)}\nonumber \\
    \text{if } & \text{for every execution } \pi_0 \circ{} \pi_1 \text{ of }
                 C_0C_1 \text{ s.t.\ } \nonumber \\
    \pi_0 &\text{ is an execution of } C_0 \text{
    and } \pi_1 \text{ is an execution of } C_1, \nonumber \\
    \text{1. }& \Upsilon_1~\ruleguarantee_{\pi_0 \circ{} \pi_1}~\Gamma_0, \nonumber \\
%    \text{and 2. }& \nosendsubset(\Upsilon) \subseteq \Upsilon_0,\nonumber\\
    \text{2. }&  \myruleinfer{\Upsilon_0}{\Upsilon_1}{\nosendsubset(\Upsilon)}{\pi_0 \circ{} \pi_1},    \nonumber \\
    \text{3. }& \Upsilon \subseteq_{\pi_0 \circ{} \pi_1} \Upsilon_0 \cup{}  \Upsilon_1,
                \text{ and}\nonumber \\
    \text{4. }& \{\gamma \in \Gamma_0 \mid \neg{}(\Upsilon_1~\rulecancels_{\pi_0 \circ{} \pi_1}~\gamma)\} \cup \Gamma_1~\subseteq_{\pi_0 \circ{} \pi_1}~\Gamma. \nonumber 
  \end{align}
  
  \begin{align}
      &\frac{
      \cocond{\psi', \Gamma'}~C~\cocond{\phi', \Upsilon'}
      }
      {
      \cocond{\psi, \Gamma}~C~\cocond{\phi, \Upsilon}
    } ~~~ \textit{(consequence)}  \nonumber \\
       \text{if for every } & \text{execution } \pi \text{ of } C,~ %\nonumber \\
       \Gamma' \subseteq_{\pi} \Gamma~\wedge{}~\Upsilon \subseteq_\pi \Upsilon'
        ~\wedge{}~\psi{} \Rightarrow \psi' ~\wedge{}~\phi' \Rightarrow \phi
        \nonumber
  \end{align}
  
  \begin{align}
    & \frac{
    \cocond{\mymath{inv} \wedge{} c,\, \Gamma}~C~
    \cocond{\mymath{inv},\, \Upsilon}
    }{
    \cocond{\mymath{inv},\,\Gamma{}}~ \texttt{while(}c\texttt{)}
    ~C ~\cocond{\neg{}c \wedge{} \mymath{inv},\, \Upsilon{}}
      } ~~~ \textit{(collective loop)} \nonumber \\
    & \text{if for every execution } \pi \text{ of } C, 
      \Upsilon{}~\ruleguarantee_\pi~\Gamma
      \nonumber 
  \end{align}
  
  \begin{align}
              \frac{
    \cocond{\psi{},\, \emptyset}~
    \overrightarrow{C} \subseteq{} \overrightarrow{C_0C_1}~
    ,\,\,
    \cocond{\psi{},\, \Gamma}~
    C_0C_1~
    \cocond{\phi{},\, \Upsilon}
    }{
    \cocond{\psi{},\, \Gamma}~
    C~
    \cocond{\phi{},\, \Upsilon}
    }~~~\textit{(elaboration)} \nonumber
  \end{align}
    }
}
  \caption{Rules for decomposing collective triples}
  \label{fig:triple:rules}
\end{figure}

The \textit{sequence}, \textit{consequence} and \textit{collective
  loop} rules in $\corule$ were inspired by the \textit{sequence},
\textit{consequence} and \textit{loop} rules in Hoare logic.  Rules in
$\corule{}$ over state-requirements and -guarantees are similar to
pre- and post-conditions in Hoare logic.  Rules over path-requirements
and -guarantees are explained by the follows.

The \textit{sequence} rule is the basis of the decomposition.  For a a
sequence of two substatements $C_0C_1$, in order to prove
$\model \models \cotriplearg{C_0C_1}$, one proves
$\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and
$\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$ separately instead.
The decomposition is feasible if all the side conditions are
satisfied.

Side Condition 1 enforces that $C_0$ will never be interfered by
$C_1$.  The meaning of Side Condition 2 has been explained with the
``$\ruleinfer{\ldots}{\ldots}{\ldots}$'' assertion above.  Side
Condition 3 expresses that the path-guarantees of $C_0$ and $C_1$
together shall be no weaker than the one of $C_0C_1$.  Stated by Side
Condition 4, since $\Upsilon_1$ may $\rulecancels$ some elements in
$\Gamma_0$, the path-requirement of $C_0$ and $C_1$ together may be
weaker but shall not be stronger than the one of $C_0C_1$.

The \textit{consequence} rule is more obvious: if a collective triple
is valid, it is still valid after strengthening its state- or
path-requirement, and it is still valid after weakening its state- or
path-guarantee.


The \textit{collective loop} rule requires the user to provide a loop
invariant $\mymath{inv}$. This rule can only be applied to the loops
whose body $C$ can be specified by a collective triple
$\cotriplenoloc{}$.  In other words, the loop body must be collective
style.  This rule can be seen as a sequence of applications of the
\textit{sequence} rule to the unrolled loop body $CC\ldots{}$.

The \textit{elaboration} rule is designed for the cases where a
collective triple cannot be decomposed by the three rules above due to
the existence of branches, such as the following statement $C$ (at
line 3--6):
  \begin{center}
    \begin{program}
      \ccode{var} dat;\\
      ...\ \\
      \ccode{if} (PID == 0) \\
      \lb{}bcast(dat, 0); gather(dat, 0);\rb{} \\
      \ccode{else} \\
      \lb{}bcast(dat, 0); gather(dat, 0);\rb{}
    \end{program}
  \end{center}
  where \texttt{bcast} and \texttt{gather} are procedures defined in
  Fig.\ \ref{fig:minimp:example:bcast} and
  \ref{fig:minimp:example:gather}, respectively.  One can tell that
  the code above is equivalent to such a sequence of calls
  \begin{center}
    \texttt{bcast(dat, PID); gather(dat, PID);}.
  \end{center}
  However, the sequence rule is not suitable for the original branch.
  With the elaboration rule, if one can prove the ``elaboration
  condition'',
  \begin{center}
    $\cocond{\psi, \emptyset{}}~\overrightarrow{C} \subseteq
    \overrightarrow{\texttt{bcast(dat, PID);gather(dat, PID);}}$
  \end{center}
  for some condition $\psi$, is valid, one can infer a collective
  triple of the original branch from a triple of the sequence of
  calls.  The latter triple can be further decomposed by an application
  of the sequence rule.  Proving the elaboration condition requires
  some other techniques, such as model checking.  It is out of the
  scope of this chapter.

  Concluding this section, $\corule$ is incomplete.  It means that it
  is not always the case that a collective triple can be derived by
  $\corule$.  As we argued in Chapter \ref{chp:intro}, the
  effectiveness of $\corule$ relies on the collective programming
  style, which dominates the message-passing HPC programming.

%%%%%%%%%%%%%%%%%% ADAPTATION %%%%%%%%%%%%%%%%%%
  \section{The Adaptation
    Problem} \label{sec:minimp:spec:rule:adaptation} There is an
  \emph{adaptation problem} that arises from re-using verified
  collective triples.  Example \ref{exam:minimp:rule:adaptation} shows
  such a problem.

\begin{exmp}
  Let $C$ be the left and $C'$ be the right
  statements below:
  
  \begin{minipage}[t]{.45\textwidth}
    \begin{program}
      \ccode{if} (PID == 0) \lb{} \\
      \ \ send(x, y); \\
      \rb{} \ccode{else if} (PID == 1) \lb{} \\
       \ \ recv(x, 0); \\
        \rb{} \\
    \end{program} \\
\end{minipage}
\begin{minipage}[t]{.45\textwidth}
    \begin{program}
      \ccode{if} (PID == 0) \lb{} \\
       \ \ send(x, z); \\
       \rb{} \ccode{else if} (PID == 1) \lb{} \\
       \ \ recv(x, 0); \\
       \rb{} \\
    \end{program} \\
\end{minipage}\\

The only difference between $C$ and $C'$ is that variable \texttt{y}
in $C$ is replaced by \texttt{z} in $C'$.  Now suppose that we have
verified a collective triple of $C$,
$\cocond{\texttt{y} = 1, \Gamma}~C~\cocond{\phi,
  \Upsilon}$, and is going to verify a collective triple of $C'$,
$\cocond{\texttt{z} = 1, \Gamma}~C'~\cocond{\phi,
  \Upsilon}$.  Intuitively, the validity of the triple of $C'$ can be
concluded from the former one.  However, no rule in $\corule$ can be
applied here to re-use the verified triple of $C$ without a variable
name substitution from \texttt{y} to \texttt{z} happens first. $\qed$
\label{exam:minimp:rule:adaptation}
\end{exmp}

To generalize the solution to the problem of Example
\ref{exam:minimp:rule:adaptation}, one shall allow free substitution
from existing variable names to fresh new variable names over
collective triples.  Such substitutions are common transformations in
first order logic that cannot affect the validity of collective
triples.  In this dissertation, we will not discuss about details in
solving adaptation problem for two reasons.

First, the adaptation problem has been well studied and tackled by
earlier works \cite{hoare:1969:axiomatic,
  Kleymann:1999:HLA:2769784.2769811}.  There is nothing new in this
problem for our unique inference system for \minimp{}.
  
More importantly, in later chapters, we will focus on applying
collective triples to procedures only.  This is one of the typical
ways to implement a contract based verification system.  For \minimp{}
procedures, the adaptation problem is naturally solved.  Recall the
semantics of \minimp{} in \S\ref{sec:minimp:semantics}, a mapping from
actual parameters to formal parameters happens automatically.  In
addition,  global variables are visible everywhere in a program.  No
substitution is ever needed for global variables.
  

%%%%%%%%%%%%%%%%%% EXAMPLES %%%%%%%%%%%%%%%%%%

\section{An Derivation Example} \label{sec:rules:example}

We now show an example of the application of $\corule$.

Figure \ref{fig:minimp:corule:example:1} shows a contract for the
sequential combination $C=C_0C_1$ of two substatements. $C_0$ and its
contract are given by Fig.\ \ref{fig:minimp:spec:bcast}. $C_1$ and its
contract are given by Fig.\ \ref{fig:minimp:spec:gather}.  Recall that
we have explained in \S\ref{sec:minimp:spec:triple} that the contract
of $C_1$ misses a path-requirement.

Figure \ref{fig:minimp:corule:apply:1} shows a $\corule$ derivation of
the collective triple representing $C$ and its contract.  In the
derivation, we write $\textsf{id}$ for the value of \texttt{PID}, $n$
for the value of \texttt{NPROCS}, $v$ for the value of \texttt{val},
and $r$ for the value of \texttt{root}.  We write $x_p$ for a
variable or value $x$ on process $p$.  Let $X_p, Y_p, Z_p \in \dom$ be
values of \texttt{dat} on a process $p \in \nprocs{n}$ at different
states.  In this derivation, irrelevant conditions are
simplified, e.g., we ignored the values of variables \texttt{root} and
\texttt{val} in the state-guarantee of Triple 1.

At a generic pre-state of $C$, variable \texttt{dat} on process $i$
holds value $X_i$.  We simplified the condition that all processes
have an agreement on their values of \texttt{root} by letting all
processes have the same value $r$ for \texttt{root}.  Note the
state-guarantee in Triple 1 involves the use of the
\texttt{\acslold{}} construct to refer the value $X_i$ of \texttt{dat}
at the pre-state on process $i$.  Triple 1 represents $C$ and its
contract. It can be proved valid if Triple 1.1 and 1.2 are valid,
according to the sequence rule.

Triple 1.1 relates to the contract of $C_0$.  Note we added the
path-requirement here that was missing in Fig.\
\ref{fig:minimp:spec:gather}.  Besides, since \texttt{dat} is modified
by $C_0$, the value of \texttt{dat} at the post-state of $C_0$ needs
to be represented by a different symbol $Y$.  According to the
contract of $C_0$, elements in \texttt{dat} on process \texttt{root}
are ``gathered'' from other processes, i.e.,
\[
  \forall{t \in \nprocs{n}}.\, Y_r = X_t[t].
\]

Triple 1.2 relates to the contract of $C_1$.  In addition to the
contract showed in Fig.\ \ref{fig:minimp:spec:bcast}, we added an
extra path guarantee
\begin{center}
  \texttt{\acslguarantee{\textsf{id}}{\texttt{root}}{\texttt{root}}}.
\end{center}
Adding such a path guarantee strengthens the guarantee of the original
contract.  It is not hard for the reader to find out that $C_1$ still
satisfies the strengthened contract.  By the consequence rule, if the
strengthened the triple is valid, the original triple of $C_1$ is also
valid.  This extra path guarantee is required in meeting Side Condition
1 of the sequence rule.  The rest of the side conditions are valid
with obviousness.  At the post-state of $C_1$, the values of
\texttt{dat} are represented with the symbol $Z$ for the
aforementioned reason.  The state-guarantee can be further simplified
to be exact the same as the state-guarantee in Triple 1.

\begin{figure}
\begin{center}  
  \begin{program}
    \ccode{var} dat, val, root, i, y;\\
    ...\ \\
    \mycomment{// contract:}\\
    \ccode{requires} \acslforall{} t; \acslon{}(root, t) == root;\\
    \ccode{requires} 0 <= root \&\& root < NPROCS \&\& val == dat[PID];  \\
    \ccode{assigns} dat, i, y;\\
    \ccode{ensures} \acslforall{} t; 0 <= t \&\& t < NPROCS ==>\\
    \ \ \ \ \ \ \ \ \ \
    dat[t] == \acslold(\acslon(dat[t], t)); \\
    \ccode{ensures}
    \acslabsent{\acslexit(PID)}{\acslenter(PID)}{\acslenter(root)};\\
  \end{program}
\end{center}
\caption{A contract for the sequential combination of the two branch
  statements given by Fig.\ \ref{fig:minimp:spec:gather} and
  \ref{fig:minimp:spec:bcast}.}
\label{fig:minimp:corule:example:1}
\end{figure}

\begin{figure}[t]
  \centering
    \fbox{
    \parbox{.97\textwidth}{
  \[
    \begin{array}{l l l}
      1. &  \lco{}~\textsf{dat}_{\textsf{id}} = X_{\textsf{id}}
           \wedge{} \texttt{root}_{\textsf{id}} = r
           \wedge{} \texttt{val}_{\textsf{id}} = v_{\textsf{id}}
           \wedge{} & \hspace{-3cm}\text{(seq 1.1, 1.2)}
      \\[\myskip]
         &~~X_{\textsf{id}}[\textsf{id}] = v_{\textsf{id}} \wedge{}
           0 \leq r < n,\,  \emptyset & \\
         &~\rco{} & \\[\myskip]
         &~C_0C_1 & \\[\myskip]
         & \lco{}~
           \forall{t \in \nprocs{n}}.\,
           Z_{\textsf{id}}[t] =
           X_t[t]~\wedge{}~\textsf{dat}_{\textsf{id}} = Z_{\textsf{id}}, & \\
         &~~\{\texttt{\acslwaitsfor{\textsf{id}}{$r$}}\}  & \\
         & \rco{} & \\[\myskip]
      1.1. & \lco{}~\textsf{dat}_{\textsf{id}} = X_{\textsf{id}}
             \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{}
             \texttt{val}_{\textsf{id}} = v_{\textsf{id}} \wedge{}
             X_{\textsf{id}}[\textsf{id}] = v_{\textsf{id}} \wedge{} 0
             \leq r < n,
                    & \\[\myskip]
         &~\{\texttt{\acslgamma{\textsf{id}}{$r$}{$r$}}\}~ &
      \\  [\myskip]
         & \rco{} &\\
         & ~C_0 & \\  [\myskip]
         & \lco{}~(\forall{t \in \nprocs{n}}.\, Y_r[t]
           = X_t[t]) \wedge{} \textsf{dat}_{\textsf{id}} =
           Y_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{}
           0 \leq{} r < n,\,
           \emptyset{}~\rco{}~ \\ [\myskip]
      1.2. &  \cocond{~(\forall{t \in \nprocs{n}}.\, Y_r[t]
             = X_t[t]) \wedge{} \textsf{dat}_{\textsf{id}} =
             Y_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{}
             0 \leq{} r < n,\,
             \emptyset{}~}  & \\  [\myskip]
         & ~C_1 & \\ [\myskip]
         & \lco{}~(\forall{t \in \nprocs{n}}.\, Y_r[t] =
           X_t[t])~\wedge{}~\textsf{dat}_{\textsf{id}} =
           Z_{\textsf{id}}~\wedge{}~Z_{\textsf{id}} =
           Z_r~\wedge{}~Z_r
           = Y_r, & \\
         & \texttt{\ \
           $\{$\acslguarantee{\textsf{id}}{$r$}{$r$}}, & \\
         & \texttt{\ \ \ \acslwaitsfor{\textsf{id}}{$r$}} \} &\\
         &\rco{}&             
    \end{array}
  \]
  }}
\caption{A $\corule$ derivation of a collective triple that specifies
  a sequential combination of two collective style \minimp{} statements.
}
\label{fig:minimp:corule:apply:1}
\end{figure}



%%%%%%%%%%%%%%%%%% SOUNDESS %%%%%%%%%%%%%%%%%%
\section{Extending the Entering/Exiting
  Notation} \label{sec:extended:enter:exit} In
\S\ref{sec:minimp:spec:progseg}, we defined two notations
$\myenter^C_{p, \rho}$ and $\myexit^C_{p, \rho}$ for marking the first
entering and the corresponding exiting of a substatement $C$ by a
process $p$ on a path $\rho$.  Here we extend such notations for a
sequence of statements $C_0C_1\ldots{}C_{m-1}$.

\begin{defn}
  
  Let
  $\progsegs{l_0}{C_0}{l_1}{C_1}{l_2}\ldots{}\progseg{l_{m-1}}{C_{m-1}}{l_m}$
  be a program segment of the statement $C = C_0C_1\ldots{}C_{m-1}$.
  Let $\rho$ be a path.  Let $t \in \mypathtrans(\rho)$ be a global
  transition of the path $\rho$.  We define $\myenter^{C_i}_{p, \rho}$
  and $\myexit^{C_i}_{p, \rho}$ for $0 \leq{} i < m$ by
  
  \begin{itemize}
  \item $\myenter^{C_0}_{p, \rho} = \myenter^C_{p, \rho}$,

  \item $t = \myenter^{C_i}_{p, \rho}$, for $i > 0$, 
    if $t$ is the first such
    transition appearing after $\myexit^{C_{i-1}}_{p, \rho}$ on $\rho$
    that
    \[
      \mytoploc(\mysrc(t), p) = l_i~\wedge{}~\myproc(t) = p
    \]

  \item $t = \myexit^{C_i}_{p, \rho}$, for $i \geq{} 0$, if $t$ is the
    first such transition appearing after $\myenter^{C_i}_{p, \rho}$
    on $\rho$ that
    \[
      \mytoploc(\mydest(t), p) = l_{i+1}~\wedge{}~\myproc(t) =
      p~\wedge{}~|\mystack(\mydest(t), p)| =
      |\mystack(\mysrc(\myenter^{C_i}_{p, \rho}), p)|
    \]
  \end{itemize}
  $\qed$
\end{defn}

Intuitively, $\myenter^{C_i}_{p, \rho}$ and $\myexit^{C_i}_{p, \rho}$
represent the entering and exiting, respectively, of each
substatement $C_i$ of $C$ by the process $p$ on $\rho$.  Again, when
$\rho$ is clear in the context, we may simplify the notations to
$\myenter^{C_i}_p$ and $\myexit^{C_i}_p$.

Remark that, for an execution or an extended execution with $n$
processes of $C_0C_1\ldots{}C_{m-1}$, there is a unique
$\myenter^{C_i}_p$, or $\myexit^{C_i}_p$, for
$p \in \nprocs{n}, 0 \leq{} i < m$.

%% does the event interpretation and absence assertion evaluation need
%% to be extended ???
%%%% For The interpretation of events $I^{\textsf{event}}_{C, \rho}$
%%%% has to be generalized accordingly.

%%With the generalized event interpretation, the absence assertion
%%interpretation $\myaeval{~}$ is generalized naturally.

\section{Soundness} \label{sec:rules:soundness}
This section presents a proof for the soundness of $\corule$.

\begin{defn}
  Let $t \circ{} t'$ be a path.  Let $\myact(t) =
  p \wedge{} \myact(t') = q$ such that $p \not= q$.  The actions of
  $t$ and $t'$ are said to be \emph{swappable} if it is not the case
  that \[ \myact(t) = \myactsend{$v$}{$q$}~\wedge{}~\myact(t')
  = \myactrecv{$v'$}{$p$}~\wedge{}~\mychan(\mysrc(t))(p, q)
  = \epsilon \qed\] 
\end{defn}
For convenience, we also say two global transitions $t$ and $t'$ are
swappable if their actions are swappable.  Intuitively, $t$ and $t'$
are swappable if they are associated with different processes and they
are independent, i.e., $\myproc(t)$ can execute $\myact(t)$ regardless
of $t'$ being executed first or not, and vice versa; $t$ and $t'$
cannot access the process state of a same process or the same message
in a message channel.

\begin{lema}
  Let $s \xrightarrow[p]{a} s'$ represent a global transition
  $t = (s, p, \alpha, s')$ such that $\myact(t) = a$.  A path then can
  be written as
  $\ldots{} s_0 \xrightarrow[p]{a} s_1 \xrightarrow[q]{b} s_2
  \ldots{}$.  For
  $s_0 \xrightarrow[p]{a} s_1 \xrightarrow[q]{b} s_2$, if the two
  global transitions 
  are swappable, we have
  \begin{center}
    $s_0 \xrightarrow[q]{b} s_1' \xrightarrow[p]{a} s_2$
  \end{center}
\label{lema:base}
\end{lema}

\noindent{} \textbf{Proof} A proof can be constructed by induction on
atomic actions of the two global transitions.  We omit this proof for
two reasons (1) it is in fact a more specific case of the general
\emph{reduction} approach proposed by Lipton in
\cite{lipton:reduction}; and (2) the lemma is intuitive and is
well-known in the field of verification of message-passing programs.
$\qed$

Given a path $\rho\colon{} s_0 \xrightarrow[p]{a}
s_1 \xrightarrow[q]{b} s_2$ with two swappable transitions, the path
$s_0 \xrightarrow[q]{b} s_1' \xrightarrow[p]{a} s_2$ is said to be
obtained via \emph{swapping transitions} of $\rho$.  And, by Lemma
\ref{lema:base}, we know these two paths share their initial and the
final states.

  %%%% SUFFICIENT NON-INTERFERENCE LEMMA
\begin{lema}
 Let $\rho$ be a path in the state space graph of $C_0C_1$ with $n$
  processes.  If $C_1$ does not interfere $C_0$, then for every
  sub-path $t \circ{} t'$ of $\rho$ such that (1)
  $\myproc(t) \not= \myproc(t')$, and (2) $t$ appears before
  $\myexit^{C_0}_{\myproc(t), \rho}$ and $t'$ appears after
  $\myexit^{C_0}_{\myproc(t'), \rho}$ on $\rho$,
  formally, 
  \begin{align} 
  \exists{i, j, x, y \in \mathbb{Z}}.\,\, & i
  < j~\wedge{}~x < y~\wedge{}~t = \rho[i]~\wedge{}~t'
  = \rho[y]~\wedge{} \nonumber \\ &\myexit^{C_0}_{\myproc(t), \rho}
  = \rho[j] \wedge{} \myexit^{C_0}_{\myproc(t'), \rho}
  = \rho[x], \nonumber 
  \end{align}
 then $t$ and $t'$ are
  swappable.  \label{lema:gen:non-interfere-sufficient} \end{lema} \noindent\textbf{Proof}
  We prove by contradiction.  Suppose that there is a sub-path
  $t \circ{} t'$ of $\rho$ satisfying Condition 1 and 2 given in the
  lemma above, but $t, t'$ are not swappable.  Let $\myproc(t) = p$,
  $\myproc(t') = q$, and $\rho_p$, $\rho_q$ be two prefixes of $\rho$
  such that $\rho_p$ ends with $\myexit^{C_0}_p$ and $\rho_q$ ends
  with $\myexit^{C_0}_q$, respectively.  Since $C_0$ is not interfered
  by $C_1$ on $\rho$,
\begin{equation}
  \mynsends{\rho_p}{p}{q} = \mynrecvs{\rho_q}{p}{q}~\wedge{}~
  \mynsends{\rho_q}{q}{p} = \mynrecvs{\rho_p}{q}{p}  \tag{3}
\end{equation}
    Since $t$ and $t'$ are not swappable,
    $\mychan(\mysrc(t))(p, q) = \epsilon$.  Let $\rho_t$ be the prefix
    of $\rho_p$ that ends with $t$.  We have
    \begin{equation}
      \mynrecvs{\rho_{t}}{p}{q} = \mynsends{\rho_{t}}{p}{q}. \tag{4}
    \end{equation}
    Since $\myact(t) = \myactsend{p}{q}$,
    \begin{equation}
      \mynsends{\rho_p}{p}{q} > \mynsends{\rho_{t}}{p}{q}. \tag{5}
    \end{equation}
   Simplifying $(3), (4), (5)$ to   
   \begin{equation}
     \mynrecvs{\rho_q}{p}{q} > \mynrecvs{\rho_{t}}{p}{q}.  \tag{6}
   \end{equation}
    However, by our assumption, $t \circ{} t'$ appears after
    $\myexit^{C_0}_q$ on $\rho$, we have
    \begin{equation}
    \mynrecvs{\rho_q}{p}{q} \leq  \mynrecvs{\rho_{t}}{p}{q}. \tag{7}
    \end{equation}
  There is a contradiction between $(6)$ and $(7)$. $\qed{}$
 

  \begin{coro} Let $\pi$ be an execution in a state space graph of
    $C_0C_1$ that ends with the termination of all processes.  If
    $C_1$ cannot interfere $C_0$,
    Lemma \ref{lema:gen:non-interfere-sufficient} allows one to keep
    swapping swappable transitions on $\pi$ to produce an alternative
    path $\pi'$ in the same state space graph such that

  \begin{enumerate}
  \item $\pi$ and $\pi'$ share their initial and the final states.
  \item $\pi' = \pi_0 \circ{} \pi_1$, where $\pi_0$ is an execution of
    $C_0$ and $\pi_1$ is an execution of $C_1$.   $\qed$
  \end{enumerate}
  \label{coro:pre:post:alternative}
\end{coro}


  %%%% REPRODUCE LEMMA
\begin{lema}
  Let $\zeta$ be an extended execution of $C_0C_1$ with $n$ processes.
  Let $P$ be a set of processes such that \[ p \in P \text{ iff
  } \myexit^{C_0}_{p, \zeta} \in \mypathtrans(\zeta).  \] Now
  if \[ \forall{q \in \nprocs{n}}.\,\forall{p \in
  P}.\,\, \mychan(\mydest(\myexit^{C_0}_{p, \zeta}))(q, p)
  = \epsilon, \] then there is another extended execution $\zeta'$ of
  $C_0C_1$ with $n$ processes such that $\zeta'
  = \pi_0' \circ{} \zeta_1'$, where
  
  \begin{enumerate}
  \item $\pi_0'$ is an execution of $C_0$ with $n$ processes,

  \item $\zeta_1'$ is an extended execution of $C_1$ with $n$ processes,
    
  \item $\forall{t \in \mypathtrans(\zeta_1')}.\, \myproc(t) \in P$, and
    
  \item every global transition $t \in \mypathtrans(\zeta_1')$
    corresponds to a unique one appearing after
    $\myexit^{C_0}_{\myproc(t), \zeta}$ on
    $\zeta$, formally, 
    \begin{align}
      & \text{let } N = \{i \in \mathbb{Z} \mid 0 \leq{} i < |\zeta|\}
        \text{ in} \nonumber \\
      & \forall{t' \in \mypathtrans(\zeta_1')}.\,
      \exists{t \in \mypathtrans(\zeta)}.\,\exists{i, j \in N}.\,\, i < j~\wedge{}~
        \zeta[i] = \myexit^{C_0}_{\myproc(t)}~\wedge{} \nonumber \\
      &~~~~~~~~~~~~~~~~\zeta[j] = t~\wedge{}~\myact(t) =
        \myact(t')~\wedge{}~\myproc(t) = \myproc(t'). \nonumber
    \end{align}
  \end{enumerate}
  \label{lema:seq:reproduce}
\end{lema}

\noindent\textbf{Proof}
Considering the same path $\zeta$ and process set $P$ in this lemma.  By
Lemma \ref{lema:base} and \ref{lema:gen:non-interfere-sufficient}, we
have an alternative path $\rho$ to $\zeta$ with $n$ processes such that

  \begin{enumerate}
  \item $\rho$ shares the initial state with $\zeta$
  \item $\rho = \rho_0 \circ{} \rho_1$ such that
    \[
       p \in P \text{ iff } \myexit^{C_0}_{p, \rho} \in
      \mypathtrans(\rho_0) ~\text{ and }~
       p \in P \text{ iff } \myenter^{C_1}_{p, \rho} \in
      \mypathtrans(\rho_1) \tag{2.1}
    \]
  \end{enumerate}
  Condition 2.1 above implies that (1) all processes in $P$ are at the
  exit of $C_0$ (or entry of $C_1$) at the final state of $\rho_0$
  while other processes are still in $C_0$, and (2) $\rho_1$ contains
  no transition associated with processes not in $P$.

  Furthermore, according to the assumption over message channels, we
  have
  \[
  \forall{q \in \nprocs{n}}.\,\forall{p \in
    P}.\,\mychan(\mysrc(\myhead(\rho_1)))(q, p) = \epsilon.
  \]
  Therefore, no transition in $\rho_1$ depends on any process
  in $\nprocs{n}\BSL{}P$ or the message channels from
  $\nprocs{n}\BSL{}P$ to $P$ at the initial state of $\rho_1$.

  Now we first construct the execution $\pi_0'$ of $C_0$ to
  $\pi_0' = \rho_0 \circ{} \rho_0'$ via letting all processes in
  $\nprocs{n} \BSL{} P$ continue to execute from
  $\mydest(\mytail(\rho_0))$ until they are all at the exit of $C_0$.
  Process states of processes in $P$ stay the same along $\rho_0'$
  because none of them ever executes.
  Note we are not interested in non-termination problem here.

  Second, we construct the $\zeta'$ to
  $\zeta' = \pi_0' \circ{} \zeta_1'$ via making $|\rho_1| = |\zeta_1'|$
  and
  \[
    \forall{i\in\mathbb{Z}}.\, 0 \leq{} i < |\rho_1| \Rightarrow{}
    \myproc(\rho_1[i]) = \myproc(\zeta_1'[i])~\wedge{}~ \myact(\rho_1[i]) =
    \myact(\zeta_1'[i]).
  \]
  Although there is no guarantee that
  $\mychan(\mydest(\mytail(\pi_0'))(q, p) = \epsilon$ for some
  $q \in \nprocs{n}$ and $ p \in P$, transitions in $\rho_1$ only
  depend on the process states of processes in $P$.  So the
  construction is feasible.

  Remark that transitions in $\rho_1$ are obtained by swapping
  transitions in $\zeta$, so Condition 4 in this lemma is naturally
  implied.  $\qed$

\begin{teom}[soundness of the sequence rule]
    Assuming all the side conditions of the sequence rule hold,
  \begin{center}
    $\model \models \cotriplearg{C_0C_1}$, if \\
    $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and
    $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$.
\end{center}
\label{lema:seq}
\end{teom}

\noindent\textbf{Proof}
The proof of Theorem \ref{lema:seq} is carried out by Lemma
\ref{lema:seq:zero}, \ref{lema:seq:one}, \ref{lema:seq:two} and
\ref{lema:seq:three}. $\qed$

%%%% LEMMA ZERO
\begin{lema}
  Under the assumption made in Theorem \ref{lema:seq}, for an
  execution $\pi$ in the state space graph of $C_0C_1$ with $n$
  processes, if $\psi$ and $\myallemptyguard{}$ hold on the initial
  state for all processes, $C_1$ does not interfere $C_0$ on $\pi$.
  \label{lema:seq:zero}
\end{lema}

\noindent\textbf{Proof}
We prove by contradiction.  Assuming $\myinterfere{\pi}{C_0}(p, q)$
for an ordered pair of unique processes $p, q \in \nprocs{n}$.
Without loss of generality, we also assume that

\begin{enumerate}
\item[(a)] $(p, q)$ is the only such ordered pair of processes that
  $\myinterfere{\pi}{C_0}(p, q)$, and

\item[(b)] let $\rho_p$ and $\rho_q$ be the prefixes of $\pi$ that end
  with $\myexit^{C_0}_{p, \pi}$ and $\myexit^{C_0}_{q, \pi}$, respectively, 
  $\mynsends{\rho_p}{p}{q} + 1 = \mynrecvs{\rho_q}{p}{q}$.
\end{enumerate}
Then $\pi$ must have such a form:
$\ldots{} \circ{} t_p \circ{}\ \ldots{} \circ{} t_q \circ{} \ldots{} $, where
\begin{enumerate}
\item $\myproc(t_p) = p$, $\myact(t_p) = $ \myactsend{$v$}{$q$},
  $\myproc(t_q) = q$ and $\myact(t_q) = $ \myactrecv{$v'$}{$p$}, for
  some $v$ and $v'$,  and

\item $\mychan(\mysrc(t_p))(p, q) = \epsilon{}$, and
\item $t_p$ appears after $\myexit^{C_0}_{p,\pi}$ and $t_q$ appears
  before $\myexit^{C_0}_{q,\pi}$ on $\pi$.
\end{enumerate}

Since $C_0$ is interfered by $C_1$ as above, and
$\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$,
it must be the case that
\begin{align}
 \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_0, \nonumber
\end{align}
for some processes $r \in \nprocs{n}$.

Considering the prefix $\rho$ of $\pi$ that ends with $t_p$.  Let $P$
be the set of processes such that $x \in P$ iff
$\myexit^{C_0}_x$ is in $\mypathtrans(\rho)$.  Obviously $p \in P$ and
$q, r \not\in P$.  By the assumption (a) above, we have
\[
\forall{y \in \nprocs{n}}\forall{x \in P}.\,
\mychan(\mysrc(\myhead(\myexit^{C_0}_x)))(y, x) = \epsilon{}.
\]
So we can apply Lemma \ref{lema:seq:reproduce}. It results in the
existence of an extended execution $\zeta = \pi_0 \circ{} \rho_1$ of
$C_0$ such that

\begin{itemize}
\item the execution $\pi_0$ of $C_0$ shares the initial state
  with $\pi$,

\item $\rho_1$ is a prefix of an execution of $C_1$, and

\item $\forall{t \in \mypathtrans(\rho_1)}.\,\, \myproc(t) \in P$ and
  $\exists{t \in \mypathtrans(\rho_1)}.\,\, \myact(t) = $
  \myactsend{$v$}{$q$} for some $v$.
\end{itemize}
Note $\zeta$ is also in the same state space graph as where $\pi$ is
in.

Since $\pi_0$ is an execution of $C_0$, which shares the initial state
with $\pi$, and the triple of $C_0$ is valid, we have $\mu$ and
\myallemptyguard{} hold at the final state $\mydest(\mytail(\pi'))$
(equal to $\mysrc(\myhead(\rho'))$) for all processes.

Since $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$,
considering the $\rho_1$, there is no 
\begin{align}
    \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_{\rho_1} \Upsilon_1 \nonumber
\end{align}
such that  $r' = r \vee r' = q$.

Thus, for $\zeta$, the assertion
$\Upsilon_1~\ruleguarantee{_\zeta}~\Gamma_0$ fails to hold.  It
contradicts the assumption that Side Condition 1 is satisfied. $\qed$

%%%%%%%%%%%%%% LEMMA ONE %%%%%%%%%%%%%%%%%%%

\begin{lema}
  Under the assumption made in Theorem \ref{lema:seq}, if an execution
  $\pi$ of $C_0C_1$ emanates from a pre-state of $C_0$ where $\psi$
  and $\myallemptyguard{}$ hold for all processes, and $\pi$ ends with
  a post-state of $C_1$, then $\phi$ and $\myallemptyguard{}$ hold on
  the post-state for all processes.
  \label{lema:seq:one}
\end{lema}

\noindent\textbf{Proof}
According to Lemma \ref{lema:seq:zero}, $C_0$ cannot be interfered by
$C_1$ on $\pi$.  Then we can apply Corollary
\ref{coro:pre:post:alternative}.  It results in an alternative $\pi'$
to $\pi$ in the same state space graph such that

\begin{enumerate}
\item $\pi$ and $\pi'$ share the initial and the final states, and
  
\item $\pi' = \pi_0 \circ{} \pi_1$ such that $\pi_0$ is an execution
  of $C_0$ and $\pi_1$ is an execution of $C_1$.
\end{enumerate}

Because of $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and
$\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$, we have $\phi$ and
$\myallemptyguard$ hold on $\mydest(\mytail(\pi'))$.  Thus, $\phi$ and
$\myallemptyguard$ also hold on $\mydest(\mytail(\pi))$.  $\qed$

%%%%%%%%%%%%%%%% LEMMA TWO %%%%%%%%%%%%%%%%%%
\begin{lema}
  Under the assumption made in Theorem \ref{lema:seq}, for an
  execution $\pi$ with $n$ processes of $C_0C_1$ that emanates from a
  pre-state $s$ of $C_0$, where $\psi$ and $\myallemptyguard{}$ hold
  for all processes,
  $\forall{p \in \nprocs{n}}. \pi \vdash{} \myaeval{\textup{$\Upsilon$}}_{C_0C_1}(s, p)$.
  \label{lema:seq:two}
\end{lema}

\noindent\textbf{Proof}
By Lemma \ref{lema:seq:zero}, $C_1$ cannot interfere $C_0$.  We prove
this lemma by contradiction.  Let $p, q, r, x \in \nprocs{n}$ be some
processes.  Let $s = \mysrc(\myhead(\pi))$.  Suppose that there is an
absence assertion $\upsilon \in_\pi \Upsilon$ such that
\begin{equation}
  \pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k), \tag{a}
  \label{lema:seq:two:proof:a}
\end{equation}
for any $k \in \nprocs{n}$.  There are two cases according to the
possible forms of $\upsilon$.

Case 1,  we have
\begin{equation}
  \upsilon = \texttt{\acslwaitsfor{$p$}{$q$}}. \tag{b}
  \label{lema:seq:two:proof:caseone:b}
\end{equation}

By Side Condition 3 of the sequence rule, there are two sub-cases.

\begin{enumerate}
\item[(1.1)] $\upsilon \in_\pi \Upsilon_0$.
  By Corollary \ref{coro:pre:post:alternative}, there is an
  alternative execution $\pi'$ to $\pi$ such that
  $\pi' = \pi_0 \circ{} \pi_1$, where

  \begin{itemize}
  \item $\pi$ and $\pi_0$ share the initial state $s$, 
  \item $\pi_0$ is an execution of $C_0$, and
  \item $\pi_1$ is an execution of $C_1$.
  \end{itemize}
  The transition swapping performed on $\pi$ for obtaining $\pi'$
  preserves the order that $\myexit^{C_0}_{p, \pi}$ appears before
  $\myenter^{C_0}_{q, \pi}$ on $\pi$ (by
  Assumption \ref{lema:seq:two:proof:a}).
  So $\pi_0 \vdash \neg\myaeval{\upsilon}_{C_0}(s, k)$ as long as
  $\pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k)$.  It
  contradicts the assumption that the triple of $C_0$ is valid.
  
\item[(1.2)] 
Since $C_0$ cannot be interfered by $C_1$, we can apply Lemma
\ref{lema:seq:reproduce} to a prefix of $\pi$ that ends with
$\myexit^{C_1}_{p, \pi}$.  It results in an extended execution $\zeta$
of $C_0$ such that $\zeta = \pi_0 \circ{} \xi_1$, where

\begin{itemize}
\item $\pi_0$ is an execution of $C_0$,
\item $\xi_1$ is a prefix of an execution of $C_1$, and $\mu$ and
  $\myallemptyguard$ hold for all processes on $\mysrc(\myhead(\xi_1))$,
  according to Lemma \ref{lema:seq:one}, and
\item $\upsilon \in_{\xi_1} \Upsilon_1$.
\end{itemize}
We show a contradiction to the validity of the triple of $C_1$ by
showing that $\upsilon$ is violated by $\xi_1$.
By Assumption \ref{lema:seq:two:proof:a}, process $q$ has not entered
$C_0$ while process $p$ exits $C_1$, i.e., $\myenter^{C_0}_{q, \pi}$
appears after $\myexit^{C_1}_{p, \pi}$ on $\pi$.  And by fact, 
$\myenter^{C_1}_{q, \pi}$ has to appear after
$\myenter^{C_0}_{q, \pi}$ on $\pi$.  Thus, no
$\myenter^{C_1}_{q, \zeta}$ in $\xi_1$, while by Lemma
\ref{lema:seq:reproduce}, $\xi_1$ includes $\myexit^{C_1}_{p, \zeta}$.
\end{enumerate}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Now considering Case 2.  We have
\begin{equation}
\upsilon =
\texttt{\acslguarantee{$p$}{$q$}{$r$}}. \tag{c}
\label{lema:seq:two:casetwo:c}
\end{equation}
By the $\nosendsubset(\Upsilon) \subseteq_\pi \Upsilon_0$ part of Side
Condition 2 of the sequence rule, we have
$\upsilon \in_\pi \Upsilon_0$.  We now have two sub-cases regarding to
the order of $\myexit^{C_0}_{p, \pi}$ and a transition $t_p$ on $\pi$,
where $\myproc(t_p) = p$ and $\myact(t_p) = $ \myactsend{$v$}{$q$} for
some $v$.  Note such $t_p$ must exist on $\pi$ because $\upsilon$ is
assumed to be violated on $\pi$.

\begin{itemize}
\item[2.1]
  \begin{equation}
    t_p \text{ appears before } \myenter^{C_0}_{r, \pi} \text{ and }
    \myexit^{C_0}_{p, \pi} \text{ on } \pi \tag{d}
    \label{lema:seq:two:casetwoone:d}
  \end{equation}

  Let us continue to consider the execution
  $\pi' = \pi_0 \circ{} \pi_1$ mentioned in Case 1.1.  Again, the
  transition swapping performed on $\pi$ to obtain $\pi'$ preserve
  the order that $t_p$ appears before $\myenter^{C_0}_{r, \pi}$ on
  $\pi$ (by Condition \ref{lema:seq:two:casetwoone:d}).  We have
  $\pi_0 \vdash{} \neg\myaeval{\upsilon}_{C_0}(s, k)$ as long as
  $\pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k)$ (Assumption
  \ref{lema:seq:two:proof:a}).  Contradicting the validity of the
  triple of $C_0$.

\item[2.2]
\begin{equation}
  t_p \text{ appears before } \myenter^{C_0}_{r, \pi} \text{ and after }
  \myexit^{C_0}_{p, \pi} \text{ on } \pi \tag{e}
  \label{lema:seq:two:casetwotwo:e}
\end{equation}
There are three further sub-cases according to Side Condition 2 of the
sequence rule.

\item[2.2.1] There is 
\begin{align}
\texttt{\acslwaitsfor{$p$}{$r$}} \in_\pi \Upsilon_0 \nonumber
\end{align}

This case can be proved contradicting to Assumption
\ref{lema:seq:two:casetwotwo:e} with the same idea as how was Case 2.1
proved.
  
\item[2.2.2] Considering the alternative $\pi' = \pi_0 \circ{} \pi_1$
  mentioned in Case 1.1.  There is
\begin{align}
\texttt{\acslwaitsfor{$x$}{$r$}} \in_\pi \Upsilon_0 \nonumber
\end{align}
and there is
\begin{align}
  \texttt{\acslguarantee{$p$}{$q$}{$x$}} \in_{\pi_1} \Upsilon_1 \nonumber
\end{align}

Since both the triples of $C_0$ and $C_1$ are valid, we
have 
\begin{align}
  &\myenter^{C_0}_{r, \pi_0} \text{ appears before } \myexit^{C_0}_{x, \pi_0} \text{ on } \pi_0, \tag{f} \label{lema:seq:two:casetwotwotwo:f}
\\
&\myenter^{C_1}_{x, \pi_1} \text{ appears before every such }
t_p' \text{ on } \pi_1 \text{ that }
\myproc(t_p') = p\wedge{}\myact(t_p') = \myact(t_p)\tag{g} \label{lema:seq:two:casetwotwotwo:g}
\end{align}
Transition swapping performed on $\pi$ for obtaining $\pi'$ preserves
the orders of the transitions given in Condition
\ref{lema:seq:two:casetwotwotwo:f} and
\ref{lema:seq:two:casetwotwotwo:g}.  Thus, we have
$\myenter^{C_0}_{r, \pi}$ appears before $t_p$ on $\pi$.
Contradicting Assumption \ref{lema:seq:two:proof:a} under Case 2.

\item[2.2.3] Considering the alternative $\pi' = \pi_0 \circ{} \pi_1$
  mentioned in Case 1.1.  There is
\begin{align}
 \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_{\pi_1} \Upsilon_1,\nonumber
\end{align}
where $r' = r \vee{} r' = q$.
A contradiction to Assumption \ref{lema:seq:two:proof:a} under Case 2
can be proved with the same idea used in Case 2.2.2.
\end{itemize}
$\qed$

%%%% SEQ LEMMA THREE

\begin{lema}
  Under the assumption made in Theorem \ref{lema:seq}, for an extended
  execution $\zeta$ with $n$ processes of $C_0C_1$, which starts from
  a pre-state of $C_0$ where $\psi$ and $\myallemptyguard$ hold for
  all processes, we have
  \begin{align}
    & \text{let } s = \mysrc(\myhead(\zeta)) \text{ in} \nonumber \\
    & \forall{p, q \in \nprocs{n}}.\,\, \myinterfere{\zeta}{C_0C_1}(p, q) \Rightarrow
      (\exists{k \in \nprocs{n}}. \zeta \vdash{} \neg{}\myaeval{\textup{$\Gamma$}}_{C_0C_1}(s, k)). \nonumber 
  \end{align}
  \label{lema:seq:three}
\end{lema}

\noindent\textbf{Proof}
Let $p, q, r \in \nprocs{n}$ be some processes.  Let
$s = \mysrc(\myhead(\zeta))$.  To prove by contradiction, we assume
that
\begin{align}
  & \myinterfere{\zeta}{C_0C_1}(p, q)~\wedge{}~
    \forall{k\in\nprocs{n}}. \zeta \vdash{} \myaeval{\textup{$\Gamma$}}_{C_0C_1}(s, k), \tag{a}
        \label{lema:three:proof:a}
  \end{align}
  for an ordered pair of processes $(p, q)$.  Without loss of
  generality, we further assume that
  
\begin{itemize}
\item $(p, q)$ is the only such order pair of processes that
  $\myinterfere{\zeta}{C_0C_1}(p, q)$, and
  
\item let $\rho_p$ and $\rho_q$ be the prefixes of $\zeta$ such that
  end with $\myexit^{C_1}_{p, \zeta}$ and $\myexit^{C_1}_{q, \zeta}$,
  respectively, we have
  $\mynsends{\rho_p}{p}{q} + 1 = \mynrecvs{\rho_q}{p}{q}$.
\end{itemize}
Then $\zeta$ must have the form
$\ldots{} \circ{} t_p \circ{} \ldots{} \circ{} t_q \circ{} \ldots{}$,
where

\begin{itemize}
\item $\myproc(t_p) = p$, $\myproc(t_q) = q$,
  $\myact(t_p) = $ \myactsend{$v$}{$q$} and
  $\myact(t_q) = $ \myactrecv{$v'$}{$p$} for some $v, v'$, and

\item $\mychan(\mysrc(t_p))(p, q) = \epsilon{}$, and
  
\item $t_p$ appears after $\myexit^{C_1}_{p, \zeta}$ and $t_q$ appears before
  $\myexit^{C_1}_{q, \zeta}$ on $\zeta$.
\end{itemize}
There are two cases for $\zeta$ with respect to the order of $t_q$ and
$\myexit^{C_0}_{q, \zeta}$ on $\zeta$:

\begin{itemize}
\item[1.] $t_q$ appears before
  $\myexit^{C_0}_{q, \zeta}$ on $\zeta$, and

\item[2.] $t_q$ appears after
$\myexit^{C_0}_{q, \zeta}$ and before $\myexit^{C_1}_{q, \zeta}$ on $\zeta$.
\end{itemize}
%% LEMMA:SEQ:THREE  PROVE FOR CASE 1
For Case 1, we have $\myinterfere{\zeta}{C_0}(p, q)$ because $\zeta$
is also a extended execution of $C_0$.  Then, by the assumption that
the triple of $C_0$ is valid, we have
\begin{align}
  & \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\zeta \Gamma_0 \tag{b} 
    \label{lema:three:proof:b}
\end{align}
such that $\zeta$ violates $\gamma$ for $C_0$.  By Side Condition 4 of
the sequence rule, there are two sub-cases.

\begin{enumerate}
\item[(1.1)] We have $\gamma \in_\zeta \Gamma$.  According to our
  construction of $\zeta$.  It contradicts Assumption
  \ref{lema:three:proof:a}.
  
\item[(1.2)] By our construction of $\zeta$, we can apply Lemma
  \ref{lema:seq:reproduce} to $\zeta$ to get an extended execution
  $\zeta'$ of $C_0$ such that $\zeta' = \pi_0' \circ{} \xi_1'$, where
  $\pi_0'$ is an execution of $C_0$ and $\xi_1'$ is an extended
  execution of $C_1$.  In this case,
  $\Upsilon_1~\rulecancels_{\zeta'}~\gamma_0$.  Consequently,
\[
  \upsilon = \texttt{\acslwaitsfor{$p$}{$x$}} \in_{\zeta'} \Upsilon_1,
\]
where $x = r \vee{} x = q$.  We need to show that $\upsilon$ is
violated by $\xi_1$ for a contradiction to the validity of the
collective triple of $C_1$.
  
Recall in our construction of $\zeta$,
  \begin{center}
  $t_p$ appears after
  $\myexit^{C_1}_{p, \zeta}$ and before $\myexit^{C_0}_{q, \zeta}$ on
  $\zeta$.
\end{center}
Consequently,
\begin{equation}
  \myexit^{C_1}_{p, \zeta} \text{ appears before }
  \myenter^{C_1}_{q, \zeta} \text{ on } \zeta. \tag{c}
  \label{lema:three:proof:c}
\end{equation}
Since the existence of $t_p$ leads to the violation of $\gamma$ by
$\zeta$ for $C_0$ (Assumption \ref{lema:three:proof:b}), $t_p$ appears
before $\myenter^{C_1}_{r, \zeta}$ on $\zeta$.  Consequently,
\begin{equation}
  \myexit^{C_1}_{p, \zeta} \text{ appears before } \myenter^{C_1}_{r, \zeta} \text{ on }
  \zeta. \tag{d}
  \label{lema:three:proof:d}
\end{equation}
Note that the order of
$\myexit^{C_1}_{p, \zeta}, \myenter^{C_1}_{q, \zeta}$ and
$\myenter^{C_1}_{r, \zeta}$ is preserved during the transition
swapping performed on $\zeta$.  Then, by Condition
\ref{lema:three:proof:c} and \ref{lema:three:proof:d}, we have that
$\upsilon$ is violated by $\xi_1'$ for $C_1$.
\end{enumerate}

%% LEMMA:SEQ:THREE  PROVE FOR CASE 2
Now we prove for Case 2.  Let us continue to consider the extended
execution $\zeta' = \pi_0' \circ{} \xi_1'$ used in Case 1.2.  

Under Case 2,
$\myinterfere{\xi_1'}{C_1}(p, q)$, because the order of $t_p$, $t_q$,
$\myexit^{C_1}_{p, \zeta}$ and $\myexit^{C_1}_{q, \zeta}$ is preserved
by the transition swapping performed on $\zeta$.  Then, since the
triple of $C_1$ is valid, there must be 
\[
  \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\xi_1'} \Gamma_1  \nonumber \\
 \tag{e}
    \label{lema:three:proof:e}
  \]
  s.t.\ $\gamma$ is violated by $\xi_1'$ for $C_1$.

  By Side Condition 4 of the sequence rule, we have
  \[
    \gamma \in_{\zeta'} \Gamma. \tag{f}     \label{lema:three:proof:f}
  \]
  Again, the order of $t_p$, $t_q$,
  $\myexit^{C_1}_{p, \zeta}, \myexit^{C_1}_{q, \zeta}$ and
  $\myexit^{C_1}_{r, \zeta}$ is preserved by transition swapping
  performed on $\zeta$ for obtaining $\zeta'$, we conclude that
\[
  \zeta \text{ has the form } \rho_0 \circ{} t_p \circ{} \rho_1 \circ{}
  t_q \circ{} \rho_2 
\]
s.t.\

\begin{itemize}
\item $\myexit^{C_1}_{p, \zeta} \in \mypathtrans(\rho_0)$, by
  construction of $\zeta$, and

\item
  $\myexit^{C_1}_{r, \zeta} \in \mypathtrans(\rho_1) \cup
  \mypathtrans(\rho'')$, by Condition \ref{lema:three:proof:e}, and

\item $\myexit^{C_1}_{q, \zeta} \in \mypathtrans(\rho_2)$, by
  construction of $\zeta$.
\end{itemize}
Thus, together with Condition \ref{lema:three:proof:f}, $\upsilon$ is
violated by $\zeta$. Contradicting Assumption
\ref{lema:three:proof:a}. $\qed$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{teom}[soundness of the consequence rule]
  Assuming the side conditions of the consequence rule over
  $\psi, \psi', \phi, \phi', \Gamma, \Gamma', \Upsilon$ and
  $\Upsilon'$ hold,
  \begin{center}
    $\model \models \cotriplenoloc$, if
    $\model \models \cocond{\psi', \Gamma'}~C~\cocond{\phi',
      \Upsilon'}$.
  \end{center}
  \label{lema:conseq}
\end{teom}

\noindent\textbf{Proof} Strengthening the state- or the path-requirement
cannot invalidate a valid collective triple.  Dually, weakening the
state- or the path-guarantee cannot invalidate a valid collective
triple. $\qed$ \param{}



\begin{teom}[soundness of the collective loop rule]
  Assuming the side condition of the collective loop rule holds, 
  \begin{center}
    $\model \models \cocond{\mymath{inv},\,\Gamma{}}~
    {\texttt{while(}c\texttt{)}~C} ~\cocond{\neg{}c \wedge{}
      \mymath{inv},\, \Upsilon{}}$, if
    $\model \models \cocond{\mymath{inv} \wedge{} c,\,
      \Gamma}~C~ \cocond{\mymath{inv},\,
      \Upsilon}$.
  \end{center}
  \label{lema:loop}
\end{teom}

\noindent\textbf{Proof}
Imagine unrolling the loop to a finite sequence $CC\ldots{}C$ of
length $m$. The validity of the original triple of the loop can be
proved by proving the following two tasks,

\begin{enumerate}
\item
  $\model \models{} \cocond{\mymath{inv} \wedge{} c,\,
    \Gamma}~CC\ldots{}C~ \cocond{\mymath{inv} \wedge{} c,\,
    \Upsilon}$, with the strengthened assumption
  $\model \models{} \cocond{\mymath{inv} \wedge{} c,
    \Gamma}~C~\cocond{\mymath{inv} \wedge{} c,
    \Upsilon}$, for the prefix $CC\ldots{}C$ of length $m-1$, and
  
\item
  $\model \models{} \cocond{\mymath{inv} \wedge{} c,
    \Gamma}~C~\cocond{\mymath{inv}, \Upsilon}$.
\end{enumerate}
Task 1 can be proved by repeatedly applying the sequence rule.
Task 2 is directly inferred by the assumption.
$\qed$


\begin{teom}[soundness of the elaboration rule]
\[
  \model \models \cotriplenoloc
\]
if
$
  \cocond{\psi{}}~\overrightarrow{C} \subseteq{}
  \overrightarrow{C_0C_1}
$
and
$
  \model \models \cocond{\psi{}, \Gamma}~{C_0}{C_1}~\cocond{\phi{}, \Upsilon}.
$
\label{lema:elab}
\end{teom}

\noindent\textbf{Proof}
According to the elaboration condition, for every execution $\pi$ of
$C$, there is an equivalent execution $\pi'$ of $C_0C_1$ such that
that both executions start from a same pre-state where $\psi$ holds.
The only difference between $\pi$ and $\pi'$ is that they have
different transitions in them that are all labeled by \texttt{skip},
which has no effect on neither the memory in state nor the order of
process executions.  So whenever $\pi'$ satisfies a specification,
$\pi$ satisfies the same specification. $\qed$ \param{}

