\section{Function Contracts for MiniMP} \label{sec:minimp:contract}
A \emph{function contract} is a specification which defines the
\emph{functional correctness} of a function.  In this section, we
define the syntax and semantics of \emph{function contract} for MiniMP
functions.

\subsection{Syntax}
%%%%%%%%%%% Contract grammar %%%%%%%%%%%%%%%
\begin{figure}[h]
  \begin{programNoNum}
    \nonterm{Contract} \ \ \ \ \ \ \ \ \ \ \ := \nonterm{LocalBehaviors} \nonterm{CollectiveBehaviors}\\
    \nonterm{LocalBehaviors} \ \ \ \ \ := \biglp{}\nonterm{Clause};\bigrp{}\textit{*} \nonterm{NamedBehavior}\textit{*}\\
    \nonterm{CollectiveBehaviors} := collective: \biglp{}\nonterm{Clause};\bigrp{}\textit{*} \nonterm{NamedBehavior}\textit{*}\\
    \nonterm{NamedBehavior}  \ \ \ \ \ \ := behavior \nonterm{Identifier} :\ \biglp{}\nonterm{Clause};\bigrp{}\textit{*}\\
    \nonterm{Range} \ \ \ \ \ \ \ \ \ \ \ \ \ \ := \nonterm{Expression} ..\ \nonterm{Expression}\\
    \nonterm{Assignable} \ \ \ \ \ \ \ \ \ := \nonterm{Identifier}[\nonterm{Range}] $\mid$ \nonterm{Identifier}\\
    \nonterm{SetExpr} \ \ \ \ \ \ \ \ \ \ \ \ := \nonterm{Assignable} $\mid$ \nonterm{Expression}\\
    \nonterm{ContractExpr} \ \ \ \ \ \ \ := \nonterm{Expression} $\mid$ \nonterm{Expression} @ \nonterm{Expression} $\mid$ \BSL{}result\\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\mid$ \BSL{}old(\nonterm{Expression}, \nonterm{Expression})\\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\mid$ \BSL{}forall \nonterm{VariableDecl}; \nonterm{ContractExpr} \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\mid$ \BSL{}exists \nonterm{VariableDecl}; \nonterm{ContractExpr} \\
    \nonterm{Clause} \ \ \ \ \ \ \ \ \ \ \ \ \ := requires \nonterm{ContractExpr} \ \ \ \ \ \ \ \ \ \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  $\mid$ ensures \nonterm{ContractExpr} \ \ \ \ \ \ \ \ \ \ \\ 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  $\mid$ assigns \nonterm{Assignable} \biglp{}, \nonterm{Assignable}\bigrp{}\textit{*} $\mid$ \BSL{}nothing \\ 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  $\mid$ assumes \nonterm{Expression} \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \\ 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  $\mid$ waitsfor \nonterm{SetExpr} \biglp{}, \nonterm{SetExpr}\bigrp{}\textit{*} $\mid$ \BSL{}nothing\\ 
  \end{programNoNum}
  \caption{The syntax of function contracts in
    MiniMP. Keywords that start with a 
      ``\texttt{\BSL{}}'' are borrowed from ACSL}
  \label{fig:minimp:contract-syntax}
\end{figure}

An ACSL-like grammar of the MiniMP function contracts is given in
Figure \ref{fig:minimp:contract-syntax}.

A MiniMP function contract is composed of two parts: \emph{local
  behaviors} and \emph{collective behaviors}.  Each of the two parts
is a collection of \emph{behaviors}, including a \emph{default
  behavior} and \emph{named behaviors}.  A behavior is a collection of
\emph{contract clauses} under an \emph{assumption}.  Contract clauses
\texttt{requires}, \texttt{ensures} or \texttt{assumes} shall be
followed by a boolean expression.  Contract clause \texttt{assigns}
shall be followed by a list of variables.  Contract clause
\texttt{waitsfor} shall be followed by a list of expressions.

For expressive power, few more constructs are added upon what has been
defined in \nonterm{Expression}: 1) a range or a range over an array
is a finite set of integers; 2) an \texttt{\BSL{}old} unary operator,
which bridges the states before and after a function; 3) a remote
operator \texttt{@}, which is designed for referring evaluation of
other processes; 4) a term \texttt{\BSL{}result} which refers to the
return expression of a function and 5) first order logic quantifiers:
\texttt{\BSL{}forall} and \texttt{\BSL{}exists}.

A \texttt{requires} clause specifies a pre-condition.  An
\texttt{ensures} clause specifies a post-condition. An
\texttt{assigns} clause specifies a \emph{frame condition}, which is
essentially a post-condition.  The frame condition states that a set
of objects always stay unchanged before and after a function.  It is
expressed by explicitly listing the set of objects, that might be
changed by a function, in \texttt{assigns} clauses.  A constant
\texttt{\BSL{}nothing} can be used to represent an empty set in an
\texttt{assigns} clause.  A \texttt{assumes} clause specifies an
assumption for a named behavior.

A \texttt{waitsfor} clause specifies a synchronous condition.  A
synchronous condition states that the running process will not leave a
function until a specific set of processes that have arrived the
function.  The synchronous condition is expressed via explicitly
listing expressions, which represent the set of \texttt{PID}s of the
processes that must be waited for, in \texttt{waitsfor} clauses.  A
constant \texttt{\BSL{}nothing} can be used to represent an empty set in an
\texttt{waitsfor} clause.

The absence of \texttt{requires} (resp. \texttt{ensures},
\texttt{assumes}) clause in a function contract is equivalent to have
a sole \texttt{requires true} (resp. \texttt{ensures true},
\texttt{assumes true}) clause in it.  The absence of \texttt{assigns}
clause in a function contract is equivalent to stating that all
objects might be changed by the function.  The absence of
\texttt{waitsfor} clause in a function is equivalent to have a sole
\texttt{waitsfor \BSL{}nothing} clause in it.

In a behavior collection, a named behavior starts from a keyword
\texttt{behavior} with an identification tag and ends with either
another named behavior, the end of a behavior collection or the end of
the function contract.  The default behavior consists of all contract
clauses before all named behaviors.

A collective behavior collection starts from a keyword
\texttt{collective} and ends with the end of the function contract.  A
local behavior collection consists of all behaviors before a
collective behavior collection.

Figure \ref{fig:example-exchange} is an example of a function contract
of a MiniMP function \texttt{exchange}.  In \texttt{exchange}, every
process sends a message to its right neighbor and receives a message
from its left neighbor in a cyclic way.  The contract of
\texttt{exchange} consists of a local behavior collection, which only
has the default behavior with an \texttt{assigns} clause, and a
collective behavior collection, which contains two named behaviors.
One of the named behaviors is for processes whose \texttt{PID} is
greater than zero; the other is for the process whose \texttt{PID}
equals to zero.  Post-conditions in the two behaviors have the same
meaning: after this function, the variable \texttt{buf} will hold the
value in variable \texttt{val} of its left neighbor.
\begin{figure}
\begin{program}
\ccode{int} to, from, buf;\\
  \ccode{int} exchange(int val) \\
\ \  assigns  to, from, buf; \\
\ \  collective: \\
\ \ \ \ behavior regular: \\
\ \ \ \ \ \ assumes PID > 0; \\
\ \ \ \ \ \ ensures buf == val@(PID-1); \\
\ \ \ \ \ \ waitsfor PID-1; \\
\ \ \ \ behavior leftmost: \\
\ \ \ \ \ \ assumes PID == 0; \\
\ \ \ \ \ \ ensures buf == val@(NPROCS-1); \\
\ \ \ \ \ \ waitsfor NPROCS-1 ; \\
\lb{}  \\
\ \ \ccode{if} (PID == NPROCS - 1) \lb{}\\
\ \ \ \ to = 0;\\
\ \ \rb{} \ccode{else} \lb{}\\
\ \ \ \ to = PID + 1;\\
\ \ \rb{}\\
\ \ \ccode{if} (PID == 0) \lb{}\\
\ \ \ \ from = NPROCS - 1;\\
\ \ \rb{} \ccode{else} \lb{}\\
\ \ \ \ from = PID - 1;\\
\ \ \rb{}\\
\ \ send(val, to);\\
\ \ recv(buf, from);\\
\ \  \ccode{return} 0;\\
\rb {}\\
\ccode{int} main() \lb{}\\
\ \ exchange(PID); \\
\ \ \ccode{return 0}; \\
\rb {}
\end{program}
\caption{a MiniMP program where a collective-style function
  \texttt{exchange} is defined with function contracts}
\label{fig:example-exchange}
\end{figure}

\subsection{Model of Contracts}
We first give the model of a MiniMP function contract.  Let us assume
that there is always a preprocess procedure which replaces all the
\texttt{\BSL{}result} terms in a function contract with the return
expression of the function.  We say that $e_0 \texttt{ \&\& } e_1
\texttt{ \&\& } ... \texttt{ \&\& } e_{n-1}$ is a \emph{conjunction}
of a set of expressions $\{e_0, e_1, ..., e_{n-1}\}$.


\begin{defn}
  A function contract $C_f$ of a function $f$ is a pair:
  \begin{center}
    $\mymath{C_f = (B^{local}_f, B^{col}_f)}$
  \end{center},
  where $\mymath{B^{local}_f}$ is a set of local behaviors and
  $\mymath{B^{col}_f}$ is a set of collective behaviors.
\end{defn}

\begin{defn}  
  A behavior is a tuple:
  \begin{center}
    $\mymath{b_f = (A_{b_f}, R_{b_f}, E_{b_f}, Var_{b_f}, W_{b_f})}$
  \end{center}
  , where 
  \begin{enumerate}
  \item $\mymath{A_{b_f}}$ is the conjunction of the expressions that are
    specified in \texttt{assumes} clauses in this behavior
  \item $\mymath{R_{b_f}}$ is the conjunction of the expressions that are
    specified in \texttt{requires} clauses in this behavior
  \item $\mymath{E_{b_f}}$ is the conjunction of the expressions that are
    specified in \texttt{ensures} clauses in this behavior
  \item $\mymath{Var_{b_f}}$ is the set of variables that are specified in
    \texttt{assigns} clauses in this behavior
  \item $\mymath{W_{b_f}}$ is the set of expressions that are specified in
    \texttt{waitsfor} clauses in this behavior
  \end{enumerate}
\end{defn}

Note that a named bahavior describes specification for some specific
executions or processes.  Whether an execution or a process must
satisfy a named behavior depends on if the assumption in the behavior
evaluates to true.  The meaning of the named behavior becomes
confusing if an assumption evaluation may be different before and
after executing a function.  In order to eliminate such meaningless
situations from the model, we add a restriction $A_{b_f} \in
Form((Var_f \cup Var_g) - Var_{b_f})$ for $A_{b_f}$.

The Definition \ref{defn:function-graph} of function graphs is then
extended with contracts:

\begin{defn}
  A function graph of a function $f$ with a contract $C_f$ is a tuple:
  \begin{center}
    $\mymath{FG'_f = (f, Loc_f, loc_{0_f}, Var_f \cup Var_g, Act,
      Edge_f, \phi^{local}_f, \psi^{local}_f, \phi^{col}_f, \psi^{col}_f, Sync_f)}$
  \end{center}
  , where 
  \begin{enumerate}
  \item $\phi^{local}_f$ is the local pre-condition of the function
    contract, which is the conjunction of the set of expressions
    $\mymath{\{\texttt{!}A_{b_f} \texttt{ || } R_{b_f} \mid b_f \in
      B^{local}_f\}}$
  \item $\psi^{local}_f$ is the local post-condition of the function
    contract, which is the conjunction of the set of
    expressions\\ $\mymath{\{\texttt{!}A_{b_f} \texttt{ || (}
      E_{b_f}\texttt{ \&\& } var \texttt{ == \BSL{}old(}var\texttt{))}
      \mid var \in Var_g - Var_{b_f}, b_f \in B^{local}_f\}}$
  \item $\phi^{col}_f$ is the collective pre-condition of the function
    contract, which is the conjunction of the set of expressions
    $\mymath{\{\texttt{!}A_{b_f} \texttt{ || } R_{b_f} \mid b_f \in
      B^{col}_f\}}$
  \item $\psi^{col}_f$ is the collective post-condition of the function
    contract, which is the conjunction of the set of
    expressions\\ $\mymath{\{\texttt{!}A_{b_f} \texttt{ || (}
      E_{b_f}\texttt{ \&\& } var \texttt{ == \BSL{}old(}var\texttt{))}
      \mid var \in Var_g - Var_{b_f}, b_f \in B^{col}_f\}}$
  \item $\mymath{Sync_f}$ is a set of pairs $\mymath{\{(A_{b_f}, e) \mid
    e \in W_{b_f}, b_f \in B^{col}_f \}}$
  \end{enumerate}
  \label{defn:function-graph-with-contract}
\end{defn}


\subsection{Function Contract Semantics}
A contract clause has different meanings depending on whether it
belongs to local behaviors or collective behaviors.  We call contract
clauses that belong to local behaviors \emph{local contract clause}
and the ones that belong to collective behaviors \emph{collective
  contract clause}.  A local contract clause states properties for a
process state.  A collective contract clause states properties for a
state, including all process states and the communication channels.
According to the difference in their meanings, the following
constraints will be applied to local contract clauses: 
\begin{enumerate}
\item the remote operator \texttt{@} shall not be used in local contract clause
\item the \texttt{waitsfor} clause shall not be used in local
  behaviors of any function contract
\end{enumerate}

For a function contract, its local behaviors are assigned \emph{local
  contract semantics} while collective behaviors are assigned
\emph{collective contract semantics}.  The local contract semantics is
based on Hoare Logic.  It describes how does a process state change
before and after a function execution as if the process executes the
function sequentially.  Local behaviors can not fully express the
functional correctness of a MiniMP function including communications.
The functional correctness of communications, more specifically,
collective communications, will be described by collective behaviors
in a contract with collective contract semantics.  According to the
two kinds of semantics of function contracts, a MiniMP function
contract can be assigned to a function that either involves no
communication or only collective communications.  Collective
communications are the communication patterns in
\emph{collective-style} functions.  Informally, a collective-style
function is a function that requires to be called by all processes
collectively to complete a communication and guarantees that the
messages sent from these call instances will be received by these call
instances.  A typical example of a collective-style MiniMP function is
the \texttt{main} function.  In the rest of this section, we will
precisely define collective-style functions and contract semantics.

\subsubsection{Collective-style Functions} \label{sec:collective-style-function}
Function contracts that include collective behaviors can only be
assigned to collective-style functions.  A collective-style function,
in general, is a function that includes collective communications,
which requires all processes to participate.  A collective
communication that is started by a statement in a collective-style
function must be completed by a statement in the same function.

%% definition of collective state in terms of bulk-synchronous:
\textbf{Collective states}.  The definition of collective-style
functions, as well as the collective contract semantics, is based on a
notion---\emph{collective states}.  Let $\mymath{\coLoc{} \in P
  \mapsto Loc}$ be the functional relation that maps each process to a
desired location in a model $\model$.  We call $\mymath{\coLoc{}}$ a
collective mapping.  We will use $\coLoc{}_{\model}$ to explicitly
express the model $\model$ associated with the collective mapping when
it is not clear in the context.  Otherwise, we use $\coLoc{}$.  In an
execution $\mymath{\pi \in G_{\model}}$, a state $s$ is a collective
state if for every process $p$ in $s$ such that $\mymath{toploc(s, p)
  = \coLoc{}(p)}$.  Imagine that if there is a barrier at
$\mymath{\coLoc{}(p)}$ for every $p$, the state where all processes
stay their barriers is a collective state.

In an execution $\mymath{\pi \in G_{\model}}$ with $n$ processes, a
process $q$ may reach the location $\mymath{\coLoc{}(q)}$ $m$ times while
another process $q'$ reaches the location $\mymath{\coLoc{}(q')}$ $m'$
times. Note that $m$ is not necessarily equal to $m'$.  Let $m_p$ be
the number of times that each process $p \in [n]$ reaches its desired
location $\mymath{\coLoc{}(p)}$ in $\pi$.  Again, imagine that there is a
barrier in every location $\mymath{\coLoc{}(p)}$, there will be a number
$\mymath{min(m_0, m_1, ..., m_{n-1})}$ of collective states that are
associated with $\mymath{\coLoc{}}$ in $\pi$.  In each collective state,
every process $p$ is arriving at the location $\mymath{\coLoc{}(i)}$ at
$k$-th time, for $\mymath{0 < k < min(m_0, m_1, ..., m_{n-1})}$.  Let
$\mymath{coState(\coLoc{}, \pi, k)}$ denote a collective state that is
associated with a collective mapping $\mymath{\coLoc{}}$ where every
process $p$ is arriving at $\mymath{\coLoc{}(p)}$ at $k$-th time in an
execution $\pi$.  Specially, $\mymath{coState(\coLoc{}, \pi, k) = \xi}$
for $\mymath{0 = k \vee min(m_0, m_1, ..., m_{n-1}) \leq k}$.

However, in general, we cannot assume that such barriers exist.  For
an execution $\pi$, it is common that $\mymath{coState(\coLoc{}, \pi, k)
  \not\in States(\pi)}$.  A process $p$ can arrive and leave the
location $\mymath{\coLoc{}(p)}$ before another process $q$ arrives
$\mymath{\coLoc{}(q)}$.  But this does not mean that we can only talk
about collective states for a specific subset of executions of a model
or we have to modify the original model. In fact, it is always able to obtain
the set of collective states that is associated with a collective
mapping $\mymath{\coLoc{}}$ from any execution of $\model$.  We will
explain and define procedures for obtaining collective states in the
following paragraphs.

%% why collective states exist
Since MiniMP is a message-passing programming language, there is no
shared storage among processes.  In an execution of a model $\model$,
the process state of a process $p$ where $p$ visits location
$\mymath{\coLoc{}(p)}$ at $k$-th time is independent with any other
processes.  That is, the process state of $p$ will not be changed by
any transition associated with another process $q$.  Hence, the
process state of each process $p$ in $\mymath{coState(\coLoc{}, \pi,
  k)}$ is same as the process state of each $p$ in the state where $p$
visits $\mymath{\coLoc{}(p)}$ at $k$-th time separately.

%% procedure for a merged state:
The procedure $\mymath{coLabel(\rho, loc, p, k)}$, which depends on a
path $\rho$, a location $\mymath{loc}$, a process $p$ and a positive
integer $k$, labels a state $\mymath{s \in States(\rho)}$ where
process $p$ arrives at $\mymath{loc}$ at $k$-th time. 
\begin{center}
  \begin{itemize}
  \item[] $\mymath{coLabel(\rho, loc, p, k) =}$
  \item  $\mymath{src(t)}$, if $\mymath{\rho = t \circ \rho'}$ and $k = 1$ and $\mymath{toploc(src(t), p) = \coLoc{}(p)}$
  \item  $\mymath{dest(t)}$, if $\mymath{\rho = t \circ \rho'}$ and $k = 1$ and $\mymath{toploc(dest(t), p) = \coLoc{}(p)}$
  \item $\mymath{coLabel(\rho', loc, p, k-1)}$, if $\mymath{\rho = t
    \circ \rho'}$ and $k > 1$ and $\mymath{toploc(src(t), p) = loc}$
  \item $\mymath{coLabel(\rho', loc, p, k)}$, if $\mymath{\rho = t
    \circ \rho'}$ and $k > 0$ and $\mymath{toploc(src(t), p) \not= loc}$
  \item $\xi$, otherwise
  \end{itemize}
\end{center}

For an execution $\pi \in G_{\model}$ with $n$ processes, a collective
mapping $\mymath{\coLoc{}}$ and some integer $k$, we have
\begin{center}
$\mymath{\forall{p}.  proj_p(coLabel(\pi, \coLoc{}(p), p, k)) =
  proj_p(coState(\coLoc{}, \pi, k))}$, if
$\mymath{\forall{p}. coLabel(\pi, \coLoc{}(p), p, k) \not= \xi}$, $p \in [n]$
\end{center}

%% message channels:
Recall that a state consists of a set of process states and
communication channels.  The remaining problem is to find a way to
obtain the communication channels of $\mymath{coState{(\coLoc{}, \pi, k)}}$
from the execution $\pi$.

%% how to get collective states:
To figure out the communication channels in $\mymath{coState{(\coLoc{},
    \pi, k)}}$, we first think about the case that there is a barrier
at $\mymath{\coLoc{}(p)}$ for every process $p$.  Let $s$ be the state
where a process $q$ visits $\mymath{\coLoc{}(q)}$ at first time in an
execution $\pi$.  There is no state prior to $s$ where a process $q'$
visits $\mymath{\coLoc{}(q')}$.  In other words, process $q$ is the first
process that visits its mapped location $\mymath{\coLoc{}(q)}$ in the
execution.  Because of the barrier at $\mymath{\coLoc{}(q)}$, $q$ cannot
proceed hence it cannot update the channels until the arrival of other
processes.  Other processes may continue to change the channels in the
following states after $s$ via executing communication statements
until they arrive at their corresponding locations and get blocked
there.  When the last process $q''$ reaches $\mymath{\coLoc{}(q'')}$ at
state $s'$, we have $\mymath{s' = coState(\coLoc{}, \pi, 1)}$.  Similar
behaviors will be found for cases that processes visit specific
locations at the general $k$-th time.  This special case observation
directly leads to a procedure for constructing the communication
channels of a collective state $\mymath{coState(\coLoc{}, \pi, k)}$ from
a general execution $\pi$ (no assumption on the existence of
barriers): Starting from a copy $\mymath{chan}$ of the communication
channels in the state $\mymath{coLabel(\pi, \coLoc{}(p), p, k)}$, where
the first process $p$ visits $\mymath{\coLoc{}(p)}$ at $k$-th time, and
letting $\mymath{chan}$ keep been updated by the following transitions
associated to every other process $p'$ which has not $k$-th time
passed $\mymath{\coLoc{}(p')}$.  When all processes have $k$-th time
passed their corresponding locations, we are done with updating
$\mymath{chan}$.

Let $\mymath{coPath(\coLoc{}, \pi, k)}$ identify a sub-path
$t_0t_1...t_{m-1}$ of the execution $\pi \in G_{\model}$ with $n$
processes such that
\begin{itemize}
\item $\mymath{\exists{p}. src(t_0) = coLabel(\pi, \coLoc{}(p),
p, k), p \in [n]}$
\item $\mymath{\exists{p}. src(t_{m-1}) = coLabel(\pi, \coLoc{}(p),
p, k), p \in [n]}$
\item $\mymath{\forall{p}. coLabel(\pi, \coLoc{p}, p, k) \in States(t_0t_1...t_{m-1}), p \in [n]}$
\end{itemize}

%% general formal definition of a collective communication channels
By applying a procedure $\mymath{coBuild}$, a collective state
$\mymath{coState(\coLoc{}, \pi, k)}$ can be obtained from a
$\mymath{coPath(\coLoc{}, \pi, k)}$ and a functional relation
$\mymath{\eta_{\pi, k} \in [n] \mapsto State}$ that maps processes to
labeled states:
\begin{center}
$\mymath{\forall{p}. \eta_{\pi, k}(p) = coLabel(\pi,
  \coLoc{}(p), p, k), p \in [n]}$
\end{center}.
Let $s_0$ be the source state of the first transition in the
$\mymath{coPath(\coLoc{}, \pi, k)}$, we have
$\mymath{coState(\coLoc{}, \pi, k) = coBuild(s_0, coPath(\coLoc{},
  \pi, k), \eta_{\pi, k})}$.  The procedure $\mymath{coBuild}$ is
defined by
\begin{itemize}
\item[] $\mymath{coBuild(s, \rho, \eta) = }$
\item $s$, if $\rho = \epsilon$ or $\mymath{\forall{p}. \eta(p) = \xi, p \in [n]}$

\item $\mymath{coBuild(s[proj_p(s') / proj_p(s)], \rho, \eta[p \mapsto \xi])}$, if $\mymath{\rho
  = (s', p, e, s'') \circ \rho'}$ and for some $p \in [n]$ such that $\mymath{\eta(p) = s'}$

\item $\mymath{coBuild(next(s, p, e), \rho', \eta)}$, if $\mymath{\rho
  = (s', p, e, s'') \circ \rho'}$ and $\mymath{\eta(p) \not= \xi}$

\item $\mymath{coBuild(s, \rho', \eta)}$, otherwise while
  $\mymath{\rho = (s', p, e, s'') \circ \rho'}$
\end{itemize}


%% now we can define collective-style function:
Now we define collective-style functions:
\begin{defn}
  A MiniMP function $f$ is a collective-style function if and only if 
  \begin{center}
    $\mymath{\forall{\model, \pi, n, p, p', k}.\,}$
    $\mymath{coState(loc_{ref_f}, \pi, k) \not= \xi \wedge comm(coState(loc_{ref_f}, \pi, k))(p, p') = \epsilon }$,\\ if
    $\mymath{coState(loc_{0_f}, \pi, k) \not= \xi \wedge comm(coState(loc_{0_f}, \pi, k))(p, p') = \epsilon}$,\\
    for $\mymath{\pi \in G_{\model}, n \geq 0, p, p' \in [n], k \geq 0}$
  \end{center}
  \label{defn:collective-function}
\end{defn}
We call the collective state $\mymath{coState(loc_{0_f}, \pi, k)}$ a
collective pre-state of $f$ and $\mymath{coState(loc_{ret_f}, \pi,
  k)}$ a collective post-state of $f$.  If $\mymath{coState(\coLoc{},
  \pi, k) \not= \xi}$, every process $p$ visits $\mymath{\coLoc{}(p)}$
at least $k$ times in execution $\pi$.  We say that the communication
channels $\mymath{comm}$ are empty if $\mymath{\forall{p, p'}.\,
  comm(p, p') = \epsilon}$.  

Definition \ref{defn:collective-function} means that for a
collective-style function $f$, if a collective pre-state, where
message channels are empty, exists, a corresponding collective
post-state, where message channels are empty, will also exist.

\subsubsection{Contract Evaluation} \label{sec:contract-evaluation}
For evaluating expressions in function contracts, we define a new
evaluation relation $\myeval{~}_c$.  For an expression $e$ in a
function contract, $\myeval{e}_c \in State \times [n] \mapsto D \cup
2^\mathbb{Z}$.  $\myeval{e}_c$ is defined inductively as follows:

\begin{align}
  \myeval{\texttt{$e_0$ ..\ $e_1$}}_c(s, p) &= \{i \mid \myeval{e_0}(s, p) \leq i < \myeval{e_1}(s, p)\}\nonumber \\
  \myeval{\texttt{a[$e_0$ ..\ $e_1$]}}_c(s, p) &= \{\myeval{\texttt{a[$i$]}}(s, p) \mid \myeval{e_0}(s, p) \leq i < \myeval{e_1}(s, p)\}\nonumber \\
  \myeval{e_0~ \texttt{@}~
    e_1}_{c}(s, p) &= 
  \begin{cases}
    \mymath{\myeval{e_0}(s, \myeval{e_1}(s, p))}, &
    \text{if}~ \mymath{\myeval{e_1}(s, p)} \in \mymath{[n]} 
    \\ \textbf{UNDEF}, & \text{otherwise}
  \end{cases}
  \nonumber \\
  \myeval{\texttt{\BSL{}old(}e\texttt{)}}_c(s, p) &= 
  \begin{cases}
    \myeval{e}(coState(\pi,
    loc_{0_f}, k), p), & \text{if } \exists{\model, f, \pi, k}.\, s = coState(\pi,
    loc_{ret_f}, k), \\ & \text{for } \pi \in G_{\model}, k \geq 0
    \\ 
    \textbf{UNDEF}, & \text{otherwise}
  \end{cases}
  \nonumber \\
  \myeval{e}_{c}(s, p) &= \myeval{e}(s, p), \text{if $e$ does not have the above forms} \nonumber
\end{align}


\subsubsection{Contract Semantics} \label{sec:contract-semantics}
We use $\mymath{FG'_f \models C_f}$ to denote that a function $f$
satisfies its function contract $C_f$.  Specially, if there is no
communication statement in the function body of $f$, $f$ is considered
a local function.  Local functions can be assigned function contracts
that include only local contract.  For such a case, $\mymath{FG'_f
  \models C_f}$ has nothing different from a Hoare Triple hence we will
not have further discussion on such cases.  We will only discuss
$\mymath{FG'_f \models C_f}$ for the cases that $f$ is a
collective-style function.

\begin{defn}
  For a collective-style function $f$, $\mymath{FG'_f \models C_f}$ if
  and only if
  \begin{enumerate}
  \item $\mymath{\forall{\model, \pi, n, p, k}.\,}$
     $\mymath{coState(loc_{{ret}_f}, \pi, k) \not= \xi\, \wedge\,}$\\
     $\mymath{\myeval{\psi{}^f_{local}}_{col}(coState(loc_{{ret}_f}, \pi, k), p) = \textbf{T}\,\wedge\,}$
     $\mymath{\myeval{\psi{}^f_{col}}_{col}(coState(loc_{{ret}_f}, \pi, k), p) = \textbf{T}}$,
     $\mymath{\text{if } coState(loc_{0_f}, \pi, k) \not= \xi \,\wedge\,}$
     $\mymath{\myeval{\phi{}^f_{local}}_{col}(coState(loc_{0_f}, \pi, k), p) = \textbf{T} \,\wedge\,}$\\
     $\mymath{\myeval{\phi{}^f_{col}}_{col}(coState(loc_{0_f}, \pi, k), p) = \textbf{T}}$,\\
     $\mymath{\text{for } \pi \in G_{\model}, n \geq 0, p \in [n], k \geq 0}$

  \item $\mymath{\forall{\model, \pi, n, p, k, (a, e)}\,\exists{\rho, \rho', \rho''}.\,}$\\
    $\mymath{\pi = \rho \circ coLabel(\pi, loc_{0_f}, \myeval{e}_{col}, k) \circ \rho' \circ coLabel(\pi, loc_{ret_f}, p, k) \circ \rho''}$,\\
    if $\mymath{\myeval{a}_{col}(coState(loc_{{ret}_f}, \pi, k), p)} = \textbf{T}$, \\
    for $\mymath{\pi \in G_{\model}, n \geq 0, p \in [n], k \geq 0, (a, e) \in Sync_f}$
  \end{enumerate}
\label{defn:contract-satisfy}
\end{defn}

In Definition \ref{defn:contract-satisfy}, the first condition is
analogous to the meaning of Hoare Triples: if collective and local
pre-conditions hold in a collective pre-state of a collective-style
function, collective and local post-conditions will hold in the
collective post-state when all processes have completed the execution
of the function.  The second condition speaks of the semantics of the
synchronous behaviors: a process $p$ cannot leave a collective-style
function until the processes that $p$ waits for have all entered the
function.  Recall that expressions in \texttt{waitsfor} clauses
designate IDs of processes that every process waits for. 

\subsubsection{The \texttt{exchange} Example} \label{sec:contract-semantics-example}
We conclude this section by showing an execution $\pi$ of the MiniMP
program in Figure \ref{fig:example-exchange}.  We also show that the
$\pi$ does not violate the function contract of \texttt{exchange}.

The execution $\pi$ is presented in Figure
\ref{fig:example-exchange-pi}, it involves 2 processes and consists of
15 states.  All 15 states are listed below.  For simplicity, we use
$\mymath{\{~\}}$ to represent a function that always return
\textbf{UNDEF}; $\mymath{\{x_0 \mapsto d_0, x_1 \mapsto d_1, ...\}}$
to represent a function that maps $\mymath{x_0, x_1, ...}$ to
$\mymath{d_0, d_1, ...}$ respectively and maps elements outside of
$\mymath{\{v_0, v_1, ...\}}$ to \textbf{UNDEF}.

\begin{footnotesize}
\begin{align}
s_0\text{: }
  (&((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{~\}) \nonumber \\
s_1\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange},14, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{~\}) \nonumber \\
s_2\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 19, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{~\}) \nonumber \\
s_3\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 24, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{~\}) \nonumber \\
s_4\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 25, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_5\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 25, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange},14, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_6\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 25, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 19, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_7\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 25, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 24, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_8\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 25, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 25, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0, (1, 0) \mapsto 1\}) \nonumber \\
s_9\text{: }
  (&((\texttt{main}, 29, \{~\})
  (\texttt{exchange}, 26, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1, \texttt{buf} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 25, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_{10}\text{: }
  (&((\texttt{main}, 30, \{~\}),
  \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1, \texttt{buf} \mapsto 1\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 25, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_{11}\text{: }
  (&((~),
  \{~\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 25, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0\}), \nonumber \\
  &\{(0, 1) \mapsto 0\}) \nonumber \\
s_{12}\text{: }
  (&((~),
  \{~\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 26, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0, \texttt{buf} \mapsto 0\}), \nonumber \\
  &\{~\}) \nonumber \\
s_{13}\text{: }
  (&((~),
  \{~\}), \nonumber \\
  &((\texttt{main}, 30, \{~\}),
   \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0, \texttt{buf} \mapsto 0\}), \nonumber \\
  &\{~\}) \nonumber \\
s_{14}\text{: }
  (&((~),
  \{~\}), \nonumber \\
  &((~),
   \{~\}), \nonumber \\
  &\{~\}) \nonumber
\end{align}
\end{footnotesize}

\begin{figure}
  \begin{align}
    & t_0 : (s_0, 0, 29, \texttt{true}, \texttt{call exchange}, 14, s_1)      \nonumber \\
    & t_1 : (s_1, 0, 14, \texttt{!(PID == NPROCS - 1)}, \texttt{to = PID + 1}, 19, s_2)  \nonumber \\
    & t_2 : (s_2, 0, 19, \texttt{PID == 0}, \texttt{from = NPROCS - 1}, 24, s_3)  \nonumber \\
    & t_3 : (s_3, 0, 24, \texttt{true}, \texttt{send val to to}, 25, s_4)  \nonumber \\
    & t_4 : (s_4, 1, 29, \texttt{true}, \texttt{call exchange}, 14, s_5)  \nonumber \\
    & t_5 : (s_5, 1, 14, \texttt{PID == NPROCS - 1}, \texttt{to = 0}, 19, s_6)  \nonumber \\
    & t_6 : (s_6, 1, 19, \texttt{!(PID == 0)}, \texttt{from = PID - 1}, 24, s_7)  \nonumber \\
    & t_7 : (s_7, 1, 24, \texttt{true}, \texttt{send val to to}, 25, s_8)  \nonumber \\
    & t_8 : (s_8, 0, 25, \texttt{true}, \texttt{recv val from from}, 26, s_9)  \nonumber \\
    & t_9 : (s_9, 0, 26, \texttt{true}, \texttt{ret 0}, 30, s_{10})  \nonumber \\
    & t_{10} : (s_{10}, 0, 30, \texttt{true}, \texttt{ret 0}, 31, s_{11})  \nonumber \\
    & t_{11} : (s_{11}, 1, 25, \texttt{true}, \texttt{recv val from from}, 26, s_{12})  \nonumber \\
    & t_{12} : (s_{12}, 1, 26, \texttt{true}, \texttt{ret 0}, 30, s_{13})  \nonumber \\    
    & t_{13} : (s_{13}, 1, 30, \texttt{true}, \texttt{ret 0}, 31, s_{14})  \nonumber 
  \end{align}
  \caption{an execution with 2 processes of the MiniMP program in Figure \ref{fig:example-exchange}}
  \label{fig:example-exchange-pi}
\end{figure}

If we apply the $\mymath{coLabel}$ procedure to $\pi$, we will have
that $s_1$ and $s_9$ are labeled as where process 0 visits the entry
and the exit of \texttt{exchange} at first time.  Similar for $s_5$
and $s_12$ for process 1.  The path $t_1t_2t_3t_4$ is identified by
$\mymath{coPath(loc_{0_\texttt{exchange}}, \pi, 1)}$ and
$t_9t_{10}t_{11}$ is identified by
$\mymath{coPath(loc_{{ret}_\texttt{exchange}}, \pi, 1)}$.  Then if we
apply the $\mymath{coBuild}$ procedure, we obtain the collective pre-
and post-states:
\begin{align}
   co&State(loc_{0_\texttt{exchange}}, \pi, 1) = \nonumber \\
   (&((\texttt{main}, 29, \{~\})
   (\texttt{exchange},14, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
  &((\texttt{main}, 29, \{~\})
   (\texttt{exchange},14, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2\}), \nonumber \\
   &\{~\}) \nonumber \\
   co&State(loc_{{ret}_\texttt{exchange}}, \pi, 1) = \nonumber \\
   (&((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 26, \{\texttt{val} \mapsto 0\}), \{\texttt{PID} \mapsto 0, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 1, \texttt{from} \mapsto 1, \texttt{buf} \mapsto 1\}), \nonumber \\
   &((\texttt{main}, 29, \{~\})
   (\texttt{exchange}, 26, \{\texttt{val} \mapsto 1\}), \{\texttt{PID} \mapsto 1, \texttt{NPROCS} \mapsto 2, \texttt{to} \mapsto 0, \texttt{from} \mapsto 0, \texttt{buf} \mapsto 0\}), \nonumber \\
   &\{~\}) \nonumber 
\end{align}

Now we show that the contracts hold for $\pi$.  The pre-condition of
\texttt{exchange} are trivially \texttt{true}.  The post-condition of
\texttt{exchange} is \texttt{(!(PID > 0) || buf == val\@(PID-1)) \&\&
  (!(PID == 0) || buf == val\@(NPROCS-1))}.  For process 0, its
constant \texttt{PID} has value 0, so \texttt{(!(PID > 0) ||
  val\@(PID-1))} evaluates to \textbf{T}.  Since there are in total 2
processes, the constant \texttt{NPROCS} always has value 2.  On the
collective post-state, both variable \texttt{buf} of process 0 and
variable \texttt{val} of process 1 have value 1, so \texttt{(!(PID ==
  0) || buf == val\@(NPROCS-1))} evaluates to \textbf{T} for process
0.  Similarly, the post-condition will be evaluated to \textbf{T} on
the collective post-state for process 1 as well.

For process 0, the assumption \texttt{PID > 0} does not hold in any
state hence it only waits for process \texttt{NPROCS-1}, i.e. process
1.  Similarly, process 1 only waits for process 0.  Therefore, to show
that $\pi$ satisfies the synchronous behavior of the contract, we only
need to show that
\begin{enumerate}
\item The state ($s_5$), where process 1 enters \texttt{exchange},
  precedes the state ($s_9$) where process 0 is going to leave
  \texttt{exchange}.
\item The state ($s_1$), where process 0 enters \texttt{exchange},
  precedes the state ($s_{12}$) where process 1 is going to leave
  \texttt{exchange}.
\end{enumerate}