Invariant properties -- algebraic laws
class employee { employee
public:
employee( int n = 0 ) : sal(n) { }
employee* salary(int n) { sal = n; return this; }
virtual long salary() { return sal; }
protected:
int sal;
};
Invariant
k == (e->salary(k))->salary()
slide: Invariant properties as algebraic laws
Invariant properties are often conveniently
expressed in the form of algebraic laws that must
hold for an object.
Naturally, when extending a class by inheritance
(to define a specialization or refinement)
the invariants pertaining to the base class
should not be disrupted.
Although we cannot give a general guideline
to prevent disruption, the example discussed here clearly
suggests that hidden features should be carefully
checked with respect to the invariance properties
of the (derived) class.
The example is taken from [Bar92].
In slide [object-invariant], we have defined a class employee.
The main features of an employee are the (protected)
attribute sal (storing the salary of an employee)
and the methods to access and modify the salary
attribute.
For employee objects,
the invariant (expressing that any amount k
is equal to the salary of an employee whose
salary has been set to k)
clearly holds.
Now imagine that we distinguish between ordinary employees
and managers by adding a permanent
bonus when paying the salary of a manager,
as shown in slide [hidden-bonus].
The reader may judge whether this example is realistic or not.
Problem -- hidden bonus
class manager : public employee { manager
public:
long salary() { return sal + 1000; }
};
Invariant
k =?= (m->salary(k))->salary()
slide: Violating the invariant
Then, perhaps somewhat to our surprise, we find that
the invariant stated for employees no longer
holds for managers.
From the perspective of predictable object behavior
this is definitely undesirable, since invariants
are the cornerstone of reliable software.
The solution to this anomaly is to make the assignment
of a bonus explicit, as shown in slide [explicit-bonus].
Solution -- explicit bonus
class manager : public employee { manager'
public:
manager* bonus(int n) { sal += n; return this; }
};
Invariant -- restored
k + n == ((m->salary(k))->bonus(n))->salary()
slide: Restoring the invariant
Now, the invariant pertaining to managers may be strengthened
by including the effects of assigning a bonus.
As a consequence, the difference in salary
no longer occurs as if by magic but is directly
visible in the interaction with a manager object, as it should be.