Living with free type and class union

There are two constructs in the formal specification language Object-Z for modelling polymorphic and recursive structures. One construct, the free type, is adopted from the Z specification language. The other, class-union, facilitates polymorphic class declarations. Free type and class-union constructs are respectively based upon the functional value point of view and the object reference point of view. Consequently, the roles these two constructs perform in system modelling are different. The free type and class-union constructs are compared and discussed through various examples. The aim of this comparison and discussion is to present guidelines on how to appropriately and effectively use these two constructs to specify polymorphic and recursive structures