they have what they call model variables or ghost variables and the formula
An attempt at using model-based specification while at the same time being
independant of the implementation. Thus it has the easiness of model-based
specification and the generality of algebraic specification.
--
FL