diff --git a/README.md b/README.md index 1cfe1d2..685c363 100644 --- a/README.md +++ b/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): - - `double min(double[])` and overloads - - `double max(double[])` and overloads +- Class `math.IEEE754rUtils`: + - `static double min(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` @@ -23,7 +27,7 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638` - (TODO) `FluentBitSet set(int)` - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` - + ## Run Tests ``` diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java b/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java index 74af790..69d3d20 100644 --- a/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java +++ b/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java @@ -137,6 +137,8 @@ public final class Fraction extends Number implements Comparable, 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, 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, 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"); diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java b/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java index 17c6dfb..4921426 100644 --- a/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java +++ b/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; + } } diff --git a/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java b/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java index 3c294e1..beb9587 100644 --- a/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java +++ b/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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(2, 0)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-3, 0)); + // changed to allow jSicko violations + assertThrows(Throwable.class, () -> Fraction.getFraction(1, 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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, Integer.MIN_VALUE)); + // changed to allow jSicko violations + 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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10)); + // changed to allow jSicko violations + assertThrows(Throwable.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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 6, -10)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -6, -10)); + // changed to allow jSicko violations + assertThrows(Throwable.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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 2, 0)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -3, 0)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MAX_VALUE, 1, 2)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-Integer.MAX_VALUE, 1, 2)); + // changed to allow jSicko violations + assertThrows(Throwable.class, () -> Fraction.getFraction(0, 1, 0)); + assertThrows(Throwable.class, () -> Fraction.getFraction(1, 2, 0)); + assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -3, 0)); + 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)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 1, Integer.MAX_VALUE)); - assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 2, Integer.MAX_VALUE)); + // changed to allow jSicko violations + assertThrows(Throwable.class, () -> Fraction.getFraction(0, 4, Integer.MIN_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)); - assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(2, 0)); - assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(-3, 0)); + // changed to allow jSicko violations + assertThrows(Throwable.class, () -> Fraction.getReducedFraction(1, 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);