public class AccountWithEquality extends Account {

  /*@ requires amt >= 0;
    @ assignable bal;
    @ ensures bal == amt; @*/
  public AccountWithEquality(int amt) {
    super(amt);
  }
 
  /*@ assignable bal;
    @ ensures bal == acc.bal; @*/
  public AccountWithEquality(AccountWithEquality acc) {
    this(acc.balance());
  }

  public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object other) {
    if (this == other) {
      return true;
    }
    if (other == null) {
      return false;
    }
    if (getClass() != other.getClass()) {
      return false;
    }
    return balance() == ((AccountWithEquality) other).balance();
  }
}