// @(#)$Id: PlusAccount.pri,v 1.4 1997/07/24 21:49:14 leavens Exp $
// Private members of PlusAccount

private:
  Money * chk_bal;

  //@ invariant assigned(chk_bal, any);
  //@ depends checking on *(chk_bal\any);
  //@ invariant checking\any = (*(chk_bal\any))\any;