int deposit(acct_no acct, int amt)
   semantics
   {
      balance(acct) == @balance(acct) + amt,
      return == balance(acct)
   };