/* ESC/Java2 exercise

   Objects of this class represent euro amounts; eg an amount with
     cents = 55
     euros = 1
   represents 1.55 euro

   Specify the class with JML and check it ESC/Java2.  
   NB There are a few bugs in the code that you will have to repair,
   but you should find these while using ESC/Java2.
 
   You should include the invariants discussed below in your JML
   specification:

   1) The cents field should always be between -100 and 100.  
      We allow negative cents fields in order to have negative amounts; 
      eg. an amount with
        cents = -55
        euros = -1
      represents -1.55 euro

   2) We do not want to represent -1.55 euro as an object with
       cents =  45
       euros = -2
      and we do not want to represent 1.55 euro as an object with
       cents = -45
       euros =  2
      (The "equals" method will not be correct if we allow this.)
      So specify an invariant disallowing the bad representations
      mentioned above, ie. those with a negative cents field and a
      positive euros field or vice versa

   The only JML keywords needed for this are
      requires
      invariant
      ensures

   If you want, you can also use
      non_null

   In developing your specs, it may be useful to use the keywords
      assert
   to add additional assertions in source code, to find out what 
   ESC/Java2 can - or cannot - prove at a given program point.
  

   Once ESC/Java2 no longer complains, try to add some interesting 
   postconditions to methods, using the keyword 
     ensures

*/

public class Amount{

 private int cents;

 private int euros;
 
 public Amount(int euros, int cents){
   this.euros = euros;
   this.cents = cents;
 }

 public Amount negate(){
   return new Amount(-cents,-euros); 
 }

 public Amount decrease(Amount a){
   return this.increase(a.negate());
 }

 public Amount increase(Amount a){
   int new_euros = euros + a.euros;
   int new_cents = cents + a.cents; 
   if (new_cents < -100) {  
      new_cents = new_cents + 100;
      new_euros = new_euros - 1;
   } 
   if (new_cents > 100) {  
      new_cents = new_cents - 100;
      new_euros = new_euros - 1;
   } 
   if (new_cents < 0 && new_euros > 0) { 
       new_cents = new_cents + 100; 
       new_euros = new_euros - 1;
   } 
   if (new_cents >= 0 && new_euros <= 0) {
       new_cents = new_cents - 100; 
       new_euros = new_euros + 1;
   }
   return new Amount(new_euros,new_cents);
 }

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

}