add jml/esc source files

diff --git a/jml_esc/Amount.java b/jml_esc/Amount.java
new file mode 100644 (file)
index 0000000..dbcde87
--- /dev/null
+++ b/jml_esc/Amount.java
@@ -0,0 +1,99 @@
+
+/* ESC/Java2 exercise
+
+   Objects of this class represent euro amounts. For example, an Amount 
+   object with
+     euros == 1
+     cents == 55
+   represents 1.55 euro. 
+
+   Specify the class with JML and check it ESC/Java2.  
+
+   NB there may be errors in the code that you have to fix to stop 
+   ESC/Java2 from complaining, as these complaints of ESC/Java2 
+   point to real bugs in the code. But keep changes to the code to
+   a minimum of what is strictly needed. 
+   Mark any changes you have made in the code with a comment,
+   eg to indicate that you replaced <= by <.
+
+   You should add enough annotations to stop ESC/Java2 complaining,
+   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.
+
+   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.
+
+   The only JML keywords needed for this are
+      requires
+      invariant
+      ensures
+
+   If you want, you can also use
+      non_null
+
+   While 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.
+
+*/
+
+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);
+ }
+
+}

diff --git a/jml_esc/Bag.java b/jml_esc/Bag.java
new file mode 100644 (file)
index 0000000..b5bc38b
--- /dev/null
+++ b/jml_esc/Bag.java
@@ -0,0 +1,119 @@
+
+/* ESC/Java2 Exercise: 
+   
+   This class implements a Bag of integers, using an array.
+
+   Add JML specs to this class, to stop ESC/Java2 from complaining.
+
+   NB there may be errors in the code that you have to fix to stop 
+   ESC/Java2 from complaining, as these complaints of ESC/Java2 
+   point to real bugs in the code. But keep changes to the code to
+   a minimum of what is strictly needed. 
+   Mark any changes you have made in the code with a comment,
+   eg to indicate that you replaced <= by <.
+
+
+   The only JML keywords needed for this are
+      requires
+      invariant 
+      ensures 
+  
+   If you want, you can also use
+      non_null
+   as abbreviation.
+
+
+   While 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.
+  
+*/
+
+class Bag {
+
+  int[] contents;
+  int n;
+
+  Bag(int[] input) {
+    n = input.length;
+    contents = new int[n];
+    arraycopy(input, 0, contents, 0, n);
+  }
+
+  Bag() {
+    n =0;
+    contents = new int[0];
+  }
+
+  void removeOnce(int elt) {
+    for (int i = 0; i <= n; i++) {  
+      if (contents[i] == elt ) {
+         n--;
+         contents[i] = contents[n];
+         return;
+      }
+    }
+  }
+
+  void removeAll(int elt) {
+    for (int i = 0; i <= n; i++) {   
+      if (contents[i] == elt ) {
+         n--;
+         contents[i] = contents[n];
+      }
+    }
+  }
+
+  int getCount(int elt) {
+    int count = 0;
+    for (int i = 0; i <= n; i++) 
+      if (contents[i] == elt) count++; 
+    return count;
+  }
+
+  /* Warning: you may have a hard time checking the method "add" below.
+     ESC/Java2 may warn about a very subtle bug that can be hard to spot. 
+     If you cannot find the problem after staring at the code for an hour, 
+     feel free to stop.
+   */
+
+  void add(int elt) {
+    if (n == contents.length) {
+       int[] new_contents = new int[2*n]; 
+       arraycopy(contents, 0, new_contents, 0, n);
+       contents = new_contents;
+    }
+    contents[n]=elt;
+    n++;
+  }
+
+  void add(Bag b) {
+    int[] new_contents = new int[n + b.n];
+    arraycopy(contents, 0, new_contents, 0, n);
+    arraycopy(b.contents, 0, new_contents, n+1, b.n);
+    contents = new_contents; 
+  }
+
+  void add(int[] a) {
+    this.add(new Bag(a));
+  }
+
+  // The example below is a bit nasty.
+  // NB this is a constructor, not a method.
+  // 
+  // Bag(Bag b) {
+  //   this.add(b);    
+  // }
+
+  private static void arraycopy(int[] src,
+                                int   srcOff,
+                                int[] dest,
+                                int   destOff,
+                                int   length) {
+    for( int i=0 ; i<length; i++) {
+       dest[destOff+i] = src[srcOff+i];
+    }
+  }
+  
+}