next up previous contents
Next: Compositional verification Up: The refinement relation Previous: The refinement relation   Contents

Circular assignments

A circularity error occurs if there is a cycle of zero-delay assignments amongst the union of all assignments in all layers. Thus for example, the following program:

        layer Q : {
          x := y;
        }
        layer P : {
          y := x;
          next(x) := y;
        }
        P refines Q;
is erroneous, even though it is functionally equivalent to the non-circular program:
        y := x;
        next(x) := y;



2002-10-28