Contracts on fractions

README.md

@@ -5,9 +5,13 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
 
 ## List of semantically different functions with contracts
 
-- Class `math.IEEE754rUtils` (converted from Utility/"static" class to allow use of contracts):
+- Class `math.IEEE754rUtils`:
-  - `double min(double[])` and overloads 
+  - `static double min(double[])` and overloads 
-  - `double max(double[])` and overloads
+  - `static double max(double[])` and overloads
+- Class `math.Fraction`
+  - `static Fraction getFraction(int, int)` and `static Fraction getFraction(int, int, int)`
+  - `static Fraction getReducedFraction(int, int)`
+  - (TODO PICK OTHER 3 FROM HERE)
 - Class `CharRange`
   - `boolean contains(CharRange)`
 - Class `util.FluentBitSet`

src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java

@@ -137,6 +137,8 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      * @throws ArithmeticException if the denominator is {@code zero}
      * or the denominator is {@code negative} and the numerator is {@code Integer#MIN_VALUE}
      */
+    @Pure
+    @Requires("get_fraction_pre")
     public static Fraction getFraction(int numerator, int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");
@@ -167,6 +169,9 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      * @throws ArithmeticException if the resulting numerator exceeds
      *  {@code Integer.MAX_VALUE}
      */
+    @Pure
+    @Requires("get_fraction_whole_pre")
+    @Ensures("get_whole_fraction_post")
     public static Fraction getFraction(final int whole, final int numerator, final int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");
@@ -203,6 +208,8 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      * @return a new fraction instance, with the numerator and denominator reduced
      * @throws ArithmeticException if the denominator is {@code zero}
      */
+    @Requires("get_reduced_fraction_pre")
+    @Ensures("get_reduced_fraction_post")
     public static Fraction getReducedFraction(int numerator, int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");

src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java

@@ -21,5 +21,37 @@ package ch.usi.inf.sdm.sdm04.math;
 
 import ch.usi.si.codelounge.jsicko.Contract;
 
+@SuppressWarnings("unused") // used by jSicko
 public interface FractionContracts extends Contract {
+
+    @Pure
+    static boolean get_fraction_pre(final int numerator, final int denominator) {
+        return denominator != 0 && (denominator > 0 ||
+                (numerator != Integer.MIN_VALUE && denominator != Integer.MIN_VALUE));
+    }
+
+    @Pure
+    static boolean get_reduced_fraction_pre(final int numerator, final int denominator) {
+        return denominator != 0 && (numerator != 0 || denominator != Integer.MIN_VALUE);
+    }
+
+    @Pure
+    static boolean get_fraction_whole_pre(final int whole, final int numerator, final int denominator) {
+        final long numeratorValue = whole * (long) denominator + (long) (whole > 0 ? 1 : -1) * numerator;
+        return numerator >= 0 && denominator > 0 &&
+                numeratorValue >= Integer.MIN_VALUE && numeratorValue <= Integer.MAX_VALUE;
+    }
+
+    @Pure
+    static boolean get_reduced_fraction_post(final Fraction returns, final int numerator, final int denominator) {
+        final Fraction f = Fraction.getFraction(numerator, denominator);
+        return returns.compareTo(f) == 0;
+    }
+
+    @Pure
+    static boolean get_whole_fraction_post(final Fraction returns, final int whole, final int numerator, final int denominator) {
+        final long numeratorValue = whole * (long) denominator + (long) (whole < 0 ? -1 : 1) * numerator;
+        final Fraction calc = Fraction.getFraction((int) numeratorValue, denominator);
+        return returns.compareTo(calc) == 0;
+    }
 }

src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java

@@ -18,6 +18,7 @@
  */
 package ch.usi.inf.sdm.sdm04.math;
 
+import net.bytebuddy.implementation.bytecode.Throw;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.*;
@@ -54,7 +55,8 @@ public class FractionTest {
         assertEquals(Integer.MAX_VALUE, f.getNumerator());
         assertEquals(1, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).abs());
+        // changed to allow jSicko violations
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).abs());
     }
 
     @Test
@@ -420,13 +422,15 @@ public class FractionTest {
         assertEquals(10, f.getDenominator());
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-3, 0));
 
         // very large: can't represent as unsimplified fraction, although
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(4, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, Integer.MIN_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(4, Integer.MIN_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, Integer.MIN_VALUE));
     }
 
     @Test
@@ -452,25 +456,28 @@ public class FractionTest {
         assertEquals(2, f.getDenominator());
 
         // negatives
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
 
         // negative whole
         f = Fraction.getFraction(-1, 6, 10);
         assertEquals(-16, f.getNumerator());
         assertEquals(10, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -6, 10));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -6, 10));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, 6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -6, -10));
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(0, 1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(0, 1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 2, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -3, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-Integer.MAX_VALUE, 1, 2));
 
         // very large
         f = Fraction.getFraction(-1, 0, Integer.MAX_VALUE);
@@ -478,9 +485,10 @@ public class FractionTest {
         assertEquals(Integer.MAX_VALUE, f.getDenominator());
 
         // negative denominators not allowed in this constructor.
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(0, 4, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 1, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(0, 4, Integer.MIN_VALUE));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 2, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 1, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, 2, Integer.MAX_VALUE));
     }
 
     @Test
@@ -914,9 +922,10 @@ public class FractionTest {
         assertEquals(5, f.getDenominator());
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(-3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(-3, 0));
 
         // reduced
         f = Fraction.getReducedFraction(0, 2);
@@ -946,7 +955,8 @@ public class FractionTest {
         assertEquals(-(Integer.MIN_VALUE / 2), f.getDenominator());
 
         // Can't reduce, negation will throw
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(-7, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(-7, Integer.MIN_VALUE));
 
         // LANG-662
         f = Fraction.getReducedFraction(Integer.MIN_VALUE, 2);