Considerations when writing class invariants

Introduction

Class invariants can be an invaluable aid to developing bug-free code as discussed in Prof. Meyer's article Why not program right?, however there is a common pitfall in designing invariant conditions that should be kept in mind. It is easy to inadvertently write a precondition that gets in the way of an especially useful design pattern, that I like to call the "Conforming Instance Factory pattern". This "invariant gotcha" is mainly the fault of the compiler but in the absence of a change to the compiler can be remedied by a change to class design.

The Conforming Instance Factory Pattern

The Conforming Instance Factory Pattern is exemplified by the Eiffel-Loop class EL_OBJECT_FACTORY. This class offer a variety of ways to return a new initialised instance of a class from a given set of types conforming to a common base type. An example of it's use can be found in routine new_codec_by_id from class EL_ZCODEC_FACTORY. A simplified source listing is as follows:

class EL_ZCODEC_FACTORY inherit EL_FACTORY_CLIENT feature -- Access new_codec_by_id (id: INTEGER): EL_ZCODEC do Result := Codec_factory.instance_from_type (Codec_types [id], agent {EL_ZCODEC}.make) end feature {NONE} -- Constants Codec_types: HASH_TABLE [TYPE [EL_ZCODEC], INTEGER] once create Result.make (30) Result [1] := {EL_ISO_8859_1_ZCODEC} Result [2] := {EL_ISO_8859_2_ZCODEC} Result [3] := {EL_ISO_8859_3_ZCODEC} Result [4] := {EL_ISO_8859_4_ZCODEC} Result [5] := {EL_ISO_8859_5_ZCODEC} Result [6] := {EL_ISO_8859_6_ZCODEC} Result [7] := {EL_ISO_8859_7_ZCODEC} Result [8] := {EL_ISO_8859_8_ZCODEC} Result [9] := {EL_ISO_8859_9_ZCODEC} Result [10] := {EL_ISO_8859_10_ZCODEC} Result [11] := {EL_ISO_8859_11_ZCODEC} Result [13] := {EL_ISO_8859_13_ZCODEC} Result [14] := {EL_ISO_8859_14_ZCODEC} Result [15] := {EL_ISO_8859_15_ZCODEC} Result [1251] := {EL_WINDOWS_1251_ZCODEC} Result [1252] := {EL_WINDOWS_1252_ZCODEC} Result [1253] := {EL_WINDOWS_1253_ZCODEC} Result [1254] := {EL_WINDOWS_1254_ZCODEC} Result [1255] := {EL_WINDOWS_1255_ZCODEC} Result [1256] := {EL_WINDOWS_1256_ZCODEC} Result [1257] := {EL_WINDOWS_1257_ZCODEC} Result [1258] := {EL_WINDOWS_1258_ZCODEC} end Codec_factory: EL_OBJECT_FACTORY [EL_ZCODEC] once create Result end end

Incognizant Invariants

Now to analyse what is happening in routine new_codec_by_id and how incognizant invariants can sometimes "get in the way" of what it is trying to achieve. What this routine essentially does is make a call to

class REFLECTOR

  new_instance_of (type_id: INTEGER_32): ANY

and then cast the result to the type specified as the generic parameter G to EL_OBJECT_FACTORY, before initializing the object by calling a make routine from the parameter type, in this case {EL_ZCODEC}.make.

But a problem arises if EL_ZCODEC contains an invariant because the invariant will be called before the make routine has had a chance to initialize the class, invariably giving rise to an invariant violation.

Compiler Fix

A smarter compiler would realise that this agent is being applied as an initialization routine and would generate code that does not call the invariant condition prematurely.

Library Fix

But in the absence of a smarter compiler we can take a queue from the Vision2 class EV_ANY which suggests a solution to this problem via the routine is_initialized. Basically we can write all invariants using the following form:

invariant condition_name: is_initialized implies ...