Compositional verification

In order to verify a given assignment x//P, where x is a signal and P is layer, it is allowed to use any other assignment y//Q as an assumption (with one proviso, below). The syntax for this is:

        using x//P prove y//Q;

In this case, x//P is referred to as the ``assumption'' and y//Q as the ``guarantee''. The one restriction on the use of this statement is that if x and y are identical, then P must refine Q. Other than this, any use is allowed, including circularities. For example, it is legitimate to write:

        using x//P prove y//P;
        using y//P prove x//P;

As a example, suppose we have:

        layer P : {
          x := 0;
          y := 0;
        }
        layer Q : {
          init(x) := 0;
          next(x) := y;
          y := x;
        }
        Q refines P;
        using x//P prove y//P;
        using y//P prove x//P;

That is, in essence, the ``using'' declarations say that in order to prove that x is always zero, we can assume that y is always zero, and vice versa.