Some generic feedback on the ESC/Java2 & JML exercise

- If a property is declared as invariant, there is no need to repeat
  it in pre- or postconditions.

- The method add(int elt) in Bag: The easy way to fix this method is
  to replace 2*n with 2*n+1

- The method add(Bag b) in Bag: there is a simple of-by-one error in
  the second call to array copy. A correct spec of arraycopy will
  point this out.

- In the second if-branch in the add method in the Amount class
  there is a logical flaw, namely in in

     new_cents = new_cents - 100;
     new_euros = new_euros - 1;

  Here if new_cents is DE-creased by 100 then the euros have to be
  IN-creased. This is a logic bug that ESC/Java2 will not find for
  you, if you just add some invariants. (If you'd try to give a
  complete functional specification, with a detailed post-condition
  for add, then the tool might be able to spot this flaw.) So brownie
  points for spotting & fixing this flaw.