In some cases, it may be necessary to introduce auxiliary signals that are used as part of the specification, or part of the proof, but do not belong to the system being verified. Such signals are introduced by the keyword abstract, as follows:
abstract <signal> : <type>
The implementation of a non-abstract signal may not depend on an abstract signal.