jml_esc/Amount.java

   1
   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
  57  private int euros;
  58
  59  public Amount(int euros, int cents){
  60    this.euros = euros;
  61    this.cents = cents;
  62  }
  63
  64  public Amount negate(){
  65    return new Amount(-cents,-euros);
  66  }
  67
  68  public Amount subtract(Amount a){
  69    return this.add(a.negate());
  70  }
  71
  72  public Amount add(Amount a){
  73    int new_euros = euros + a.euros;
  74    int new_cents = cents + a.cents;
  75    if (new_cents < -100) {
  76       new_cents = new_cents + 100;
  77       new_euros = new_euros - 1;
  78    }
  79    if (new_cents > 100) {
  80       new_cents = new_cents - 100;
  81       new_euros = new_euros - 1;
  82    }
  83    if (new_cents < 0 && new_euros > 0) {
  84        new_cents = new_cents + 100;
  85        new_euros = new_euros - 1;
  86    }
  87    if (new_cents >= 0 && new_euros <= 0) {
  88        new_cents = new_cents - 100;
  89        new_euros = new_euros + 1;
  90    }
  91    return new Amount(new_euros,new_cents);
  92  }
  93
  94  public boolean equal(Amount a) {
  95    if (a==null) return false;
  96    else return (euros == a.euros && cents == a.cents);
  97  }
  98
  99 }