A Small Example

With these notion of check-code, auto-completion rules and associated guards we can now model a given predicate. Consider a HTML form involving three input fields of type text: p,q and r. These fields satisfy the relationship $\mathbb{R}$ given by a predicate P(p,q,r). The relationship is defined by the corresponding check-code C:

C $\equiv$ val(p) == val(q) / val(r)

A set of rules can now be given to model how a unknown field value can be deduced from a set of known field values. The complete set of rules and the corresponding modes and guards for the predicate P is shown in Figure 5.

Figure 5: A divide predicate with check-code and auto-completion rules and associated guards