\section{Procedure Contract System for
  \minimp{}} \label{sec:minimp:modular:system}

In this section, we discuss about the challenges in building a
verification system based on procedure contracts for \minimp{}
programs.  Instead of general program segments, the system allows the
user to only specify contracts to procedures.  Those contracts are
called \emph{procedure contracts}.

Recall that a program segment has no \texttt{\ccode{return}}
sub-statement.  But \texttt{\ccode{return}}s are important to
procedures.  In addition, different procedure calls have different
actual parameters.  It comes to the adaptation problem.  We explain
solutions to these problems in
\S\ref{sec:minimp:system:formal:return}.  We describe how to integrate
collective states to \emph{on the fly} model checking in
\S\ref{sec:minimp:system:onthefly}.  In \S\ref{sec:minimp:system:por},
we briefly talk about the verification of absence assertions and how
does the verification affect the partial order reduction problem.
Finally, we discuss about the infinite state space problem of model
checking in \S\ref{sec:minimp:system:limitation}.


\subsection{Formal Parameters and Return
  Value} \label{sec:minimp:system:formal:return}

In order to let the syntax of \minimp{} procedures accept contracts,
we modify the grammar of \minimp{} to:
\begin{center}
\begin{programNoNum}
  \nonterm{Procedure}~:=~\ccode{fun}~\nonterm{Identifier} (
  \nonterm{List-of-Identifiers} ) \nonterm{Spec}$\regxques$ \\
  \lb{}~\biglp{}\nonterm{List-of-Identifier}\bigrp{}$\regxques$
  ;~\nonterm{Statements}~\rb{}
\end{programNoNum}
\end{center}
Whether a procedure has a contract is optional.  Lexically, a contract
of a procedure follows the formal parameter declaration. It gives a
hint that formal parameters are visible to the contract.

\textbf{Formal Parameters.}  For a procedure contract, variables that
are visible to it are global variables and formal parameters.  Note
the local variables of the procedure are invisible to the contract.

However, formal parameters of a procedure $f$ are invisible to the
location where $f$ is called.  For example, given the following
procedure definition with a contract:
\begin{center}
  \begin{programNoNum}
    \ccode{int} f(\ccode{int} x) \\
    \ccode{requires} x > 0; \\
    \ldots{}
  \end{programNoNum}
\end{center}
Recall the adaptation problem.  Suppose we need to infer the behavior
of the call \texttt{f(a)}, we have to substitute the formal parameter
\texttt{x} with the actual parameter \texttt{a} in the contract of
\texttt{f}.

A natural solution to this problem follows the semantics of procedure
calls.  Whenever the contract of a procedure call needs to be
evaluated, a frame associated with the procedure will be pushed onto
the stack of the corresponding process, just like how is a call 
executed.  Then the contract will be evaluated in the context where
formal parameters are visible and have been assigned proper values
corresponding to the actual parameters.  Finally, after executing the
\myactrefresh{} statement, the process pops the frame and continues
its execution.

\textbf{Returned Values.}  In many cases, procedures return values.
Recall that program segments are defined to have no
\texttt{\ccode{return}} statement.  Hence there is no construct
defined in \minispec{} for accessing returned values.  For a
procedure, returned value carries the most important result delivered
by the functionality of the procedure.  A contract language without
construct for returned values is useless for procedures.

Therefore, we extended \minispec{} by adding \texttt{\acslresult} as a
specification expression to \nonterm{SpecExpr}.  This expression is
borrowed from ACSL.  It can only be used in the state-guarantee of a
procedure contract to refer the returned value.

Whenever the behavior of a procedure call has to be inferred from its
contract, \texttt{\acslresult} refers to a fresh new symbol
representing the arbitrary returned value.  The returned value usually
is constrained by the contract.  The symbol is then saved as the
returning value which will be assigned to a variable, if the call is
the right-hand side of an assignment.

\begin{exmp}
  Figure \ref{fig:minimp:contract:example:exchange} shows a \minimp{}
  procedure \texttt{exchange} with a contract.

  In the procedure, every process sends \texttt{a[1]} and
  \texttt{a[n-2]} to its \texttt{left} and \texttt{right} neighbor,
  respectively.  And, every process receives values from its
  \texttt{left} and \texttt{right} neighbors in \texttt{a[0]} and
  \texttt{a[n-1]}, respectively.

  In the contract, the state-requirement expresses that the
  ``neighbor-relation'' is well-defined, i.e., (1) a neighbor of a
  process must be one of the running processes; and (2) neighbors are
  mutual, i.e., every process is the \texttt{left} (resp.\
  \texttt{right}) neighbor of its \texttt{right} (resp.\
  \texttt{left}) neighbor.  Besides, the state-requirement requires
  that the length of the array \texttt{a} must be at least 4.  The
  state-guarantee states that the messages were sent and received by
  every process correctly, i.e., the returned value of every process
  will store the value of \texttt{a[1]} of its \texttt{right} neighbor
  in the \texttt{n-1}-th element, and stores the value of
  \texttt{a[n-2]} of its \texttt{left} neighbor in the \texttt{0}-th
  element.  The path guarantee states that a process cannot leave the
  procedure until both of its neighbors enter the procedure.

  By the contract, only two elements of \texttt{a} are modified by the
  procedure.  Since the returned value is actually \texttt{a}, the
  elements in the returned value excluding \texttt{\acslresult[0]} or
  \texttt{\acslresult[n-1]} remain their values in the pre-state.
  Since the returned value is an arbitrary fresh new symbol
  constrained by the state-guarantee, without the condition at line 9,
  one can never infer certain values in \texttt{\acslresult[1 .. n-2]}
  from this contract.  $\qed$
\end{exmp}


\begin{figure}[t]
  \begin{center}
  \begin{program}
    \ccode{fun} exchange(\ccode{var} a, n, left, right)\\
    \ \  \ccode{requires} 0 <= left \&\& left < NPROCS;\\
    \ \  \ccode{requires} 0 <= right \&\& right < NPROCS;\\
    \ \  \ccode{requires} \acslon(right, left) == PID \&\& \acslon(right, left) == PID;\\
    \ \ \ccode{requires}  4 <= n \&\& n == len(a);\\
    \ \  \ccode{assigns}  a[0], a[n-2];\\
    \ \  \ccode{ensures} \acslon(a[n-2], left) = \acslresult[0]
    \&\&
    \\
    \ \ \ \ \ \ \ \ \ \ \acslon(a[1], right) =
    \acslresult[n-1]; \\
    \ \ \ccode{ensures} \acslforall{} i; 1 <= i \&\& i < n-1 ==>
    \acslresult[i] = a[i];\\
    \ \ \ccode{ensures} \acslwaitsfor{\texttt{PID}}{\texttt{left}};\\
    \ \ \ccode{ensures} \acslwaitsfor{\texttt{PID}}{\texttt{right}};\\
    \lb{} \\
    \ \ send(a[1], left); \\
    \ \ recv(a[n-1], right);\\
    \ \ send(a[n-2], right); \\
    \ \ recv(a[0], left);\\
    \ \ \ccode{return} a;\\
    \rb{}
  \end{program}
  \end{center}
  \caption{A \minimp{} procedure \texttt{exchange} and its contract.}
  \label{fig:minimp:contract:example:exchange}
\end{figure}