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 refered 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.