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