Problem
-- hidden bonus
class manager : public employee {
manager
public: long salary() { return sal + 1000; } };
Invariant
k =?= (m->salary(k))->salary()
slide
:
Violating the invariant
