jml_esc/AmountMartLubbers.java

   1 //Mart Lubbers s4109503
   2 /* ESC/Java2 exercise
   3
   4    Objects of this class represent euro amounts. For example, an Amount
   5    object with
   6    euros == 1
   7    cents == 55
   8    represents 1.55 euro.
   9
  10    Specify the class with JML and check it ESC/Java2.
  11
  12    NB there may be errors in the code that you have to fix to stop
  13    ESC/Java2 from complaining, as these complaints of ESC/Java2
  14    point to real bugs in the code. But keep changes to the code to
  15    a minimum of what is strictly needed.
  16    Mark any changes you have made in the code with a comment,
  17    eg to indicate that you replaced <= by <.
  18
  19    You should add enough annotations to stop ESC/Java2 complaining,
  20    but you should ALSO specify invariants discussed below:
  21
  22    1) We do not want to represent 1.55 euro as an object with
  23    euro  == 0
  24    cents == 155
  25    (Note that the "equals" method will not be correct if we allow
  26    this.)
  27    Specify an invariant that rules this out.
  28
  29    2) We do not want to represent 1.55 euro as an object with
  30    euros =  2
  31    cents =  -45
  32    Specify one (or more) invariant(s) that rule this out. But note that
  33    we DO want to allow negative amounts, otherwise the method negate
  34    can't be allowed.
  35    It may be useful to use the JML notation ==> (for implication) in
  36    your invariants.
  37
  38    The only JML keywords needed for this are
  39    requires
  40    invariant
  41    ensures
  42
  43    If you want, you can also use
  44    non_null
  45
  46    While developing your specs, it may be useful to use the keywords
  47    assert
  48    to add additional assertions in source code, to find out what
  49    ESC/Java2 can - or cannot - prove at a given program point.
  50
  51 */
  52
  53 public class Amount{
  54
  55         private int cents;
  56         //@ invariant -100 < cents && cents < 100;
  57
  58         private int euros;
  59         //@ invariant euros >= 0 ==> cents >= 0 && euros < 0 ==> cents <= 0;
  60
  61         //@ ensures -100 < cents && cents < 100;
  62         //@ ensures euros >= 0 ==> cents >= 0 && euros < 0 ==> cents <= 0;
  63         public Amount(int euros, int cents){
  64                 //CHANGED: Check if cents is of the correct sign
  65                 //         Make sure cents and euros are never over 100
  66                 if(euros >= 0 & cents < 0 | euros < 0 & cents > 0)
  67                         cents = -cents;
  68                 this.euros = euros + cents/100;
  69                 this.cents = cents % 100;
  70         }
  71
  72         public Amount negate(){
  73                 return new Amount(-cents,-euros);
  74         }
  75
  76         public Amount subtract(Amount a){
  77                 //CHANGED: Add a null check here.
  78                 return a == null ? this : this.add(a.negate());
  79         }
  80
  81         public Amount add(Amount a){
  82                 //CHANGED: Add a null check here.
  83                 if(a == null)
  84                         return this;
  85                 int new_euros = euros + a.euros;
  86                 int new_cents = cents + a.cents;
  87                 if (new_cents < -100) {
  88                         new_cents = new_cents + 100;
  89                         new_euros = new_euros - 1;
  90                 }
  91                 if (new_cents > 100) {
  92                         new_cents = new_cents - 100;
  93                         new_euros = new_euros - 1;
  94                 }
  95                 if (new_cents < 0 && new_euros > 0) {
  96                         new_cents = new_cents + 100;
  97                         new_euros = new_euros - 1;
  98                 }
  99                 if (new_cents >= 0 && new_euros <= 0) {
 100                         new_cents = new_cents - 100;
 101                         new_euros = new_euros + 1;
 102                 }
 103                 return new Amount(new_euros,new_cents);
 104         }
 105
 106         public boolean equal(Amount a) {
 107                 if (a==null) return false;
 108                 else return (euros == a.euros && cents == a.cents);
 109         }
 110 }