public class Amount{

 private int cents;
//@ invariant cents < 100 && cents > -100;
 private int dollars;
//@ requires cents < 100 && cents > -100;
 public Amount(int dollars, int cents){
   this.dollars = dollars;
   this.cents = cents;
 }
//@ ensures \result != null;
 public Amount negate(){
   return new Amount(-this.dollars, -this.cents);
 }
 //@ requires a != null;
 public Amount subtract(Amount a){
   return this.add(a.negate());
 }
//@ requires a != null;
 public Amount add(Amount a){
   int new_dollars = dollars + a.dollars;
   int new_cents = cents + a.cents;
   if (new_cents < -100) {
      new_cents = new_cents + 100;
      new_dollars = new_dollars - 1;
      return new Amount(new_dollars,new_cents);
   }
   else if (new_cents > 100) {
      new_cents = new_cents - 100;
      new_dollars = new_dollars - 1;
      return new Amount(new_dollars,new_cents);
   }
   else if (new_cents < 0 && new_dollars > 0) {
       new_cents = new_cents + 100;
       new_dollars = new_dollars - 1;
       return new Amount(new_dollars,new_cents);
   }
   else if (new_cents > 0 && new_dollars < 0) {
       new_cents = new_cents - 100;
       new_dollars = new_dollars + 1;
       return new Amount(new_dollars,new_cents);
   }
 }

 public boolean equal(Amount a) {
   if (a==null) return false;
   else return (dollars == a.dollars && cents == a.cents);
 }

}

@@ -35,16 +35,17 @@
  cents;%0A
+ 
 //@ inva
@@ -79,16 +79,18 @@
 %3E -100;%0A
+ %0A
  private
@@ -107,47 +107,219 @@
 rs;%0A
-//@ requires cents %3C 100 && cents %3E -10
+ //@ invariant dollars %3E 0 ==%3E cents %3E= 0;%0A //@ invariant dollars %3C 0 ==%3E cents %3C= 0;%0A%0A //@ requires cents %3C 100 && cents %3E -100;%0A //@ requires dollars %3E 0 ==%3E cents %3E= 0;%0A //@ requires dollars %3C 0 ==%3E cents %3C= 
 0;%0A 
@@ -406,24 +406,25 @@
 = cents;%0A %7D%0A
+ 
 //@ ensures 
@@ -613,16 +613,17 @@
 ());%0A %7D%0A
+ 
 //@ requ

Add another invariant with requirement