From 72a0403299c707ea8b3eb2e6dff883cf2157c7a6 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 13 Nov 2016 11:05:06 +0100 Subject: [PATCH] add jml/esc source files --- jml_esc/Amount.java | 99 ++++++++++++++++++++++++++++++++++++ jml_esc/Bag.java | 119 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 218 insertions(+) create mode 100644 jml_esc/Amount.java create mode 100644 jml_esc/Bag.java diff --git a/jml_esc/Amount.java b/jml_esc/Amount.java new file mode 100644 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 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