public class BankAccount {

 static int nextAccountNr = 1;

 protected int accountnr;
 protected int balance; 
 protected int creditLimit; // minimum balance that is allowed
 protected int nextLogEntry; 
 
 protected int[] log; 

 public BankAccount(int bal, int limit){
  balance = bal;
  accountnr = nextAccountNr;
  creditLimit = limit;
  nextAccountNr++;
  log = new int[10];
 }

 public int getBalance(){
  return balance;
 }

 private void log(){
  log[nextLogEntry]=balance;
  nextLogEntry++;
  balance++;
  if (nextLogEntry==log.length) { nextLogEntry = 0; }
 }

 //@ ensures balance == \old(balance) - amount;
 public void debit(int amount) {
  log();
  if (balance-amount < creditLimit) {
  //    throw new DebitException();
  }
  balance=balance-amount;
 }

 //@ ensures balance == \old(balance) + amount;
 public void credit(int amount){
  log();
  balance=balance+amount;
 }

 //@ ensures balance == \old(balance) - amount;
 public void transfer(int amount, BankAccount dest) {
  debit(amount);
  dest.credit(amount);
 }

}