$$\Gamma ::= \emptyset \ | \ \Gamma, {P} \ f( \ \overrightarrow{x} \ ) \ {Q} \quad \text{ where } \quad \begin{split}
& f( \ \overrightarrow{x} \ ) \text{ is not in } \Gamma \\
\land \ & pv(P) \subseteq { \ \overrightarrow{x} \ } \\
\land \ & pv(Q) = {\ ret \ }
\end{split}$$
- Contained within a [[Function Specification Environment]]