An Abstract Type Variable is a variable which appears in type expressions and which is intended to keep track of all the current values (instances) of an abstract type. For instance, in the following:
Person : set of Entity := {}
Student : set of Person := {}
s : Student
assert s = Undefined and Student = Person = {}
s := New(Student)
assert s /= Undefined and Student = Person = {s}
both Person and Student are Abstract Type Variables.
As a side-effect of calling the pseudo-function, New, an abstract value is created and added to the (initially empty) set of values assigned to Student. Furthermore, since Student is constrained by its declaration to contain only a set of values of type Person, the new abstract value is also added (by New) to the (initially empty) set of values assigned to Person.
It is important to note that, at the time when the variable s is defined, its type expression results in the empty set, which means that no values (apart from Undefined) may legally be assigned to s. Nevertheless, the (not Undefined) abstract value returned by New is quite legally assigned to s in the next assignment instruction, because the type of s is actually specified by the variable Student, rather than by the value of Student at the time s was defined (see Type Expression for details).
The convention that a variable can be used to type another variable may seem extremely bizarre at first glance, but one soon gets used to it. The alternative would be to use one name to keep track of all the potential values of type Student, and another to keep track of the values than can actually be used. This soon becomes tedious, and furthermore makes it impossible to enforce referential integrity constraints by means of type checks.