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.