LARA

Soft Typing

$\begin{equation*} \textsf{contract}(A,r,B) = (\forall x.\forall y. x \in A \land (x,y) \in r \rightarrow y \in B) \end{equation*}$

Note: this is weakest precondition, see Hoare Logic Basics

Example:

$\begin{equation*} {+} : \mathbb{C} \times \mathbb{C} \to \mathbb{C} \end{equation*}$

$\begin{equation*} \textsf{contract}(\mathbb{Z} \times \mathbb{Z}, {+}, \mathbb{Z}) \end{equation*}$

- Login

Trace: • soft_typing

projects/guru/soft_typing.txt · Last modified: 2015/04/21 17:34 (external edit)