finish jml assignment

[ss1617.git] / jml_esc / Amount.java

diff --git a/jml_esc/Amount.java b/jml_esc/Amount.java
index dbcde87..2591183 100644 (file)
--- a/jml_esc/Amount.java
+++ b/jml_esc/Amount.java
@@ -3,8 +3,8 @@
 
    Objects of this class represent euro amounts. For example, an Amount 
    object with
-     euros == 1
-     cents == 55
+   euros == 1
+   cents == 55
    represents 1.55 euro. 
 
    Specify the class with JML and check it ESC/Java2.  
@@ -20,31 +20,31 @@
    but you should ALSO specify invariants discussed below:
 
    1) We do not want to represent 1.55 euro as an object with
-         euro  == 0
-         cents == 155
-      (Note that the "equals" method will not be correct if we allow 
-       this.)
-      Specify an invariant that rules this out.
+   euro  == 0
+   cents == 155
+   (Note that the "equals" method will not be correct if we allow 
+   this.)
+   Specify an invariant that rules this out.
 
    2) We do not want to represent 1.55 euro as an object with
-         euros =  2
-         cents =  -45
-      Specify one (or more) invariant(s) that rule this out. But note that
-      we DO want to allow negative amounts, otherwise the method negate 
-      can't be allowed.
-      It may be useful to use the JML notation ==> (for implication) in 
-      your invariants.
+   euros =  2
+   cents =  -45
+   Specify one (or more) invariant(s) that rule this out. But note that
+   we DO want to allow negative amounts, otherwise the method negate 
+   can't be allowed.
+   It may be useful to use the JML notation ==> (for implication) in 
+   your invariants.
 
    The only JML keywords needed for this are
-      requires
-      invariant
-      ensures
+   requires
+   invariant
+   ensures
 
    If you want, you can also use
-      non_null
+   non_null
 
    While developing your specs, it may be useful to use the keywords
-      assert
+   assert
    to add additional assertions in source code, to find out what 
    ESC/Java2 can - or cannot - prove at a given program point.
 
@@ -52,48 +52,59 @@
 
 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 subtract(Amount a){
-   return this.add(a.negate());
- }
-
- public Amount add(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 equal(Amount a) {
-   if (a==null) return false;
-   else return (euros == a.euros && cents == a.cents);
- }
-
+       private int cents;
+       //@ invariant -100 < cents && cents < 100;
+
+       private int euros;
+       //@ invariant euros >= 0 ==> cents >= 0 && euros < 0 ==> cents <= 0;
+
+       //@ ensures -100 < cents && cents < 100;
+       //@ ensures euros >= 0 ==> cents >= 0 && euros < 0 ==> cents <= 0;
+       public Amount(int euros, int cents){
+               //CHANGED: Check if cents is of the correct sign
+               //         Make sure cents and euros are never over 100
+               if(euros >= 0 & cents < 0 | euros < 0 & cents > 0)
+                       cents = -cents;
+               this.euros = euros + cents/100;
+               this.cents = cents % 100;
+       }
+
+       public Amount negate(){
+               return new Amount(-cents,-euros); 
+       }
+
+       public Amount subtract(Amount a){
+               //CHANGED: Add a null check here.
+               return a == null ? this : this.add(a.negate());
+       }
+
+       public Amount add(Amount a){
+               //CHANGED: Add a null check here.
+               if(a == null)
+                       return this;
+               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 equal(Amount a) {
+               if (a==null) return false;
+               else return (euros == a.euros && cents == a.cents);
+       }
 }