[Next] [Up] [Previous] [Contents]
Next: Circular assignments Up: Refinements Previous: Refinements

The refinement relation

The refinement relation between layers is by definition transitive. Thus if we have:

        P refines Q;
        Q refines R;
then by implication
        P refines R;
The refinement relation may not be circular. Thus
        P refines P
is an error. The implementation of a signal is the assignment to that signal whose layer is minimal with respect to the refinement relation. If no unique minimal assignment to a signal exists, the program is in error.





Ken McMillan
Sat Jun 6 21:41:59 PDT 1998