\section{Composite and Modular Verification for
  \minimp{}} \label{sec:minimp:system:symExeModular}

We have introduced a monolithic verification algorithm $\mcalgo$ in
\S\ref{sec:minimp:system:symExe} that is able to prove the validity of
a collective triple for a fixed number of processes.  In this section,
we improve $\mcalgo$ to $\mcalgo^{\Delta}$, which is a composite and
modular verification algorithm taking advantages from $\corule$.

Given a collective triple $\cotriplenoloc$ such that
$C = C_0C_1\ldots{}C_{m-1}$ or
$\cocond{\psi} \overrightarrow{C} \subseteq{}
\overrightarrow{C_0C_1\ldots{} C_{m-1}}$ for $m$ statement sequences
$C_0$, $C_1$, $\ldots{}$, $C_{m-1}$, $m > 0$.  We call a set of
collective triples a \emph{set of sequentially-decomposed triples} of
$C$, if the set contains a unique collective triple
$\mycosubtriple{i}{\psi_i}{\phi_i}{C_i}$ for each $C_i$,
$0 \leq{} i < m$.

Let $\textsf{Tri}$ be a subset of a sequentially-decomposed triple set
of $C$.  The algorithm $\mcalgo^{\Delta}$ verifies the validity of
$\cotriplenoloc$ by exploring feasible paths in a state space graph of
$C$ with the assumption that all triples in $\textsf{Tri}$ are valid.
During the verification, for each
$\mycosubtriple{i}{\psi_i}{\phi_i}{C_i} \in \textsf{Tri}, 0 \leq{} i <
m$, only the contract of $C_i$ is used to derive behaviors of $C_i$.

Intuitively, there is a gap between contract evaluation and semantics
of collective triple $\cotriplenoloc{}$: for an execution $\pi$ of
$C$, there is not necessarily a pair of pre- and post-states of a
$C_i, 0 \leq{} i < m$, exist in $\pi$.  In such cases, where is the
contract of $C_i$ suppose to be evaluated?  We propose a solution to
this problem using \emph{collective states} in
\S\ref{subsec:collective:state}.  The algorithm $\mcalgo^{\Delta}$ is
based on collective states and is described in
\S\ref{subsec:modular:algorihtm}.

In this section, we fix our context with the collective triple
$\cotriplenoloc{}$ and the subset $\textsf{Tri}$ of a
sequentially-decomposed triple set of $C$.

%%%%%%%%%%%%%%%% COLLECTIVE STATES %%%%%%%%%%%%%%%%%%%
\subsection{Collective States} \label{subsec:collective:state}

A \emph{collective state} is a state where every process is at a
desired location as if there is a ``bulk-synchronous'' at each of the
location.

\begin{defn}
Let $n$ be a positive integer.  Let $\textsf{Loc}$ be the set of
locations in $\model$.  Let $\textsf{myloc}\colon{} \nprocs{n}
\rightarrow{} \textsf{Loc}$ be a function that maps integers in
$\nprocs{n}$ to locations.  Let $\rho$ be a path such that for every
process $p \in \nprocs{n}$, $\exists{\omega \in
  \mypathstates(\rho)}.\, \mytoploc(\omega, p) = \textsf{myloc}(p)$.
A state $\omega'$ is a collective state associated with $\rho$ and
$\textsf{myloc}$, if it satisfies the following condition:
\[
\forall{p\in\nprocs{p}}.\exists{\omega \in \mypathstates(\rho)}.\, \myprocState_p(\omega') =
\myprocState_p(\omega) \wedge{} \mytoploc(\omega', p) = \textsf{myloc}(p). \qed
\]
\end{defn}

Our interest actually focuses on certain kinds of collective states,
the \emph{collective pre-} and \emph{post-states}.  They are the
collective states where processes are at entry and exit, respectively,
of a particular substatement.

Let $\pi$ be an execution of $C$.  We are interested in the pre- and
post-states of $C_i$, ($0 \leq{} i < m$), associated with $\pi$, if
$\mycosubtriple{i}{\psi_i}{\phi_i}{C_i} \in \textsf{Tri}$.  The
process state of a process $p$ in the collective pre-state of $C_i$
will be equivalent to $\myprocState(\mysrc(\myenter^{C_i}_{p,
  \pi}))$. Similarly, the process state of $p$ in the collective
post-state of $C_i$ will be equivalent to
$\myprocState(\mydest(\myexit^{C_i}_{p, \pi}))$.  Recall $\myenter$
and $\myexit$ are defined in \S\ref{sec:extended:enter:exit}.


The value of the message channels in the collective pre-state (resp.\
post-state) of $C_i$ associated with $\pi$ follows an observation.
Suppose that there is a ``bulk-synchronous'' barrier at the entry
(resp.\ exit) of $C_i$.  Let $\pi'$ be an execution of such $C$ that
contains the barrier and the sub-statement $C_i$.  Let $\omega$ be the
state in $\pi'$ where all processes are blocked by the barrier.  The
message channels in $\omega$ depends and only depends on the
transitions that appear before $\omega$ and are labeled by a send or a
receive action.

Such an observation will be generalized by a precise definition for
collective states.

\begin{defn}
Let $\pi$ be an execution of $C$.  By $\mycspre{\pi}{C_i}$, we denote
the collective pre-state of $C_i$ associated with $\pi$; by
$\mycspost{\pi}{C_i}$, we denote the collective post-state of $C_i$
associated with $\pi$. $\qed$
\end{defn}

\begin{defn}
 Let $\pi$ be an execution of $C$. A transition $t$ is said to
  \emph{be depended on by the message channels} of the collective
  state $\mycspre{\pi}{C_i}$ (resp.\ $\mycspost{\pi}{C_i}$), if
  
  \begin{enumerate}
  \item $t \in \mypathtrans(\pi)$,
    
  \item $\myact(t)$ is either a send or receive action, and
  \item $t$ appears before $\myenter^{C_i}_{\myproc(t), \pi}$ (resp.\
    $\myexit^{C_i}_{\myproc(t), \pi}$) on $\pi$. $\qed$
  \end{enumerate}
\end{defn}

\begin{defn}
Let $\pi$ be an execution of $C$.  Let $\rho$ be a subpath of $\pi$.
We use the procedure $\myCoChanPre(\omega, \rho, \pi, C_i)\colon{} \mystates^{\sym}$ to
describe the state that is obtained by updating the message channel
function in the given state $\omega$ with respect to the transitions
in $\rho$, on which $\mycspre{\pi}{C_i}$ depends:
  \begin{align}
    &    \myCoChanPre(\omega, \rho, \pi, C_i) = \nonumber \\
    &    \text{let } t = \myhead(\rho) \text{ in} \nonumber \\    
    &    \text{let } p = \myproc(t) \text{ in} \nonumber \\
    &    \text{let } \rho = t \circ{} \rho', \text{if } \rho \not=
      \epsilon, \text{ in} \nonumber \\
    &    \begin{cases}
      \omega, & \text{if }\rho = \epsilon \\
      \myCoChanPre(\omega, \rho', \pi, C_i), &\text{if }
      \mycspre{\pi}{C_i}  \text{ not depends on } t\\
      \myCoChanPre(\omega[\enque{(p, q)}{v}], \rho', \pi, C_i), & \text{if } \myact(t) =
      \myactsend{$v$}{$q$} \\
      \myCoChanPre(\omega[\deque{(q, p)}{v}], \rho', \pi, C_i) & \text{if } \myact(t) =
      \myactrecv{$v$}{$q$} 
    \end{cases} \nonumber
  \end{align}
  Similar for $\myCoChanPost$, whose definition is omitted here for
  brevity. $\qed$
\end{defn}

\begin{defn}
  Let $n$ be a positive integer and $\pi$ an execution with $n$
  processes of $C$.  A collective pre-state $\mycspre{\pi}{C_i}$ of
  $C_i$ associated with $\pi$ is defined by
  \begin{align}
    &\textbf{process states:}  \nonumber \\
                    &~~~~\forall{p \in \nprocs{n}}.\,
                      \myprocState(\mycspre{\pi}{C_i}, p)
                      = \myprocState(\mysrc(\myenter^{C_i}_{p, \pi}), p)
                      \nonumber \\
    &\textbf{message channels:}  \nonumber \\                 
                    &~~~~ \mychan(\mycspre{\pi}{C_i}) =
                      \mychan(\myCoChanPre(\mysrc(\myhead(\pi)), \pi, \pi, C_i))
                      \nonumber \\
    &\textbf{path condition:}  \nonumber \\
                    &~~~~ \mypathcond(\mycspre{\pi}{C_i}) =
                      \bigwedge\limits_{p \in{}
                      \nprocs{n}}\mypathcond(\mysrc(\myenter^{C_i}_{p,
                      \pi})) \nonumber
  \end{align}
  The definition of the collective post-state $\mycspost{\pi}{C_i}$ is
  similar to above.  Hence we omit it for brevity. $\qed$
  \label{defn:collective:state}
\end{defn}

Message channels of the collective pre-state $\mycspre{\pi}{C_i}$
actually can be represented in many different ways since for any state
$\omega$ that appears before the first $\myenter^{C_i}_{p, \pi}$ for
some $p \in \nprocs{n}$ on $\pi$, the message channels of $\omega$
depend on all the transitions labeled by communication actions.  Hence
one can still obtain the correct message channels by applying the
$\myCoChanPre$ procedure on $\omega$ and the suffix of $\pi$ emanating
from $\omega$.  In practice, it is the most efficient to do
\[
  \myCoChanPre(\mysrc(\myhead(\rho)), \rho, \pi, C_i), 
\]
where $\rho$ is defined as the minimal sub-path of $\pi$ such that
$\forall{p \in \nprocs{n}}.\, \myenter^{C_i}_{p, \pi} \in
\mypathtrans(\rho)$.

\begin{exmp}
  Figure \ref{fig:minimp:example:collective:state} shows a collective
  pre-state (upper right) of a statement $C_1$ associated with an
  execution (below) of a \minimp{} code $C_0C_1$ (upper left), where
  $C_0$ is a statement sequence at line 4-5 and $C_1$ is a statement
  sequence at line 6-7.  The collective state depends on the process
  states in state 4, 6 and 7.  The value of the message channels in
  the collective state is initialized by the one in state 4, where the
  message channels from 0 to 1 and from 1 to 2 are non-empty.  After
  state 4, communication actions performed by process 1 and 2 can
  still affect the collective state.  From state 5, process 1
  \texttt{recv}s a message from process 0.  It causes the message
  channel from 0 to 1 in collective state to be updated to empty.
  After state 6, only process 2 can affect the collective state.  From
  state 6, process 2 \texttt{recv}s a message from process 1.  The
  message channels in the collective state eventually are updated to
  all empty.  $\qed$
  \label{exmp:collective:state}
\end{exmp}


\begin{figure}[h]
  \begin{minipage}{.45\textwidth}
    \begin{programSmall}
      \ccode{var} dat = \ccode{new} [2]; \\
      \ccode{var} r = (PID + 1) \% NPROCS; \\
      \ccode{var} l = (PID + NPROCS - 1) \% NPROCS; \\
      send(dat[PID], r);\\
      recv(dat[r], r);\\
      send(dat[PID], l);\\
      recv(dat[l], l);\\
      ...\
    \end{programSmall}
  \end{minipage}
  \begin{minipage}{.45\textwidth}
    \includegraphics[scale=.30]{collective_state}
  \end{minipage}
  
  \hrulefill

  \vspace{-1cm}
  \begin{center}
    \includegraphics[scale=.37]{exec}
  \end{center}
    \vspace{-1cm}
    \caption{A collective state (upper right) associated with an
      execution (below) of a \minimp{} program (upper left).  All
      processes are collectively at line 6 in the collective state.}
  \label{fig:minimp:example:collective:state}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%% MODULAR ALGORITHM %%%%%%%%%%%%%%
\subsection{The Composite and Modular Verification Algorithm}\label{subsec:modular:algorihtm}
We talk about the composite and modular algorithm $\mcalgo^{\Delta}$
in this subsection.

\begin{defn}
 \[
 \mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}}, n) =
 \textbf{T}
 \] iff 
 \[\model \models \cotriplenoloc{} \text{ and }
 \forall{\textsf{tri} \in \textsf{Tri}}.\, \model \models
 \textsf{tri}. \qed
  \]  
\end{defn}

We describe $\mcalgo^{\Delta}$ by illustrating the differences between
$\mcalgo$ and itself.

First, besides the atomic statements defined in
\S\ref{sec:minimp:semantics}, we add a new atomic statement
$\myactrefresh{}$ for $\mcalgo^{\Delta}$.  The statement means to
assign ``fresh new'' (i.e., unique and unconstrained) symbols to all
\emph{visible} variables to a process.  

\begin{defn} The semantics of $\myactrefresh$ is defined by
\begin{align}
  &  I^{\sym}(\omega, p, (l, g, \myactrefresh{}, l')) = \nonumber \\
    & \text{let } f \text{ be the procedure associated with }
    \mytop(\omega, p) \text{ in} \nonumber \\
  & \text{let } \{X_0, X_1, \ldots{} \} \text{ be an infinite set of
    symbols that are  fresh new to } \omega \text{ in} \nonumber \\
  & \text{let } \{v_0, v_1, \ldots{}, v_{m-1}\} \text{ be union of }
    \globvar{} \cup{} \locvar(f)
    \text{ in} \nonumber \\
  & \text{let } \textsf{pc} = \mypathcond(\omega) \text{ in} \nonumber
  \\
  &
    \{\omega[\textsf{pc:= }\textsf{pc} \wedge{} \myeval{g}(\omega, p)][v_0 \leftarrow{} X_0, v_1 \leftarrow{} X_1, \ldots{},
    v_{m-1} \leftarrow{} X_{m-1}]_p\} \qed \nonumber
\end{align}
\end{defn}
Let $\myactrefresh{}$ also be an atomic action.  So we have $\myact(t)
= \myactrefresh$, if given a global transition $t = (\omega, p, (l, g,
\myactrefresh{}, l'), \omega)$.


We then modify the translation procedure $\transT$ to
$\transT_{\textsf{Tri}}$, which translates $C$ to a set of local
transitions such that, for any
$\mycosubtriple{i}{\psi_i}{\phi_i}{C_i} \in \textsf{Tri}$, the
translation result excludes the detail of $C_i$.

\begin{defn}
The translation procedure $\transT_{\textsf{Tri}}$ is defined by

\begin{itemize}
  \item[] $\transT_{\textsf{Tri}}(l, C_i) =$
  \begin{itemize}
  \item $(l + 1, (l, \texttt{true}, \myactrefresh{}, l + 1))$, 
    if  $\exists{}\mycosubtriple{i}{\psi_i}{\phi_i}{C_i} \in
    \textsf{Tri}$
  \item $\transT(l, C_i)$, if $C_i$ is an assignment, a return, a
    call, or a communication statement.
  \item apply $\transT_{\textsf{Tri}}$ to substatements of $C_i$
    recursively, otherwise. $\qed$
  \end{itemize}
\end{itemize}
\end{defn}
Intuitively, the \texttt{refresh} statement can be seen as an
operation for making the weakest over-approximation of the behaviors
of a sub-statement of $C$.

While the weakest over-approximation can barely be useful, we want the
approximation of $C_i$ to reflect the contract.  We shall assume that
$\phi_i$ and $\myallemptyguard$ hold on the collective post-state
$\mycspost{\pi}{C_i}$, if $\phi_i$ and $\myallemptyguard$ hold on the
collective pre-state $\mycspre{\pi}{C_i}$.  In addition, we assume
that the path-guarantee $\Upsilon_i$ is satisfied by every execution
of $C$.  Technically, an execution is infeasible if these assumptions
fail to hold on it.

%%%%%%%%%%%%%%%%%%%% DEFN %%%%%%%%%%%%%%%%%%%%%
\begin{defn}
  Let $n$ be a positive integer.
  For the collective triple $\cotriplenoloc{}$ and the triple set
  $\textsf{Tri}$, the state space graph $G$ searched by
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}}, n)$
  is a tuple:
  \[
  (\omega_0, \Omega, \leadsto^{\sym, \Delta}_C),
  \]
  where

  \begin{itemize}    
  \item $\omega_0$ is a initial state that satisfies the following
    conditions
    
    \begin{enumerate}
    \item $\omega_0$ is a pre-state of $C$,
      
    \item for every $p\in\nprocs{n}$ and every $v \in \var$,
      $\mymem(\omega_0, p)(v)$ is a unique symbolic constant, and
      
    \item $\mypathcond(\omega_0) =
      \bigwedge\limits_{p\in\nprocs{n}}\myeval{\psi}(\omega_0, p)$,
      and $\myallemptyguard$ holds for all processes on $\omega_0$.
    \end{enumerate}
    
  \item $\Omega$ is the set of states that are reachable from
    $\omega_0$ over $\transT_{\textsf{Tri}}(l, C)$ for some location
    $l$, and
  \item $\leadsto^{\sym, \Delta}_C$ is the set of global transitions
    \[
      \{ (\omega, p, a, \omega') \mid{} \omega' \in
      I^{\sym}(\omega, p, \alpha), p \in \nprocs{n}, \omega{} \in
      \Omega, \alpha{} \in \transT_{\textsf{Tri}}(l, C)\}
    \qed \]
  \end{itemize}
\end{defn}

We define whether an execution explored by
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}}, n)$
is feasible with respect to the contracts of triples in \textsf{Tri}.

\begin{defn}
  Let $G$ be the state space graph searched by
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}},
  n)$.  An execution $\pi$ in $G$ is \emph{infeasible}, if one of the
  following conditions holds.
  
  \begin{enumerate}
  \item There is a state $\omega \in \mypathstates(\pi)$ such that
    $\mypathcond(\omega) = \textbf{F}$
    
  \item There is
    $\mycosubtriple{i}{\psi_i}{\phi_i}{C_i} \in \textsf{Tri}$ such that
    
    \begin{enumerate}
    \item  $\exists{p \in \nprocs{n}}.\,
      \myseval{\phi_i}(\mycspost{\pi}{C_i}, p) = \textbf{F}$, or
      
    \item
      $\forall{p \in
        \nprocs{n}}.\pi \vdash{} \neg \myaeval{\textup{$\Upsilon$}}_{C_i}(\mycspre{\pi}{C_i}, p)$
    \end{enumerate}
  \end{enumerate}
  The execution $\pi$ is \emph{feasible} if it is not
  \emph{infeasible}.  $\qed$
  \label{defn:modular:verification:infeasible}
\end{defn}
In fact, Condition 2.b in Def.\
\ref{defn:modular:verification:infeasible} can be strengthened to
\[
  \forall{p\in\nprocs{n}}.\pi \vdash{} \neg\myaeval{\textup{$\Upsilon$}}_{C_i}(\mycspre{\pi}{C_i}, p),
\]
where $\Lambda$ is the expression representing the set-subtraction of
the absence assertion sets represented by $\Upsilon$ and
$\nosendsubset(\Upsilon)$, respectively.  Because details of $C_i$ has
been abstracted to $\myactrefresh{}$.  Consequently, for
$\nosendsubset(\Upsilon)$, $\myaeval{~}_{C_i, \pi}$ can only evaluate
it to true.


%%%%%%%%%%%% Extend in_pi %%%%%%%%%%%%%%%
For an execution in the state space graph searched by
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}}, n)$,
there is at most one collective pre-state (resp.\ collective
post-state) of $C_i$, which is specified by a triple in
$\textsf{Tri}$.  Because recursions of $C_i$ have been abstracted away
in the execution.

Therefore, we can extend the set-operation $\in_{\rho}$ associated
with a path $\rho$ over absence assertions that are suppose to be
evaluated on collective states.

\begin{defn}
  Let $\pi$ be a feasible execution in the state space graph searched
  by $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}},
  n)$.  Let $C_i$ be a substatement of $C$ such that $\cosubtriple{i}
  \in \textsf{Tri}$.  Let $e$ be an expression and $\Gamma_i$ be of
  the form $e \texttt{ ==> } \gamma_0 \texttt{ \&\& } \ldots{}
  \texttt{ \&\& } \gamma_{m-1}$.  For an absence assertion $\lambda$,
  \[
    \lambda \in_\pi \Gamma_i \text{ iff }
    \exists{i \in \nprocs{m}}.\,\exists{p\in\nprocs{n}}.\,
    \lambda =
      \mypeval{\gamma_i}{\mycspre{\pi}{C_i}}{p}.
    \]
    Similar for $\lambda \in_\pi
    \Upsilon_i$. $\qed$
\end{defn}

%%%%%%%%%%%% Error Path Definition %%%%%%%%%%%%
The algorithm $\mcalgo^{\Delta}$ returns \textbf{F} if there is a
feasible execution in the searching space that violates a contract or
contains a deadlock.

\begin{defn}
  Given a feasible execution $\pi$ in the state space graph searched
  by $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}},
  n)$, $\pi$ violates a contract or contains a deadlock, denoted $\pi
  \not\models^{\Delta} \cotriplenoloc{}$, if $\pi \not\models
  \cotriplenoloc{}$ or one of the cases defined in
  Fig.\ \ref{fig:modular:verify:error} describes $\pi$.$\qed$
  \label{defn:modular:verify:error}
\end{defn}

\begin{figure}
\begin{center}  
\fbox{
  \parbox{.92\textwidth}{
    \begin{align}
      \text{suppose } & i < j \text{ and } \mycosubtriple{i}{\psi_i}{\phi_i}{C_i},
      \mycosubtriple{j}{\psi_j}{\phi_j}{C_j} \in \textsf{Tri},  \nonumber \\
      \textbf{SRV}, &(\text{\textbf{s}tate
                               \textbf{r}equirement
                               \textbf{v}iolation}): \nonumber \\
                   &\bigwedge\limits_{p \in \nprocs{n}}
                   \myseval{\myallemptyguard{} \texttt{ \&\& }
                   \psi_i}(\mycspre{\pi}{C_i}, p) = \textbf{F} \nonumber
      \\
  %%%
      \textbf{PRV}, &(\text{\textbf{p}ath \textbf{r}equirement
                             \textbf{v}iolation}): \nonumber \\      
                   &\exists{p\in\nprocs{n}}. \pi{} \vdash{} \neg\myaeval{\textup{$\Gamma$}}_{C_i}(\mycspre{\pi}{C_i}, p) \nonumber \\
  %%%
      \textbf{PRV-II}&:\nonumber \\
                      &       \exists{p,  q, r, r'\in \nprocs{n}}.\nonumber \\
      \exists{}& \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_i.
                                       \nonumber \\
      \neg\exists{}& \texttt{\acslgamma{$p$}{$q$}{$r'$}} \in_\pi \Gamma. \nonumber
      \\
      \myexit^{C}_{p, \pi} & \text{ appears
                       before } \myexit^{C_i}_{r, \pi} \text{ on } \pi
         ~\wedge{}~\myexit^{C_i}_{r, \pi} \text{ appears
                        before } \myexit^{C}_{r', \pi} \text{ on }
                        \pi \nonumber \\
                        %%%% 
      \textbf{PRV-III}&: \nonumber \\
                             &    \exists{p, q, r, r' \in \nprocs{n}}.\nonumber \\
     \exists{} & \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_i.
                                      \nonumber \\
     \neg\exists{} & \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_\pi \Upsilon_j.
                                                   \nonumber \\
      \myenter^{C_j}_{p, \pi} & \text{ appears before }
        \myexit^{C_i}_{r, \pi} \text{ on } \pi ~\wedge{}~\myexit^{C_i}_{r, \pi} \text{ appears before }
        \myenter^{C_j}_{r', \pi} \text{ on } \pi \nonumber\\
  %%%%%%%%%             %%%%
      \textbf{ITF-II} &: \nonumber \\
                      & \exists{t} \in
                        \mypathtrans(\pi).\,\exists{p, q, r \in \nprocs{n}}.\,\nonumber\\
                      \neg\exists{}&\texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon_i.\nonumber \\
                      &\mayInterfere^{\Delta}_G(\mysrc(t), p, q)~\wedge{}~
                      \myenter^{C_i}_{p, \pi} \text{ appears
                        before } t \text{ on } \pi \wedge{}
                        \nonumber\\
                      &t \text{ appears
                        before } \myenter^{C_i}_{r,
                        \pi}  \text{ on } \pi,
                        \nonumber\\      
                      &\text{where for some } v, \mayInterfere^{\Delta}_G(\omega,
                        p, q) = \mychan(\omega)(p, q) =
                        \epsilon{} \wedge{}\nonumber\\
                      &\exists{t_q \in \emana_G(\omega)}.\,
                       \myact(t_q) =
                        \texttt{recv($v$, $p$)} \wedge{} \myproc(t_q)
                          = q \nonumber\\ 
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      \textbf{PGV-II} &:\nonumber\\
                             & \exists{p, q, r, r'\in \nprocs{n}}. \nonumber \\
      \exists{}&\texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon.
                                      \nonumber    \\
      \neg\exists{}&\texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_\pi \Upsilon_i.
                                       \nonumber    \\
                            \myenter^{C_i}_{p, \pi}&\text{
                               appears before } \myenter^{C}_{r,
                               \pi} \text{ on } \pi
                             ~\wedge{}~ \myenter^{C}_{r, \pi} \text{
                               appears before } \myenter^{C_i}_{r',
                               \pi} \text{ on } \pi \nonumber
\end{align}
}}
\caption{Conditions of a contract violation of an execution $\pi$
  explored by $\mcalgo^{\Delta}(\model,
  \frac{\textsf{Tri}}{\cotriplenoloc{}}, n)$.}
\label{fig:modular:verify:error}
\end{center}
\end{figure}


We explain the conditions in Fig.\ \ref{fig:modular:verify:error} for
Def.\ \ref{defn:modular:verify:error}.  Given $C =
C_0\ldots{}C_i\ldots{}C_j\ldots{}$ or $\overrightarrow{C} \subseteq
\overrightarrow{C_0\ldots{}C_i\ldots{}C_j\ldots{}}$, suppose there are
collective triples $\mycosubtriple{i}{\psi_i}{\phi_i}{C_i}$ and
$\mycosubtriple{j}{\psi_j}{\phi_j}{C_j}$ in \textsf{Tri}.

\begin{itemize}
\item{} The \textbf{SRV} describes the violation that the
  state-requirement of $C_i$ fails to hold on a collective pre-state
  of $C_i$.

\item The \textbf{PRV} describes the violation of the path-requirement
  $\Gamma_i$ of $C_i$.

\item The \textbf{PRV-II} describes the violation of the
  path-requirement $\Gamma_i$ of $C_i$ in an execution \textbf{in the
    state space graph of $C$} due to weakness of the path-requirement
  $\Gamma$ of $C$.  The weakness can cause $C_i$ be interfered by a
  statement following $C$.  Remark that this is a violation that can
  happen in the state space graph of $C$ instead of where
  $\mcalgo^{\Delta}$ searches.

\item The \textbf{PRV-III} describes the violation of the
  path-requirement $\Gamma_i$ of $C_i$ in an execution \textbf{in the
    state space graph of $C$} due to the weakness of the path
  guarantee $\Upsilon_j$ of $C_j$.  The weakness can cause $C_i$ be
  interfered by $C_j$.

\item The \textbf{ITF-II} describes the violation that a sub-statement
  $C_k$ of $C$ such that $k < i$ can be interfered by $C_i$ due to the
  weakness of the path guarantee of $C_i$.  Remark that
  $\mayInterfere^{\Delta}_G$ is in fact a weaker predicate than
  $\mayInterfere_G$.

\item Finally, the \textbf{PGV-II} describes the violation of the path
  guarantee of $C$ in an execution \textbf{in the state space graph of
    $C$} due to the weakness of the path guarantee of $C_i$.
\end{itemize}

We remark that the algorithm $\mcalgo^{\Delta}$ assumes that every
collective-style statement sequence specified by a triple in
$\textsf{Tri}$ is invoked collectively.  Of course, a sound
verification system should be able to detect invalid invocations of
collective style statement sequences.  This is actually one of the
reasons why we implemented a contract system on the basis of procedure
contracts.  It is natural to detect unmatched collective procedure
calls.  We talk about building such a contract system in
\S\ref{sec:minimp:modular:system}.

Finally, the soundness of $\mcalgo^{\Delta}$ is proved in
\S\ref{sec:minimp:modular:proof}.