Specification Patterns

As in the Bandera project [6] specification patterns are used to facilitate formulating correctness properties. These specification patterns concern temporal properties of method invocations, and are either temporal patterns or judgement patterns concerning the invocation of a particular method. Below a set of patterns that we have defined, and which are commonly used, are given.

To express that within the call of a method $m$ the property $\phi$ holds the judgment pattern

$$\mathsf{Within}\;m\;\phi \;\stackrel {\Delta}{=}\; m \vdash \phi$$

is used. The property that a call to $m_1$ never triggers method $m_2$ can be specified as:

$$\begin{array}{l} \multicolumn{1}{l}{m_1\;\mathsf{never}\;\ma... ...;m_1\;(\mathsf{never}\;\mbox{\sf loc}_{\>} m_2)\\ \end{array}$$

Next define the temporal patterns (formulas) (i) $m_2\;\mathsf{after}\;m_1$, i.e., $m_2$ can only be called after a call to $m_1$; (ii) $m_2\;\mathsf{through}\;m_1$, i.e., $m_2$ can only be called from $m_1$; (iii) $m_2\;\mathsf{from}\;m_1$, i.e., $m_2$ can only be called directly from $m_1$; and (iv) $m_1\;\mathsf{excludes}\;m_1$, i.e., when $m_1$ is called this excludes the possibility that $m_2$ will later be called; (v) $p\;\mathsf{cannotCall}\;m$, i.e., the method $m$ cannot be directly called from any method in package $p$.

$$\begin{array}{l} \multicolumn{1}{l}{m_2\;\mathsf{after}\;m_1... ...athsf{next}\;\neg \mbox{\sf loc}_{\>} m\right) \\ \end{array}$$

The intuitive idea of the formulation of $m_2\;\mathsf{from}\;m_1$ is to express that the current program point can be in method $m_2$ only because of a direct call from $m_1$, or because it was already in $m_2$, and initially the program point is not in $m_2$.

The above patterns can be combined with the $\mathsf{Within}$ pattern. For example,

$$\mathsf{Within}\;m_1\;\left(m_3\;\mathsf{after}\;m_2\right)$$

expresses that during a call to $m_1$ the method $m_3$ will be called only after calling $m_2$.

An alternative technique for expressing correctness properties of behaviours of programs of stack-based languages is to use stack inspection techniques [13]. Essentially these techniques express constraints on the set of all possible runtime stacks. Note however that for instance the $\mathsf{after}$ property above cannot directly be coded as a stack inspection property since the calls to $m_1$ and $m_2$ need not be concurrent.