From: Mart Lubbers Date: Sun, 13 Nov 2016 11:57:26 +0000 (+0100) Subject: finish jml assignment X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=5f23f0394ea3dadddd3bb44f2e2651ad8c0358bb;p=ss1617.git finish jml assignment --- diff --git a/jml_esc/Amount.java b/jml_esc/Amount.java index dbcde87..2591183 100644 --- 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); + } } diff --git a/jml_esc/Bag.java b/jml_esc/Bag.java index b5bc38b..517ffcb 100644 --- a/jml_esc/Bag.java +++ b/jml_esc/Bag.java @@ -1,6 +1,6 @@ /* 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. @@ -14,106 +14,129 @@ 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 as abbreviation. 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. - + */ 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= 0; + + Bag(int[] input) { + if(input == null) + input = new int[0]; + n = input.length; + contents = new int[n]; + arraycopy(input, 0, contents, 0, n); + } + + Bag() { + contents = new int[0]; + n = 0; + } + // + // The example below is a bit nasty. + // NB this is a constructor, not a method. + // + Bag(Bag b) { + //CHANGED: Initialize object with empty bag, then check for + // null and then add. + this(); + if(b == null) + b = new Bag(); + this.add(b); + } + + + + void removeOnce(int elt) { + // CHANGED: off by one error + for (int i = 0; i < n; i++) { + if (contents[i] == elt ) { + n--; + contents[i] = contents[n]; + return; + } + } + } + + void removeAll(int elt) { + // CHANGED: off by one error + for (int i = 0; i < n; i++) { + if (contents[i] == elt ) { + n--; + contents[i] = contents[n]; + } + } + } + + int getCount(int elt) { + int count = 0; + // CHANGED: off by one error + 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) { + //CHANGED: Check that contents may be empty still + if (contents.length == 0){ + contents = new int[1]; + } else 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) { + // CHANGED: add null check + if(b != null){ + int[] new_contents = new int[n + b.n]; + arraycopy(contents, 0, new_contents, 0, n); + //CHANGED: off by one error on n + arraycopy(b.contents, 0, new_contents, n, b.n); + contents = new_contents; + } + } + + void add(int[] a) { + this.add(new Bag(a)); + } + + //@ requires srcOff >= 0 && destOff >= 0 && length >= 0; + //@ requires src != null && dest != null; + //@ requires srcOff + length <= src.length; + //@ requires destOff + length <= dest.length; + private static void arraycopy(int[] src, + int srcOff, + int[] dest, + int destOff, + int length) { + for(int i=0 ; i