Function Specification Environment.md

Definition

$$(\gamma, \Gamma)$$ A pair with [[Function Context]] $\gamma$ and [[Function Specification Context]] $\Gamma$.

• Adds pre & post conditions to functions. $${P} \ f( \ \overrightarrow{x} \ ) \ {Q} \text{ is the specification of } f( \ \overrightarrow{x} \ ) \text{ in } \Gamma$$