Notice that the case of the circular buffer, we don't really have to send the byte indices, since they can be inferred from the ordering property of the interface. The data output doesn't depend on them. Thus, in the actual implementation, we would leave out the idx output of the buffer, considering it only an ``auxiliary'' variable used in the verification. This use of ``auxiliary state'' added to the implementation gives us a convenient way to specify interfaces as a function of abstract models. The auxiliary information tells us which object in the abstract model is currently appearing at the interface. This in turn allows us to specify what data should be appear at the interface as a function of the abstract model. In the next section, we'll see a slightly different way to do this.
We can tell SMV that a given variable is part of the proof only, and not part of the actual implementation, by declaring it as abstract. For example, in the byte_intf module, we would declare the idx component as:
abstract idx : INDEX;
SMV will verify for us that no actual implementation logic depends on this variable. The abstract variables can thus be excised from the implementation while retaining all the properties we've proved.