In this section, we introduce a specification language \minispec{} for
\minimp{} programs.  A \minispec{} specification specifies partial
correctness properties for a \minimp{} \emph{substatement}.  Inspired
by Hoare logic, as well as Lamport's ``Hoare Logic'' for concurrent
programs \cite{lamport:1980:hoare}, we invented an abstract
representation, called a \emph{collective triple}, for a \minimp{}
substatement with its specification.  When it is clear in the
context, we may use ``triple'' to refer ``collective triple'' for
brevity.

This chapter is structured as the follow.
\S\ref{sec:minimp:spec:progseg} describes an abstract representation,
called \emph{program segment}, of a \minimp{} substatement.
\S\ref{sec:minimp:spec:path} talks about the notion of \emph{path
  predicates}. Syntax of \minispec{} is given in
\S\ref{sec:minimp:spec:syntax}.  Semantics of \minispec{} with respect
to a \minimp{} program segment is described in
\S\ref{sec:minimp:spec:semantics}.  Finally, we define the meaning of
that a \minimp{} substatement satisfies a specification using
collective triples in \S\ref{sec:minimp:spec:triple}.

\section{Program Segment} \label{sec:minimp:spec:progseg}

In \minimp{}, the body of a procedure is a statement.  To refer to a
segment of a procedure body, we give the intuitive term,
\emph{substatement}, a precise definition.

\begin{defn}
  Let $\vocab{}$ be a vocabulary, $i, j , m$ be integers such that
  $0 \leq i \leq j < m$, and $\psi \in \bexprv_{\vocab{}}$. Given a
  \minimp{} \nonterm{Statement} $C$, a \emph{substatement} of $C$ is
  defined inductively by
  \begin{align}
    \texttt{\lb{}$C_iC_{i+1}\ldots{}C_j$\rb{}} &
                                                 \text{, if } C \text{ matches }
                                                 \texttt{\lb{}$C_0C_1\ldots{}C_m$\rb{}}  \nonumber \\
    C, C_0 \text{ or } C_1 &   \text{, if } C \text{ matches }
                          \texttt{\ccode{if} ($\psi$) } C_0
                             \texttt{\ccode{ else }} C_1 \nonumber \\
    C \text{ or } C_0 &   \text{, if } C \text{ matches }
                          \texttt{\ccode{while} ($\psi$) } C_0
                        \nonumber   \\
    C& \text{, otherwise.} \qed \nonumber
  \end{align}
\end{defn}
Note that a substatement is also a \nonterm{Statement}.

A \emph{program segment} is an abstract representation of a
substatement of a \minimp{} \nonterm{Statement}.

\begin{defn}
  Let $\vocab{} = (\myprocedure, \var, \globvar, \locvar)$ be a
  vocabulary and $\model = (\texttt{main}, \textsf{pg})$ be a
  \minimp{} model.  Let $C$ be a substatement of the body of a
  procedure $f$ in $\model$ such that there is no
  \texttt{\ccode{return}} substatement of $C$.  A \emph{program
    segment} of $C$, denoted $\progseg{l}{C}{l'}$, is a tuple
  \begin{center}
    $(\myloc{}, l, l', T)$,
  \end{center}
  where
  
  \begin{itemize}
  \item $\myloc{}$ is a set of program locations,
  \item $l \in \myloc{}$ is the sole entry location of $C$,
  \item $l' \in \myloc{}$ is the sole exit location of $C$, and
  \item $T$ is a set of local transitions such that
    $(l', T) = \transT(l, C)$ and $T$ is a subset of the location
    transition set of $\textsf{pg}(f)$.   $\qed$
  \end{itemize}
\end{defn}


\begin{exmp}
  A program segment associated to the loop \nonterm{Statement} of the
  \texttt{bcast} procedure (line 5-9) in Fig.\
  \ref{fig:minimp:example:bcast} is given by the follow
  \begin{center}
    ($\{2, \ldots{}, 9\}$, $2$, $9$, $T$),
  \end{center}
  where $T = \{$
  
        \begin{tabular}{ll}
      $(2,\, \textcolor{red}{\texttt{i < NPROCS}},\, \myactskip,\, 3),$
         &
      $(3,\, \textcolor{red}{\texttt{i != root}},\, \myactskip,\, 4),$ \\
      $(4,\, \textcolor{red}{\texttt{true}},\, \texttt{\send{dat}{i}},\, 5),$ &
      $(5,\, \textcolor{red}{\texttt{true}},\, \myactskip,\, 7),$
         \\
      $(3,\, \textcolor{red}{\texttt{i == root}},\,
           \myactskip,\, 6),$ &
      $(6,\, \textcolor{red}{\texttt{true}},\, \myactskip,\,
      7),$\\
      $(7,\, \textcolor{red}{\texttt{true}},\, \texttt{i = i + 1},\,
                8),$&
      $(8,\, \textcolor{red}{\texttt{true}},\, \myactskip,\,
      2),$ \\
       $(2,\, \textcolor{red}{\texttt{i >= NPROCS}},\, \myactskip,\,
      9),$&
        \end{tabular}
        
        $\}$

        Figure \ref{fig:program:segment:visual} visualizes the program
        segment.  The visualization makes it clear that the program
        segment is a sub-graph of the one of \texttt{bcast} given in
        Fig.\ \ref{fig:exmp:func-graph}.  $\qed$
\end{exmp}

\begin{figure}
  \usetikzlibrary{shapes.geometric, arrows}
  \tikzstyle{loc} = [rectangle, minimum width=.7cm, minimum
  height=.7cm,text centered, draw=black]
    \tikzstyle{end} = [rectangle, minimum width=.7cm, minimum
    height=.7cm,text centered, draw=black, thick]
    \tikzstyle{arrow} = [thick,->,>=stealth]
    \centering
  \begin{tikzpicture}[node distance=2cm]
    \node (l2) [end, right of=l1, xshift=.6cm] {$2$};
    \node (l3) [loc, right of=l2, xshift=1.5cm] {$3$};
    \node (l4) [loc, right of=l3, xshift=1.5cm] {$4$};
    \node (l5) [loc, below of=l4, yshift=-.5cm] {$5$};
    \node (l6) [loc, below of=l3, yshift=-.5cm] {$6$};
    \node (l7) [loc, below of=l5, yshift=-.5cm] {$7$};
    \node (l8) [loc, below of=l6, yshift=-.5cm] {$8$};
    \node (l9) [end, below of=l2, yshift=-.5cm] {$9$};
    %% arrows
    \draw [arrow] (l2) -- node[anchor=south]{\textcolor{red}{\texttt{i
          < NPROCS}}}
    node[anchor=south, yshift=-.55cm]{$\myactskip{}$}
    (l3);

    \draw [arrow] (l3) -- node[anchor=south]{\textcolor{red}{\texttt{i
          != root}}}
        node[anchor=south, yshift=-.55cm]{$\myactskip{}$}
    (l4);

    \draw [arrow] (l4) --
    node[anchor=east, yshift=.3cm]{\textcolor{red}{\texttt{true}}}
    node[anchor=east, yshift=-.25cm]{\texttt{\send{dat}{i}}}
    (l5);

    \draw [arrow] (l5) --
    node[anchor=east, yshift=.3cm]{\textcolor{red}{\texttt{true}}}
    node[anchor=east, yshift=-.25cm]{$\myactskip$}
    (l7);

    \draw [arrow] (l3) -- node[anchor=east, yshift=.3cm]{\textcolor{red}{\texttt{i
          == root}}}
    node[anchor=east, yshift=-.25cm]{$\myactskip$}
    (l6);

    \draw [arrow] (l6) --
    node[anchor=east, yshift=.1cm]{\textcolor{red}{\texttt{true}}}
    node[anchor=east, yshift=-.45cm]{$\myactskip$}
    (l7);

    \draw [arrow] (l7) --
    node[anchor=south]{\textcolor{red}{\texttt{true}}}
    node[anchor=south, yshift=-.55cm]{\texttt{i = i + 1}} (l8);
    
    \draw [arrow] (l8) --
node[anchor=east, yshift=.2cm]{\textcolor{red}{\texttt{true}}}
    node[anchor=east, yshift=-.35cm]{$\myactskip$}
    (l2);

    \draw [arrow] (l2) -- node[anchor=east, yshift=.3cm]{\textcolor{red}{\texttt{i
          >= NPROCS}}}
    node[anchor=east, yshift=-.25cm]{$\myactskip$}
    (l9);
  \end{tikzpicture}
  
  \caption{The program segment of the loop \nonterm{Statement} in the
    \texttt{bcast} procedure showed in Fig.\
    \ref{fig:minimp:example:bcast}.}
  \label{fig:program:segment:visual}
\end{figure}

As aforementioned, we will introduce specifications for program
segments later.  A specification of a program segment specifies the
behaviors of the program segment, which is defined in term of a state
space graph.

\begin{defn}
  Given a vocabulary $\vocab{}$, a domain, a positive integer $n$, a
  \minimp{} model $\model$ and a program segment
  $\progseg{l}{C}{l'} = (\myloc{}, l, l', T)$ corresponding to
  $\model$, the \emph{state space graph} of $\progseg{l}{C}{l'}$ with
  $n$ processes is a tuple:
  \begin{center}
    $(S_0, S, \leadsto_{\progseg{l}{C}{l'}})$,
  \end{center}
  where 
  
  \begin{itemize}
  \item $S_0$ is a set of initial states, at each of which, every
    process is at location $l$,
  \item $S$ is the set of reachable states from $S_0$ over $T$
  \item $\leadsto_{\progseg{l}{C}{l'}}\colon{} \mystates{} \times \nprocs{n}
    \times \stmt{} \times \mystates{}$ is a set of global
    transitions defined by
    \begin{center}
      $\{ (s, p, \alpha{}, s') \in \leadsto{} | s' \in I(s, p,
      \alpha), s \in S, p \in \nprocs{n}, \alpha{} \in T \}$.  $\qed$
    \end{center}
  \end{itemize}
\end{defn}

Let $G$ be a state space graph of a program segment
$\progseg{l}{C}{l'}$.  A path $\rho$ in $G$ is said a path of
$\progseg{l}{C}{l'}$.  An execution $\pi$ in $G$ is said an execution
of $\progseg{l}{C}{l'}$.  For brevity, we also say $G$ is a state
space graph of $C$ and $\rho$ is a path of $C$ when there is no
possible ambiguity.

Given a program segment and a path $\rho$, there are two kinds of
global transitions in $\rho$ that we have special interests.

\begin{defn}
  Let $\progseg{l}{C}{l'}$ be a program segment and $\rho$ be a path.
  A global transition $t \in \mypathtrans(\rho)$ marks the \emph{first
    entering} of $C$ by a process $p$ on $\rho$, denoted
  $\myenter_{p,\rho}^C$, if $t$ is the first such transition on $\rho$
  that
  \begin{center}
    $\mytoploc(\mysrc(t), p) = l~\wedge{}~\myproc(t) = p$.
  \end{center}
  Given $\myenter_{p, \rho}^C \in \mypathtrans(\rho)$, a global
  transition $t \in \mypathtrans(\rho)$ marks the \emph{exiting} of
  $C$ by process $p$ corresponding to $\myenter_{p, \rho}^C$, denoted
  $\myexit_{p, \rho}^C$, if $t$ is the first such transition appearing
  after $\myenter_{p, \rho}^C$ on $\rho$ that
  
  \begin{enumerate}
  \item $\mytoploc(\mydest(t), p) = l'~\wedge{}~\myproc(t) = p$, and
  \item $|\mystack(\mydest(t), p)| = |\mystack(\mysrc(\myenter_{p,
      \rho}^C), p)|$. $\qed$
  \end{enumerate}
\end{defn}
Note that $\myexit_{p, \rho}^C$ depends on the stack size of the
source state of $\myenter_{p, \rho}^C$ because the execution $\pi$ may
involve recursions.

When the context is clear that there is only one unique path $\rho$,
we simplify $\myenter_{p, \rho}^C$ and $\myexit_{p, \rho}^C$ to
$\myenter_{p}^C$ and $\myenter_{p}^C$, respectively.  Remark that
there is at most one $\myenter_{p}^C$ and $\myexit_{p}^C$ in a path of
$C$ for $p \in \nprocs{n}$.


\section{Path Predicate} \label{sec:minimp:spec:path} A path predicate
consumes a path and returns either true or false.

\begin{defn}
  Let $\rho$ be a path and $A, B, C \in \powerset(\leadsto)$ be three
  global transition sets.  A predicate $\myabsentpred{A}{B}{C}$ is
  true for $\rho$, iff
  \[
    \forall{i,j \in \mathbb{Z}}.\,\,
    ((0 \leq{} i < j < |\rho|) \wedge{} \rho{}[i] \in B \wedge{}
    \rho{}[j] \in A) \Rightarrow{} \exists{k \in \mathbb{Z}}.\,\,
    i \leq{} k < j \wedge{} \rho[k] \in C. \qed
  \]
\end{defn}

The intuitive meaning of $\myabsentpred{A}{B}{C}$ for a path $\rho$ is
that no transition in $A$ can happen after a transition in $B$ until a
transition in $C$ appears on $\rho$
\cite{dwyer:1999:patterns}\footnote{An absence assertion in fact can
  be expressed as an LTL formula, which falls into the exact ``absence
  of" pattern with scope ``after ..\ until'' in the pattern system
  concluded in \cite{dwyer:1999:patterns}.  The pattern system can be
  also found at
  \url{https://matthewbdwyer.github.io/psp/patterns/ltl.html} (visited
  Nov 2019)}.

\begin{defn}
  Let $\rho$ be a path and $A, B, C \in \powerset(\leadsto)$ be three
  global transition sets.  The predicate $\myabsentpred{A}{B}{C}$ is a
  \emph{path predicate}.  Moreover, if $f, g$ are path predicates,
  $f \wedge{} g$, $\neg{}f$ and $f \vee{} g$ are also \emph{path
    predicates}.  $\qed$
\end{defn}

\begin{defn}
  Let $G$ be a state space graph, $\rho$ be a path in $G$, and $s, s'$
  be states in $G$.  For a path predicate $g$, we use

  \begin{itemize}
  \item $\rho \vdash{} g$ to denote that $g$ is true for $\rho$, and
    
  \item $G, s \hookrightarrow{} s'\vdash g$ to denote that $g$ is true
    for every such path $\zeta$ in $G$ that
    $\mysrc{}(\myhead{}(\zeta)) = s$ and $\mydest(\mytail(\zeta)) =
    s'$.    $\qed$
  \end{itemize}
\end{defn}


\section{Syntax of The \minimp{} Specification
  Language} \label{sec:minimp:spec:syntax} In this section, we
introduce a specification language, \minispec{}, for \minimp{}.  The
grammar of \minispec{} is given in Fig.\ \ref{fig:minimp-spec-expr}.
The \nonterm{SpecExpr} is an extension of \nonterm{Expr}.  The overlap
of \nonterm{SpecExpr} and \nonterm{Expr} is omitted with $\synxdots$.

\begin{figure}[h]
  \begin{programNoNum}
    \nonterm{List-of-T} \ \ \synxdef{} \nonterm{T} \biglp{},
    \nonterm{T}\bigrp{}\regxstar{} $\synxbar$ \\
    \nonterm{Spec} \ \ \ \ \  \ \ \synxdef{}
    \nonterm{Clause}$\regxstar{}$ \\
    \nonterm{Clause} \ \ \  \ \ \synxdef{}
    \ccode{requires} \nonterm{SpecExpr} ; $\synxbar$
    \ccode{ensures} \nonterm{SpecExpr}  ; \\
        \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \ccode{requires}
        \nonterm{AbsentSet} ;  $\synxbar$   \ccode{ensures}
        \nonterm{AbsentSet} ;\\
    \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ 
    \ccode{assigns} \nonterm{List-of-LSpecExpr} ;\\
    
        \nonterm{SpecExpr} \  \ \ \synxdef{}
        $\synxdots{}$$\synxbar$ \nonterm{LSpecExpr}  $\synxbar$
        \acslold{} ( \nonterm{SpecExpr} ) $\synxbar$ \nonterm{SpecExpr} ..\ \nonterm{SpecExpr}
        \\        
\ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$  \acslon{} ( \nonterm{SpecExpr} ,
\nonterm{SpecExpr} ) \\
\ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$  \acslforall{}
\nonterm{Identifier} ; \nonterm{SpecExpr} \\

\ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \acslexists{}
\nonterm{Identifier} ; \nonterm{SpecExpr} \\

\nonterm{LSpecExpr}  \ \ \synxdef{} \nonterm{LExpr} $\synxbar$
\nonterm{LSpecExpr} [ \nonterm{SpecExpr} ] \\

\nonterm{AbsentSet} \ \ \synxdef{}  \biglp{}\nonterm{Expr} ==>\bigrp{}\regxques{} \nonterm{Absent} \biglp{}\&\&
\nonterm{Absent}\bigrp{}$\regxstar$ \\

\nonterm{Absent} \ \ \ \ \ \synxdef{} \acslabsent{\nonterm{Event}}{\nonterm{Event}}{\nonterm{Event}}\\

\nonterm{Event}  \ \ \ \  \ \ \synxdef{}
\acslsend ( \nonterm{Expr} , \nonterm{Expr} ) $\synxbar$
\acslexit ( \nonterm{Expr} ) $\synxbar$ \acslenter( \nonterm{Expr} )
  \end{programNoNum}
  \caption{The syntax of \minimp{} specification language}
  \label{fig:minimp-spec-expr}
\end{figure}

A specification consists of a set of \nonterm{Clause}s. There are five
kinds of clauses: the \texttt{requires} \nonterm{SpecExpr} clause
specifies a \emph{state-requirement}; the \texttt{ensures}
\nonterm{SpecExpr} clause specifies a \emph{state-guarantee}; the
\texttt{requires} \nonterm{AbsentSet} clause specifies a
\emph{path-requirement}; the \texttt{ensures} \nonterm{AbsentSet}
clause specifies a \emph{path-guarantee}; and the \texttt{assigns}
\nonterm{SpecExpr} clause specifies a \emph{frame condition}, which is
essentially a state-guarantee.

State-requirement corresponds to pre-condition in Hoare logic.
Similarly, state-guarantee corresponds to post-condition.  A
state-requirement is an assertion holds at a pre-state for all
processes.  A state-guarantee is an assertion holds at a post-state
for all processes.

The path-requirement and -guarantee are designed for specifying
communication correctness.  We will explain and give precise
definition for them later.

\begin{defn}
  Let $\vocab{} = (\myprocedure, \var, \globvar, \locvar)$ be a
  vocabulary.  Denoted by $\sexprv_{\vocab{}}$, the set of
  \nonterm{SpecExpr}s over $\var$.  Denoted by $\seventv_{\vocab{}}$,
  the set of \nonterm{Event}s over $\var$.  Denoted by
  $\sabsentv_{\vocab{}}$, the set of \nonterm{Absent} assertions over
  $\var$.  $\qed$
\end{defn}

A few constructs were borrowed from ACSL:

\begin{enumerate}
\item A range \texttt{$e_0\,$..$\,e_1$} is the finite set of integers
  that are bounded between $e_0$ and $e_1$, both inclusive.

\item The \texttt{\acslold{}} expression bridges the pre- and
  post-states. Expression \texttt{\acslold($e$)} refers to the value
  of $e$ as if $e$ is evaluated at a corresponding pre-state.  The
  \texttt{\acslold{}} construct can only be used in a state-guarantee.

\item First order logic quantifiers: \texttt{\acslforall{}} and
  \texttt{\acslexists{}}
\end{enumerate}
In addition, we designed two new constructs for 
concurrency:

\begin{enumerate}
\item The \texttt{\acslon{}} construct bridegs different
  processes. The expression \texttt{\acslon($e_0$,$e_1$)} refers to
  the value of expression $e_0$ on the process whose \texttt{PID}
  equals to the value of $e_1$.

\item The \emph{absence assertion} allows users to specify the
  $\myabsentpred{A}{B}{C}$ path predicate.  It is the basic element of
  path-requirements or -guarantees.  An absence assertion consists of
  \emph{events}.  There are three kinds of events:
  \texttt{\acslsend{}}, \texttt{\acslenter{}} and
  \texttt{\acslexit{}}, each of which represents a specific kind of
  transitions associated with a path.  For a path, the assertion
  \texttt{\acslabsent{$\theta_0$}{$\theta_1$}{$\theta_2$}} means that
  no event $\theta_0$ can happen after event $\theta_1$ until event
  $\theta_2$ happens on the path.
\end{enumerate}

Informally, be associated with a path, a \texttt{\acslsend{($p$,
    $q$)}} event represents the set of transitions associated with
\texttt{\myactsend{$p$}{$q$}} actions; an \texttt{\acslenter{($p$)}}
event represents the set of transitions marking the first entering of
an associated program segment by process $p$; and an
\texttt{\acslexit{($p$)}} event represents the set of transitions
marking the exiting, that corresponds to the first entering, of an
associated program segment by process $p$.

These three kinds of events can be combined in many ways in an
absence assertion to express various behaviors.  In fact, to 
specify properties for \minimp{} programs, only a few combinations
of the events are needed.  So for simplicity, we impose Restriction
\ref{rest:absent:1} on the use of events in absence assertions.

\begin{rest}
  Given a vocabulary $\vocab$, let $p, q \in \exprv_{\vocab{}}$.  An
  absence assertion,
\begin{enumerate}
\item can only have the following form if it is a path requirement:
  \begin{enumerate}
  \item[]  \texttt{\acslabsent{\acslsend($p$, PID)}{\acslexit($p$)}{\acslexit(PID)}}
  \end{enumerate}
\item can only have one of the following forms if it is a path guarantee:
  \begin{enumerate}
  \item \texttt{\acslabsent{\acslsend(PID, $p$)}{\acslenter(PID)}{\acslenter($q$)}}
    
  \item
    \texttt{\acslabsent{\acslexit(PID)}{\acslenter(PID)}{\acslenter($p$)}} $\qed$
  \end{enumerate}
\end{enumerate}
\label{rest:absent:1}
\end{rest}

The syntax of the path-requirement or -guarantee clauses implies that
they can be considered as the conjunction of a set of absence
assertions.  In other words, we can use a set of absence assertions to
represent a path-requirement or -guarantee.

A \minispec{} specification is assigned to a program segment
$\progseg{l}{C}{l'}$.  We call a specification of a program segment
$\progseg{l}{C}{l'}$ a \emph{contract} of $\progseg{l}{C}{l'}$.  When
there is no ambiguity, we also call it a \emph{contract} of $C$ for
brevity.


\section{Semantics of The \minimp{}
  Contracts} \label{sec:minimp:spec:semantics} 

We fix the following structures for the discussion in the rest of this
chapter: a vocabulary
$\vocab{} = (\myprocedure, \var, \globvar, \locvar)$, a domain $\dom$,
a \minimp{} model $\model$ and a program segment $\progseg{l}{C}{l'}$
corresponding to $\model$.

Similar to Hoare logic, the semantics of the \minispec{} is based on
the notion of the \emph{pre-state} and \emph{post-state}.

Conceptually, a pre-state of $C$ is a state where all processes are at
the entry of $C$.  A post-state of $C$, which must correspond to a
pre-state of $C$, is the final state of an execution of $C$ that
starts from the corresponding pre-state.

\begin{defn}
  Let $G = (S_0, S, \leadsto_{\progseg{l}{C}{l'}})$ be the state space
  graph of $\progseg{l}{C}{l'}$ with $n$ processes.  A state $s$ in
  $G$ is a \emph{pre-state} of $C$, if $s \in S_0$.  Given a pre-state
  $s$ of $C$ and a path $\rho$ containing $s$ in $G$, a state
  $s' \in \mypathstates(\rho)$ is a \emph{post-state} of $C$ in $G$
  corresponding to $s$, if it is the \textbf{first} such state on $\rho$ after
  $s$ that

  \begin{enumerate}
  \item all $n$ processes are at the location $l'$, and
  \item
    $\forall{p \in \nprocs{n}}.\,\, |\mystack(s', p)| = |\mystack(s, p)|$.
  \end{enumerate}
  Denoted by $\mypre(s', \rho, \progseg{l}{C}{l'})$, the pre-state of
  $C$, to which the given post-state $s'$ of $C$ corresponds, in path
  $\rho$.  $\qed$
\end{defn}

An expression $e \in \sexprv_{\vocab}$ is called a contract
expression.  The semantics of a contract expression is given by an
evaluation function extended from the evaluation function for
\minimp{} expressions.

\begin{defn}
  Let $G$ be the state space graph of $\progseg{l}{C}{l'}$ with $n$
  processes.  Let $\rho$ be a path in $G$ that contains a pre-state
  $\mypre(s, \rho, \progseg{l}{C}{l'})$ of $C$ and a post-state $s$ of
  $C$.  The $n$-processes \emph{specification evaluation function}
  $\myseval{e}_n: \mystates \times \nprocs{n} \rightarrow{} \dom$
  evaluates a contract expression $e \in \sexprv_{\vocab{}}$ for a
  process $p$ at either the pre- or the post-state.  $\myseval{e}_n$
  is defined in Fig.\ \ref{fig:spec:expr:eval}. $\qed$
\end{defn}

\begin{figure}
\centering
      \fbox{
    \parbox{.9\textwidth}{
\begin{align}
  \myseval{\texttt{$e_0$ ..\ $e_1$}}_n(s, p) &= \{i \in \mathbb{Z} \mid
                                              \myseval{e_0}_n(s, p)
                                              \leq i <
                                              \myseval{e_1}_n(s, p)\}\nonumber \\
  \myseval{\texttt{a[$e_0$ ..\ $e_1$]}}_n(s, p) &=
                                                 \{\myseval{\texttt{a[$i$]}}_n(s,
                                                 p) \mid
                                                 \myseval{e_0}_n(s, p)
                                                 \leq i <
                                                 \myseval{e_1}_n(s, p)\}\nonumber \\
  \myseval{\texttt{\acslon($e_0$, $e_1$)}}_{n}(s, p) &= 
  \begin{cases}
    \mymath{\myseval{e_0}_n(s, \myseval{e_1}_n(s, p))}, &
    \text{if}~ \mymath{\myseval{e_1}_n(s, p)} \in \nprocs{n} 
    \\ \myundef{}, & \text{otherwise}
  \end{cases}
  \nonumber \\
  \myseval{\texttt{\acslold(}e\texttt{)}}_n(s, p) &=
                                                    \myseval{e}_n(\mypre(s,
                                                     \rho, \progseg{l}{C}{l'}), p)
                                                    \nonumber \\
  \myseval{\texttt{\acslforall{} $v$;} e}_n(s, p) &=
    \textbf{T},  \text{ if }\myseval{e}_n(s, p) = \textbf{T} \text{ for every } v \in \dom{} 
  \nonumber \\
    \myseval{\texttt{\acslexists{} $v$;} e}_n(s, p) &=
    \textbf{T},  \text{ if }\myseval{e}_n(s, p) = \textbf{T} \text{ for some } v \in \dom{} \nonumber \\
  \myseval{e}_n(s, p) &= \myeval{e}_n(s, p) \nonumber
\end{align}
}}
\caption{ The definition of the $n$-processes specification
  evaluation function $\myseval{e}_n$, which evaluates a contract
  expression $e$ for a process $p$ at a pre- or a post-state $s$ of a
  program segment $\progseg{l}{C}{l'}$ in a path $\rho$.}
\label{fig:spec:expr:eval}
\end{figure}
When the number of processes is clear in the context, we simplify
$\myseval{e}_n$ to $\myseval{e}$.

A frame condition states what is unchanged by a program segment.  The
\texttt{assigns} clause specifies a list of \nonterm{LSpecExpr}s and
encodes the meaning that any object that is not listed will never be
changed by the program segment.  For a programming language as simple
as \minimp{}, a frame condition can always be transformed to a
state-guarantee statically.  Because one can always assert that a
variable at a post-state preserves its value in the pre-state using
the \ccode{\acslold} expression.  All visible variables to a location
are known statically.  The transformation process is omitted.  In the
rest of this dissertation, we will not pay special attention to frame
conditions.

An \nonterm{Event} is interpreted to a set of global
transitions with respect to a path of a program segment.

\begin{defn}
  Let $G$ be the state space graph of $C$ with $n$ processes.  Let
  $\rho$ be a path in $G$.  The \emph{event interpretation} function
  $I^{\textsf{event}}_{C, \rho}: \seventv_{\vocab{}} \times \mystates
  \times \nprocs{n} \rightarrow{} \powerset(\leadsto)$ depends on $C$
  and $\rho$.  It interprets an event $\theta \in \seventv_{\vocab{}}$
  to a set of global transitions at a state $s$ for a process $p$.
  $I^{\textsf{event}}_{C, \rho}(\theta, s, p)$ is defined in Fig.\
  \ref{fig:event:interpret}. $\qed$
\end{defn}

\begin{figure}
\centering
      \fbox{
    \parbox{.9\textwidth}{
  \begin{align}
    I^{\textsf{event}}_{C, \rho}(\texttt{\acslenter{}($e$)}, s, p)
      &= \{\myenter{}^C_{\myeval{e}(s, p), \rho}\} \nonumber \\
      I^{\textsf{event}}_{C, \rho}(\texttt{\acslexit($e$)}, s, p)
      &= \{\myexit^C_{\myeval{e}(s, p), \rho}\}  \nonumber \\[\myskip]
       I^{\textsf{event}}_{C, \rho}(\texttt{\acslsend($e_0$, $e_1$)}, s, p)
     & = \{t \in \leadsto \mid \myproc(t) = \myeval{e_0}(s, p)
       \wedge{} \nonumber \\
    &~~~~~~\myact(t) = \texttt{send($v$,
      $\myeval{e_1}(s, p)$)}, v \in \var \} \nonumber       
  \end{align}
  }}
\caption{The definition of the event interpretation function
  $\mymath{I^{\textsf{event}}_{C, \rho}}$ with respect to a path
  $\rho$ and a program segment $\progseg{l}{C}{l'}$.}
  \label{fig:event:interpret}
\end{figure}

An absence assertion will be interpreted to a path predicate.

\begin{defn}
  Let $G$ be a state space graph of $C$ with $n$ processes.  Let
  $\rho$ be a path in $G$.  Let $I^{\textsf{event}}_{C, \rho}$ be the
  event interpretation function depending on $C$ and $\rho$.  The
  $n$-processes \emph{absence assertion evaluation} function
  $\myaeval{e}_{C, \rho}: \mystates{} \times \nprocs{n} \rightarrow{}
  \{\textbf{T}, \textbf{F}\}$ depends on
  $I^{\textsf{event}}_{C, \rho}$.  It evaluates an absence assertion
  $e \in \sabsentv{_{\vocab}}$ to either true or false at a state $s$
  for a process $p$.  We define
  \begin{align}
    & \myaeval{\texttt{\acslabsent{$\theta_0$}{$\theta_1$}{$\theta_2$}}}_{C,\rho}(s, p) =
      \nonumber\\
    &~~~~\text{let } A = I^{\textsf{event}}_{C,\rho}(\theta_0, s, p) \text{
      in}\nonumber \\
    &~~~~\text{let } B = I^{\textsf{event}}_{C,\rho}(\theta_1, s, p) \text{
      in}\nonumber \\
    &~~~~\text{let } C = I^{\textsf{event}}_{C,\rho}(\theta_2, s, p) \text{
      in }
      \rho \vdash{} \myabsentpred{A}{B}{C}.
      \nonumber 
  \end{align}
  Recall we also write $\rho \vdash{} \myaeval{e}_C(s,p)$ for
  $\myaeval{e}_{C,\rho}(s,p) = \textbf{T}$.  $\qed$
\end{defn}

\textbf{Writing Contracts for \minimp{} Statements.}  A \minimp{}
program will be run by a group of processes collectively.  The program
is written with the idea that it will be run by a generic process.  A
contract of a \minimp{} substatement is designed with the same idea.
A contract should be assigned to a substatement that is intended to be
run by all processes collectively.  The contract specifies the
collective behavior of the code.  Intuitively, a contract can be
understood by the user in the perspective of a generic process.  For
example, an absence assertion \texttt{\acslabsent{\acslsend($p$,
    PID)}{\acslexit{($p$)}}{\acslexit{(PID)}}} in a contract of a
substatement $C$ can be understood as `` process $p$ shall not send a
message to me after it exits $C$ until I exit $C$ too.'', where ``I''
refers to a generic process.

We use the following two \minispec{} specifications as examples to
give readers a taste of what does ``a statement satisfies a contract
in a collective way'' mean.  The formal description of the contract
conformance will be described in \S\ref{sec:minimp:spec:triple}.

\begin{exmp}
  Figure \ref{fig:minimp:spec:bcast} is a contract for the branch
  statement (at line 3-11) of the \texttt{bcast} procedure presented
  in the left of Fig.\ \ref{fig:minimp:example:bcast}.  In the
  contract, the state-requirement states that all processes must have
  the same value for their \texttt{root}.  In addition, the value
  of \texttt{root} shall be bounded between 0 and \texttt{NPROCS}.
  The statement may modify variables \texttt{dat} and \texttt{i} so
  they are listed in an \texttt{assigns} clause.  The state-guarantee
  expresses that, for every process, if it
  is \texttt{root}, \texttt{dat} remains unchanged.
  Otherwise, \texttt{dat} will be modified to have the same value as
  the one on process \texttt{root} at the post-state.  The contract
  finally guarantees that no process can exit the statement until
  process \texttt{root} enters it.  $\qed$ \end{exmp}

 \begin{figure}
   \begin{program}
     \ccode{var} i, root, dat;~\\
     \mycomment{// contract:}\\
     \ccode{requires} \acslforall{} t; \acslon{}(root, t) == root;\\
     \ccode{requires}  0 <= root \&\& root < NPROCS;  \\
     \ccode{assigns}   dat, i;             \\
     \ccode{ensures}   PID == root ==> dat == \acslold(dat);  \\
     \ccode{ensures}   dat == \acslon(dat, root);       \\
     \ccode{ensures}
     \acslabsent{\acslexit(PID)}{\acslenter(PID)}{\acslenter(root)};\\
     \mycomment{// code:} \\
   \ccode{if}~(PID~==~root)~\lb\\
    ~~i~=~0;\\
    ~~\ccode{while} (i < NPROCS) \lb{}\\
    ~~~~\ccode{if} (i != root) \\
    ~~~~~~\send{dat}{i};\\
    ~~~~i = i + 1;\\
    ~~\rb{}\\
    \rb~\ccode{else}\\
    ~~\recv{dat}{root};\\
   \end{program}
   \caption{A contract of a branch statement that ``broadcasts'' a
     value.}
   \label{fig:minimp:spec:bcast}
 \end{figure}

\begin{exmp}
  Figure \ref{fig:minimp:spec:gather} is a contract for the branch
  statement (at line 3-15) in the \texttt{gather} procedure presented
  in the right of Fig.\ \ref{fig:minimp:example:gather}.  The contract
  requires that all processes must have the same value for
  \texttt{root}, which must refer to a valid \texttt{PID} value.  In
  addition, the variable \texttt{dat} must be an array of length no
  less than \texttt{NPROCS}.  
  The statement may modify variables \texttt{i}, \texttt{y}
  and \texttt{dat}, which are therefore listed in the \texttt{assigns}
  clause.  The state-guarantee states that the value
  of \texttt{dat[$i$]} on the \texttt{root} process equals to the
  value of \texttt{val} on process $i$, for every process $i$.
  Finally, the contract guarantees that, for the \texttt{root}
  process, it will not exit the statement until all processes have
  entered it.  $\qed$ \label{exmp:minimp:spec:gather}
\end{exmp}

\begin{figure}
  \begin{center}
    \begin{program}
      \ccode{var} i, y, dat, root, val;\\
      \mycomment{// contract: }\\
      \ccode{requires} \acslforall{} t; \acslon{}(root, t) == root;\\
      \ccode{requires} 0 <= root \&\& root < NPROCS \&\&
      \ccode{len}(dat) >= NPROCS;\\
      \ccode{assigns}  dat, i, y;\\
      \ccode{ensures} PID == root ==> \\
      \ \ \ \ \ \ \ \ \ \ \acslforall{} int t; 0 <= t \&\& t < NPROCS ==>\\
      \ \ \ \ \ \ \ \ \ \ \ \ dat[t] == \acslon(val, t); \\
      \ccode{ensures} PID == root ==> \\
      \ \ \acslabsent{\acslexit(PID)}{\acslenter(PID)}{\acslenter(0
        ..\ NPROCS-1)};\\
      \mycomment{// code:}\\
      \ccode{if}~(PID~==~root)~\lb\\
      ~~i~=~0; \\
      ~~dat = \ccode{new} [NPROCS];\\
      ~~dat[root] = val;\\
      ~~\ccode{while} (i < NPROCS) \lb{}\\
      ~~~~\ccode{if} (i != root) \lb{}\\
      ~~~~~~\recvany{val}{y};\\
      ~~~~~~dat[y] = val;\\
      ~~~~\rb{}\\
      ~~~~i = i + 1; \\
      ~~\rb{}\\
      \rb~\ccode{else} \\
      ~~\send{val}{root};\\
    \end{program}
  \end{center}
  \caption{A contract for the branch statement that ``gathers'' values
    from all processes.}
  \label{fig:minimp:spec:gather}
\end{figure}

\section{The Collective Triple} \label{sec:minimp:spec:triple}

In this section, we first define an abstract representation for a
program segment with a contract, called \emph{collective triple}.
Then we discuss about the intuitive meaning of a collective triple.
Finally, we formally define the meaning of the conformance of a
program segment to a contract in terms of a corresponding collective
triple.

Recall that we have fixed the context of our discussion with these
general structures: a vocabulary
$\vocab{} = (\myprocedure, \var, \globvar, \locvar)$, a domain $\dom$,
a \minimp{} model $\model$ and a program segment $\progseg{l}{C}{l'}$
corresponding to $\model$.

\begin{defn}
  Suppose the program segment $\progseg{l}{C}{l'}$ is assigned a
  contract.  A \emph{collective triple} representing the program
  segment with the contract has such a form:
\begin{center}
  $\cotriple{}$,
\end{center}
where

\begin{itemize}
\item $\psi, \phi \in \sexprv{_\vocab}$ are the state-requirement and 
  -guarantee of $C$, respectively, and

\item $\Gamma, \Upsilon \in \sexprv{_\vocab}$ are expressions representing
      the path-requirement and -guarantee, respectively. $\qed$
\end{itemize}
\end{defn}
When the location information is not needed, we may simplify
$\cotriple{}$ to $\cotriplenoloc$.

Recall in Fig.\ \ref{fig:minimp-spec-expr}, the grammar only allows a
path-requirement or -guarantee to have such a form:
\texttt{\biglp{}\nonterm{Expr} ==>\bigrp{}\regxques{}\
  \nonterm{Absent} \&\& \nonterm{Absent} \&\& $\ldots{}$}.  So a
path-requirement or -guarantee can be represented by a set of absence
assertions, the conjunction of which equals to the path-requirement or
guarantee.  In later sections, we will define operations similar to
set-operations for reasoning about path-requirements and guarantees.


\subsection{The Intuition in Collective Triple}
%% validity means satisfaction, collective-style statement C
\begin{defn}
  The substatement $C$ satisfies a contract iff the collective triple
  $\cotriplenoloc{}$, which represents $C$ and the contract, is
  \emph{valid}. $\qed$
\end{defn}

%% intuition of the meaning of a collective triple, communication
%% closed.  Mainly pre- and post-cond  but interference can happen.
We informally discuss about the validity of a triple $\cotriplenoloc$
in this subsection.

Intuitively, a \minimp{} program can be considered as a ``collective''
statement in that

\begin{enumerate}
\item An execution of the program starts from a pre-state of the body
  of the \texttt{main} procedure, and will end at a corresponding
  post-state of the body, if every process eventually terminates.
  
\item Every message that was sent by a process $p$ when $p$ was in the
  statement will eventually be received by a process $q$ when $q$ is
  in the statement.
\end{enumerate}
Such a ``collective'' statement $C$ has two features that we are
interested in.  First, $C$ does not depend on the environment to
ensure its communication correctness.  Second, the functional
correctness of $C$ can be expressed via asserting the inputs and
outputs of $C$ with respect to its pre- and post-states.  Ideally, if
a \minimp{} program can be divided into a set of such ``collective''
substatements, we can apply Hoare logic, without much extension, to
reason about the program in a composite and modular way.  We use
Example \ref{exmp:minimp:ideal:reasoning} to briefly illustrate the
idea.

\begin{exmp}
  Figure \ref{fig:minimp:example:exchanges} shows a \minimp{} program
  in pseudocode.  In the program, a 
  \texttt{\textit{barrier}} divides the body of the \texttt{main}
  procedure into two ``collective'' substatements: one, denoted $C_0$,
  is at line 3--9 and the other, denoted $C_1$, is at line 10--11.
  Functional correctness of $C_0$ and $C_1$ can be specified using
  assertions over their inputs and outputs with respect to their pre-
  and post-states.  A reasoning about the property of our interests,
  informally, will be something like the following:

  \begin{itemize}
  \item For every process, $C_0$ ensures that \texttt{dat[9]} will be
    modified to have the same value as \texttt{dat[1]} of its
    \texttt{right} neighbor.  Nothing else will be modified by $C_0$.

  \item For every process, $C_1$ ensures that \texttt{dat[0]} will be
    modified to have the same value as \texttt{dat[8]} of its
    \texttt{left} neighbor.  Nothing else will be modified by $C_1$.

  \item Concluding from the above, the body of the \texttt{main}
    procedure ensures that, for every process, its \texttt{dat[0]} and
    \texttt{dat[9]} will be modified to have the same values as
    \texttt{dat[8]} and \texttt{dat[0]} of its \texttt{left} and
    \texttt{right} neighbors, respectively. $\qed$
  \end{itemize}
  \label{exmp:minimp:ideal:reasoning}
\end{exmp}

\begin{figure}
  \centering
  \begin{program}
    \ccode{fun} main() \lb{} \\
    \ \ \ccode{var} dat, left, right; \\
    \ \ dat = \ccode{new} [10];\\
    \ \ left = (PID + NPROCS - 1) \% NPROCS;\\
    \ \ right = (PID + 1) \% NPROCS;\\
    \ \ dat = \textit{init}(PID); \\
    \ \ \send{dat[1]}{left}; \\
    \ \ \recv{dat[9]}{right}; \\
    \ \ \textit{barrier};\\
    \ \ \send{dat[8]}{right}; \\
    \ \ \recv{dat[0]}{left}; \\
    \rb{}
  \end{program}
  \caption{A \minimp{} program in pseudocode where \textit{init} is a
    procedure that depends on \texttt{PID} and initializes
    \texttt{dat} elements.  Suppose \texttt{\textit{barrier}} is a
    barrier.}
  \label{fig:minimp:example:exchanges}
\end{figure}

However, most of the \minimp{} programs cannot be divided into
multiple such ideal substatements.  There are two reasons.  First,
\texttt{\textit{barrier}} is not frequently used in
real message-passing applications because of the pursuit of
performance.  So there is not necessarily a pair of pre- and
post-states of some substatement in an execution of a program.
Second, without \texttt{\textit{barrier}}s, the communication
correctness of a substatement may depend on the environment.  In such
cases, one cannot specify the communication correctness of a
substatement by only constraining the inputs and outputs.  We show an
example for the second reason by revisiting Example
\ref{exmp:minimp:spec:gather}.

Considering the contract (Fig.\ \ref{fig:minimp:spec:gather}) of the
statement $S$.  If one reasons about $S$ with respect to the contract
only over the executions in state space graphs of $S$, $S$ satisfies
the contract.  But it is insufficient.  In fact, the existence of $S$
may make a program invalid.  The conformance of $S$ to a contract must
guarantee the validity of the use of $S$ in any case as long as the
requirements of the contract is met.  In such a sense, $S$ actually
fails to satisfy the contract.  The communication correctness of $S$
indeed depends on its context.

Imagine that there is an execution of a program containing $S$.
Suppose there is a suffix $\rho$ of the execution that starts from a
pre-state of $S$.  On $\rho$, a non-\texttt{root} process $p$
completes $S$ and then sends a message again to the \texttt{root}
process $q$ before $q$ done all the receiving in $S$.  Since $q$
receives messages with the wildcard \texttt{recv} statement, $q$ can
receive twice from $p$ before completing $S$.  Such an execution is
undesired.  Because it can possibly lead to a deadlock.  More
importantly, there is no way one can prove the conformance of $S$ to
its contract because the message coming from the outside of $S$ is
unspecified.  Therefore, $S$ must have an assumption on the contexts
in order to ensure its communication correctness.  In general, we call
the situation, in which a process $q$ receives a message sent by a
another one $p$ after $p$ completes $S$, \emph{$S$ is interfered}.
\emph{Interference} is unwelcome.  We discuss about this problem in
the next subsection.

Path-requirements and -guarantees are designed to address the
interference problem with the idea of minimizing the communication
detail reflected off a contract.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%              EXTENDED                     %%%%%%
%%%%%%              EXECUTION                    %%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
As aforementioned, the state space graphs of a program segment is not
a sufficient scope for the problem of contract conformance.
Therefore, we define a more general notion, \emph{extended
  executions}.

\begin{defn}
  Let $T$ be the union of local transition sets of procedures in the
  model $\model$.  Let $\progseg{l}{C}{l'}$ be a program segment
  corresponding to $\model$.  A global transition sequence
  $\zeta \in \leadsto^*$ is called an \emph{extended execution} of
  $\progseg{l}{C}{l'}$, if

  \begin{enumerate}
  \item $\zeta$ starts from a pre-state of $C$, 

  \item
    $\forall{(s, p, \alpha, s') \in \mypathtrans(\zeta)}.\, s' \in
    I(s, p, \alpha)~\wedge{}~\alpha{} \in T$, and
    
  \item for every sub-path $t_it_{i+1}$ of $\zeta$,
    $\mydest(t_i) = \mysrc(t_{i+1})$.     $\qed$
  \end{enumerate}
  \label{defn:extended:execution}
\end{defn}
We also call $\zeta$ is an extended execution of $C$ when it is clear
in the context that there is a unique program segment of $C$.  An
intuitive explanation for Def.\ \ref{defn:extended:execution} is that
an extended execution of $C$ is a path emanating from a pre-state of
$C$, where processes may continue to execute after completing $C$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%% INFORMAL COLLECTIVE TRIPLE MEANING %%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

With the notion of extended executions, we informally generalize the
validity of a collective triple $\cotriplenoloc{}$ to the following:

\begin{itemize}
\item for every execution $\pi$ of $C$, if $\psi$ and
  \texttt{allempty} hold on the pre-state of $C$ (i.e., the initial
  state of $\pi$) for all processes, then $\phi$ and \texttt{allempty}
  will hold on the corresponding post-state of $C$ for all processes,
  as long as every process completes $C$ eventually, and

\item for every same execution $\pi$ as above, path predicates
  interpreted at the pre-state of $C$ for all processes are true for
  $\pi$, and

\item for every extended execution $\zeta$ of $C$, where $\psi$ and
  \texttt{allempty} hold at the pre-state $s$ of $C$ for all
  processes, if interference happens on $\zeta$, $\zeta$ must violate
  at least one path predicate among those interpreted from elements in
  $\Gamma$ at $s$ for all processes.
\end{itemize}
Note that we choose to interpret path-requirements and -guarantees at
pre-states.  This is a choice made for the convenience in
implementation while the intuition of the meaning of those contract
clauses is preserved.

We call the substatement $C$, which is specified by a \minispec{}
contract, a \emph{collective style} substatement.  The name implies
the intention that $C$ shall be executed by all processes collectively
and its communication correctness shall be independent with the
environment as long as requirements are met.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%                           interference                                   %%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Interference}

On an extended execution of $\cotriplenoloc{}$, we call the situation,
in which a process $p$ sends a message after completing $C$ and a
process $q$ receives the message before completing $C$, an
\emph{interference}.  We also say that $C$ is \emph{interfered} by the
statement following it.

Note that the symmetry case that a process in $C$ receives a message
sent by a process that has not entered $C$ can be ignored.  Suppose a
\minimp{} program is divided into a set of substatements
$C_0C_1\ldots{}C_{m-1}$.  If one proves that $C_i$ can never be
interfered by $C_{j}$, for $j > i$, one also proves the freedom of the
symmetry case.  If a process in $C_i$ receives a message sent by a
another process that has not entered $C_i$, there must be a statement
$C_k$ ahead of $C_i$ (i.e., $k < i$) in which a message sent by a
process in $C_k$ is never received by a process in $C_k$.  Without
loss of generality, we can assume that $C_k$ is the first statement in
a program.  $C_k$ is suppose to satisfy a contract, according to the
decomposition assumption.  However, since there is a execution of
$C_k$, on which a message sent by a process is never received by any
process in $C_k$, the message channels cannot all be empty at the
post-state of $C_k$.  Therefore, there is no collective triple of
$C_k$ can be proved valid.

We now give \emph{interference} a precise description in terms of the
number of messages that were sent and received by processes.

\begin{defn}
  Let $\rho$ be a path.  We use $\mynrecvs{\rho}{p}{p'}$ to denote the
  number of receive actions executed by process $p'$ from process $p$
  in $\rho$.  Dually, we use $\mynsends{\rho}{p}{p'}$ to denote the
  number of send actions executed by process $p$ to process $p'$ in
  $\rho$.  Formally,
\begin{align}
  \mynrecvs{\epsilon}{p}{p'}
  &= 0 \nonumber \\ 
  \mynrecvs{\rho~\circ{}~t}{p}{p'}
  &=
    \begin{cases}
      \mynrecvs{\rho}{p}{p'} + 1 \text{, if } \myproc(t) = p'
      \wedge{} \myact(t) = \myactrecv{$v$}{$p$} \text{ for some $v$}\\
      \mynrecvs{\rho}{p}{p'} \text{, otherwise}
      \end{cases}
    \nonumber \\
  \mynsends{\epsilon}{p}{p'}
  &= 0 \nonumber \\ 
  \mynsends{\rho~\circ{}~t}{p}{p'}
  &=
    \begin{cases}
      \mynsends{\rho}{p}{p'} + 1 \text{, if } \myproc(t) = p
      \wedge{} \myact(t) = \myactsend{$v$}{$p'$} \text{ for some $v$} \\
      \mynsends{\rho}{p}{p'} \text{, otherwise} $\qed$
      \end{cases}
    \nonumber 
\end{align}
\end{defn}

\begin{defn}
  Given an extended execution $\zeta$ of $C$.  Let $\rho_p$ be a
  prefix of $\zeta$ such that
  $\mymath{\mytail(\rho_p) = \myexit^C_p}$.  An \emph{interference
    happens} on $\zeta$ if
  $\mynsends{\rho_p}{p}{q} < \mynrecvs{\rho_q}{p}{q}$, denoted as
  $\myinterfere{\zeta}{C}(p, q)$. $\qed$
\end{defn}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%     Collective Triple Validity     %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{The Validity of A Collective Triple}
Finally, we give a precise definition for the validity of a collective
triple.

\begin{defn}
  Let $n$ be a positive integer.  For every execution $\pi$ and
  extended execution $\zeta$ of $C$ with $n$ processes.  Let
  $s = \mysrc(\myhead(\pi))$, $s' = \mydest(\mytail(\pi))$ and
  $s'' = \mysrc(\myhead(\zeta))$.  A triple $\cotriplenoloc{}$ is said
  \emph{deterministically valid}, denoted
  $\model \models^{D} \cotriplenoloc{}$, iff

  \begin{enumerate}
  \item if
    \begin{center}
    $\forall{p \in \nprocs{n}}.\, \myseval{\psi{} \wedge{}
      \texttt{allempty}}(s, p) = \textbf{T}$,
    \end{center}
    and $s'$ is a post-state of $C$
    corresponding to $s$, then
    \begin{center}
    $\forall{p \in \nprocs{n}}.\, \myseval{\phi \wedge{}
      \texttt{allempty}}(s', p) = \textbf{T}$,
  \end{center}
  and
  
  \item $\forall{p\in\nprocs{n}}.\,\pi \vdash{} \myaeval{\textup{$\Upsilon$}}_C(s, p)$.
  \end{enumerate}
  The triple is said \emph{valid}, denoted
  $\model \models \cotriplenoloc$, iff

  \begin{enumerate}
  \item $\model \models^D \cotriplenoloc$, and
  \item
    $\forall{p, q \in \nprocs{n}}.\,\, \myinterfere{\zeta}{C}(p, q)
    \Rightarrow{} \exists{k \in \nprocs{n}}.\, \zeta \vdash{} \neg{}\myaeval{\textup{$\Gamma$}}_C(s'', k)$. $\qed$
  \end{enumerate}  
  \label{defn:semantics:collective:triple}
\end{defn}
  
\begin{coro}
  For the model $\model$, If $\model \models^{\Delta} \cotriplenoloc$,
  and there is no wildcard receive ever used in $C$, we have
  $\model \models \cotriplenoloc$.  $\qed$
\end{coro}