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.
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.
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);
+ }
}
/* 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.
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<length; i++) {
- dest[destOff+i] = src[srcOff+i];
- }
- }
-
+ /*@ non_null @*/ int[] contents;
+ int n; //@ invariant n <= contents.length && n >= 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<length; i++) {
+ dest[destOff+i] = src[srcOff+i];
+ }
+ }
+
}
repositories / ss1617.git / commitdiff