More contracts

README.md

@@ -3,6 +3,27 @@
 Classes come from [https://github.com/apache/commons-lang](https://github.com/apache/commons-lang)
 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 `CharRange`
+  - `boolean contains(CharRange)`
+- Class `util.FluentBitSet`
+  - `FluentBitSet and(FluentBitSet)` and overloads
+  - `FluentBitSet andNot(FluentBitSet)` and overloads
+  - `FluentBitSet or(FluentBitSet)` and overloads
+  - `FluentBitSet clear()` and overloads
+  - `boolean get(int)` and overloads
+  - `boolean isEmpty()`
+  - `FluentBitSet flip(int)` and overloads
+  - (TODO) `FluentBitSet xor(FluentBitSet)`
+  - (TODO) `byte[] toByteArray()` and `byte[] toLongArray()`
+  - (TODO) `FluentBitSet set(int)` 
+  - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)`
+  - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)`
+  
 ## Run Tests
 
 ```

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

@@ -32,7 +32,7 @@ import java.util.Objects;
  *
  * @since 2.0
  */
-public final class Fraction extends Number implements Comparable<Fraction> {
+public final class Fraction extends Number implements Comparable<Fraction>, FractionContracts {
 
     /**
      * Required for serialization support. Lang version 2.0.
@@ -309,7 +309,6 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @throws NullPointerException if the string is {@code null}
      * @throws NumberFormatException if the number format is invalid
      */
-
     public static Fraction getFraction(String str) {
         Objects.requireNonNull(str, "str");
         // parse double format
@@ -351,7 +350,6 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      *
      * @return the numerator fraction part
      */
-
     public int getNumerator() {
         return numerator;
     }
@@ -401,7 +399,6 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      *
      * @return the whole number fraction part
      */
-
     @Override
     public int intValue() {
         return numerator / denominator;
@@ -845,6 +842,7 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @throws NullPointerException if the object is {@code null}
      */
     @Override
+    @Pure
     public int compareTo(final Fraction other) {
         if (this == other) {
             return 0;

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

@@ -0,0 +1,25 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04.math;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+public interface FractionContracts extends Contract {
+}

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

@@ -40,7 +40,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      */
     @Requires("non_null_non_empty_arg")
     @Ensures("is_minimum_element")
-    public double min(final double... array) {
+    public static double min(final double... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
 
@@ -64,7 +64,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      */
     @Requires("non_null_non_empty_arg_float")
     @Ensures("is_minimum_element_float")
-    public float min(final float... array) {
+    public static float min(final float... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
 
@@ -88,7 +88,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the smallest of the values
      */
     @Ensures("is_minimum_element_3")
-    public double min(final double a, final double b, final double c) {
+    public static double min(final double a, final double b, final double c) {
         return min(min(a, b), c);
     }
 
@@ -102,7 +102,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the smallest of the values
      */
     @Ensures("is_minimum_element_2")
-    public double min(final double a, final double b) {
+    public static double min(final double a, final double b) {
         if (Double.isNaN(a)) {
             return b;
         }
@@ -123,7 +123,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the smallest of the values
      */
     @Ensures("is_minimum_element_3_float")
-    public float min(final float a, final float b, final float c) {
+    public static float min(final float a, final float b, final float c) {
         return min(min(a, b), c);
     }
 
@@ -137,7 +137,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the smallest of the values
      */
     @Ensures("is_minimum_element_2_float")
-    public float min(final float a, final float b) {
+    public static float min(final float a, final float b) {
         if (Float.isNaN(a)) {
             return b;
         }
@@ -158,7 +158,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      */
     @Requires("non_null_non_empty_arg")
     @Ensures("is_maximum_element")
-    public double max(final double... array) {
+    public static double max(final double... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
 
@@ -182,7 +182,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      */
     @Requires("non_null_non_empty_arg_float")
     @Ensures("is_maximum_element_float")
-    public float max(final float... array) {
+    public static float max(final float... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
 
@@ -206,7 +206,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the largest of the values
      */
     @Ensures("is_maximum_element_3")
-    public double max(final double a, final double b, final double c) {
+    public static double max(final double a, final double b, final double c) {
         return max(max(a, b), c);
     }
 
@@ -220,7 +220,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the largest of the values
      */
     @Ensures("is_maximum_element_2")
-    public double max(final double a, final double b) {
+    public static double max(final double a, final double b) {
         if (Double.isNaN(a)) {
             return b;
         }
@@ -241,7 +241,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the largest of the values
      */
     @Ensures("is_maximum_element_3_float")
-    public float max(final float a, final float b, final float c) {
+    public static float max(final float a, final float b, final float c) {
         return max(max(a, b), c);
     }
 
@@ -255,7 +255,7 @@ public class IEEE754rUtils implements IEEE754rUtilsContracts {
      * @return the largest of the values
      */
     @Ensures("is_maximum_element_2_float")
-    public float max(final float a, final float b) {
+    public static float max(final float a, final float b) {
         if (Float.isNaN(a)) {
             return b;
         }

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

@@ -27,72 +27,72 @@ import java.util.stream.IntStream;
 @SuppressWarnings("unused") // methods used by jSicko
 public interface IEEE754rUtilsContracts extends Contract {
     @Pure
-    default boolean non_null_non_empty_arg(final double[] array) {
+    static boolean non_null_non_empty_arg(final double[] array) {
         return array != null && array.length > 0;
     }
 
     @Pure
-    default boolean non_null_non_empty_arg_float(final float[] array) {
+    static boolean non_null_non_empty_arg_float(final float[] array) {
         return array != null && array.length > 0;
     }
 
     @Pure
-    default boolean is_minimum_element(final double returns, final double[] array) {
+    static boolean is_minimum_element(final double returns, final double[] array) {
         return DoubleStream.of(array).filter(value -> !Double.isNaN(value)).allMatch(e -> returns <= e);
     }
 
     @Pure
-    default boolean is_maximum_element(final double returns, final double[] array) {
+    static boolean is_maximum_element(final double returns, final double[] array) {
         return DoubleStream.of(array).filter(value -> !Double.isNaN(value)).allMatch(e -> returns >= e);
     }
 
     @Pure
-    default boolean is_minimum_element_float(final float returns, final float[] array) {
+    static boolean is_minimum_element_float(final float returns, final float[] array) {
         return is_minimum_element(returns, IntStream.range(0, array.length).mapToDouble(i -> array[i]).toArray());
     }
 
     @Pure
-    default boolean is_maximum_element_float(final float returns, float[] array) {
+    static boolean is_maximum_element_float(final float returns, float[] array) {
         return is_maximum_element(returns, IntStream.range(0, array.length).mapToDouble(i -> array[i]).toArray());
     }
 
     @Pure
-    default boolean is_minimum_element_2(final double returns, final double a, final double b) {
+    static boolean is_minimum_element_2(final double returns, final double a, final double b) {
         return is_minimum_element(returns, new double[] { a, b });
     }
 
     @Pure
-    default boolean is_minimum_element_3(final double returns, final double a, final double b, final double c) {
+    static boolean is_minimum_element_3(final double returns, final double a, final double b, final double c) {
         return is_minimum_element(returns, new double[] { a, b, c });
     }
 
     @Pure
-    default boolean is_minimum_element_2_float(final float returns, final float a, final float b) {
+    static boolean is_minimum_element_2_float(final float returns, final float a, final float b) {
         return is_minimum_element(returns, new double[] { a, b });
     }
 
     @Pure
-    default boolean is_minimum_element_3_float(final float returns, final float a, final float b, final float c) {
+    static boolean is_minimum_element_3_float(final float returns, final float a, final float b, final float c) {
         return is_minimum_element(returns, new double[] { a, b, c });
     }
 
     @Pure
-    default boolean is_maximum_element_2(final double returns, final double a, final double b) {
+    static boolean is_maximum_element_2(final double returns, final double a, final double b) {
         return is_maximum_element(returns, new double[] { a, b });
     }
 
     @Pure
-    default boolean is_maximum_element_3(final double returns, final double a, final double b, final double c) {
+    static boolean is_maximum_element_3(final double returns, final double a, final double b, final double c) {
         return is_maximum_element(returns, new double[] { a, b, c });
     }
 
     @Pure
-    default boolean is_maximum_element_2_float(final float returns, final float a, final float b) {
+    static boolean is_maximum_element_2_float(final float returns, final float a, final float b) {
         return is_maximum_element(returns, new double[] { a, b });
     }
 
     @Pure
-    default boolean is_maximum_element_3_float(final float returns, final float a, final float b, final float c) {
+    static boolean is_maximum_element_3_float(final float returns, final float a, final float b, final float c) {
         return is_maximum_element(returns, new double[] { a, b, c });
     }
 }

src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSet.java

@@ -26,6 +26,7 @@ import java.util.stream.IntStream;
  * <p>
  * Originally from Apache Commons VFS with more added to act as a fluent replacement for {@link BitSet}.
  * </p>
+ *
  * @since 3.13.0
  */
 public final class FluentBitSet implements Cloneable, Serializable, FluentBitSetContracts {
@@ -153,9 +154,10 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bits specified by the indexes to {@code false}.
      *
      * @param bitIndexArray the index of the bit to be cleared.
-     * @throws IndexOutOfBoundsException if the specified index is negative.
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("valid_indexes")
     public FluentBitSet clear(final int... bitIndexArray) {
         for (final int e : bitIndexArray) {
             this.bitSet.clear(e);
@@ -167,9 +169,10 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bit specified by the index to {@code false}.
      *
      * @param bitIndex the index of the bit to be cleared.
-     * @throws IndexOutOfBoundsException if the specified index is negative.
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("get_int")
     public FluentBitSet clear(final int bitIndex) {
         bitSet.clear(bitIndex);
         return this;
@@ -180,11 +183,12 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * {@code false}.
      *
      * @param fromIndex index of the first bit to be cleared.
-     * @param toIndex index after the last bit to be cleared.
+     * @param toIndex   index after the last bit to be cleared.
-     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}.
      * @return this.
+     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
+     *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
     public FluentBitSet clear(final int fromIndex, final int toIndex) {
         bitSet.clear(fromIndex, toIndex);
         return this;
@@ -203,6 +207,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
     }
 
     @Override
+    @Pure
     public boolean equals(final Object obj) {
         if (this == obj) {
             return true;
@@ -218,9 +223,11 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bit at the specified index to the complement of its current value.
      *
      * @param bitIndex the index of the bit to flip.
-     * @throws IndexOutOfBoundsException if the specified index is negative.
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("get_int")
+    @Ensures("flip_int")
     public FluentBitSet flip(final int bitIndex) {
         bitSet.flip(bitIndex);
         return this;
@@ -231,11 +238,13 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * complement of its current value.
      *
      * @param fromIndex index of the first bit to flip.
-     * @param toIndex index after the last bit to flip.
+     * @param toIndex   index after the last bit to flip.
-     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}.
      * @return this.
+     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
+     *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
+    @Ensures("flip_int_range")
     public FluentBitSet flip(final int fromIndex, final int toIndex) {
         bitSet.flip(fromIndex, toIndex);
         return this;
@@ -261,11 +270,13 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * {@code toIndex} (exclusive).
      *
      * @param fromIndex index of the first bit to include.
-     * @param toIndex index after the last bit to include.
+     * @param toIndex   index after the last bit to include.
      * @return a new {@link BitSet} from a range of this {@link BitSet}.
      * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}.
+     *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
+    @Ensures("get_int_range")
     public FluentBitSet get(final int fromIndex, final int toIndex) {
         return new FluentBitSet(bitSet.get(fromIndex, toIndex));
     }
@@ -379,6 +390,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("or_bs_array")
     public FluentBitSet or(final FluentBitSet... set) {
         for (final FluentBitSet e : set) {
             this.bitSet.or(e.bitSet);
@@ -438,8 +450,8 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bit at the specified indexes to {@code true}.
      *
      * @param bitIndexArray a bit index array.
-     * @throws IndexOutOfBoundsException if the specified index is negative.
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative.
      */
     public FluentBitSet set(final int... bitIndexArray) {
         for (final int e : bitIndexArray) {
@@ -452,8 +464,8 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bit at the specified index to {@code true}.
      *
      * @param bitIndex a bit index
-     * @throws IndexOutOfBoundsException if the specified index is negative
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative
      */
     public FluentBitSet set(final int bitIndex) {
         bitSet.set(bitIndex);
@@ -464,9 +476,9 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * Sets the bit at the specified index to the specified value.
      *
      * @param bitIndex a bit index.
-     * @param value a boolean value to set.
+     * @param value    a boolean value to set.
-     * @throws IndexOutOfBoundsException if the specified index is negative.
      * @return this.
+     * @throws IndexOutOfBoundsException if the specified index is negative.
      */
     public FluentBitSet set(final int bitIndex, final boolean value) {
         bitSet.set(bitIndex, value);
@@ -478,10 +490,10 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * {@code true}.
      *
      * @param fromIndex index of the first bit to be set.
-     * @param toIndex index after the last bit to be set.
+     * @param toIndex   index after the last bit to be set.
-     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}.
      * @return this.
+     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
+     *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
     public FluentBitSet set(final int fromIndex, final int toIndex) {
         bitSet.set(fromIndex, toIndex);
@@ -493,11 +505,11 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * specified value.
      *
      * @param fromIndex index of the first bit to be set.
-     * @param toIndex index after the last bit to be set.
+     * @param toIndex   index after the last bit to be set.
-     * @param value value to set the selected bits to.
+     * @param value     value to set the selected bits to.
-     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}.
      * @return this.
+     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
+     *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
     public FluentBitSet set(final int fromIndex, final int toIndex, final boolean value) {
         bitSet.set(fromIndex, toIndex, value);
@@ -509,10 +521,10 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * {@code true}.
      *
      * @param fromIndex index of the first bit to be set
-     * @param toIndex index of the last bit to be set
+     * @param toIndex   index of the last bit to be set
-     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
-     *         {@code fromIndex} is larger than {@code toIndex}
      * @return this.
+     * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
+     *                                   {@code fromIndex} is larger than {@code toIndex}
      */
     public FluentBitSet setInclusive(final int fromIndex, final int toIndex) {
         bitSet.set(fromIndex, toIndex + 1);

src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContracts.java

@@ -89,11 +89,26 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
         return test_cardinality(returns, true) && test_length(returns, set::length);
     }
 
+    @Pure
+    default boolean or_bs_array(final FluentBitSet returns, final FluentBitSet... set) {
+        final FluentBitSet results = new FluentBitSet(old(this).bitSet());
+
+        for (final FluentBitSet s : set) {
+            results.or(s);
+            if (!or_bs(results, s.bitSet())) {
+                return false;
+            }
+        }
+
+        return results.equals(returns);
+    }
+
     @Pure
     default boolean or_bs(final FluentBitSet returns, final BitSet set) {
         return test_cardinality(returns, false) && test_length(returns, set::length);
     }
 
+
     @Pure
     default boolean clear_void(final FluentBitSet returns) {
         return cardinality() == 0;
@@ -113,7 +128,7 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
 
     @Pure
     default boolean is_empty(final boolean returns) {
-        return returns == (cardinality() == 0);
+        return returns == (cardinality() == 0) && returns == (length() == 0);
     }
 
     @Pure
@@ -121,6 +136,31 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
         return bitIndex >= 0;
     }
 
+    @Pure
+    default boolean valid_indexes(final int ...bitIndexArray) {
+        return IntStream.of(bitIndexArray).allMatch(this::get_int);
+    }
+
+    @Pure
+    default boolean get_int_range_pre(final int fromIndex, final int toIndex) {
+        return 0 <= fromIndex && fromIndex <= toIndex;
+    }
+
+    @Pure
+    default boolean get_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
+        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.get(i) == returns.get(i - fromIndex));
+    }
+
+    @Pure
+    default boolean flip_int(final FluentBitSet returns, final int bitIndex) {
+        return returns.get(bitIndex) != old(this).get(bitIndex);
+    }
+
+    @Pure
+    default boolean flip_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
+        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.flip_int(returns, i));
+    }
+
     @Pure
     default boolean intersects_bs(final boolean returns, final BitSet set) {
         return returns == set.intersects(this.bitSet());

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

@@ -18,20 +18,17 @@
  */
 package ch.usi.inf.sdm.sdm04.math;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
-import static org.junit.jupiter.api.Assertions.assertNotEquals;
-import static org.junit.jupiter.api.Assertions.assertSame;
-import static org.junit.jupiter.api.Assertions.assertThrows;
-import static org.junit.jupiter.api.Assertions.assertTrue;
-
 import org.junit.jupiter.api.Test;
 
+import static org.junit.jupiter.api.Assertions.*;
+
 /**
  * Test cases for the {@link Fraction} class
  */
 public class FractionTest {
 
-    private static final int SKIP = 500;  //53
+    // changed from a value of 500 to speed up tests
+    private static final int SKIP = 3000;  //53
 
     @Test
     public void testAbs() {
@@ -1037,7 +1034,7 @@ public class FractionTest {
         assertThrows(
                 ArithmeticException.class,
                 () -> Fraction.getFraction(1, Integer.MAX_VALUE).subtract(Fraction.getFraction(1, Integer.MAX_VALUE - 1)));
-        f = f1.subtract(f2);
+            f = f1.subtract(f2);
 
         // denominator should not be a multiple of 2 or 3 to trigger overflow
         assertThrows(

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

@@ -37,69 +37,69 @@ public class IEEE754rUtilsTest {
         // Changed the exception types to Throwable to allow jSicko assertion errors
         assertThrows(
                 Throwable.class,
-                () -> new IEEE754rUtils().min( (float[]) null),
+                () -> IEEE754rUtils.min( (float[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
                 Throwable.class,
-                new IEEE754rUtils()::min,
+                IEEE754rUtils::min,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
                 Throwable.class,
-                () -> new IEEE754rUtils().max((float[]) null),
+                () -> IEEE754rUtils.max((float[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
                 Throwable.class,
-                new IEEE754rUtils()::max,
+                IEEE754rUtils::max,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
                 Throwable.class,
-                () -> new IEEE754rUtils().min( (double[]) null),
+                () -> IEEE754rUtils.min( (double[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
                 Throwable.class,
-                new IEEE754rUtils()::min,
+                IEEE754rUtils::min,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
                 Throwable.class,
-                () -> new IEEE754rUtils().max( (double[]) null),
+                () -> IEEE754rUtils.max( (double[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
                 Throwable.class,
-                new IEEE754rUtils()::max,
+                IEEE754rUtils::max,
                 "IllegalArgumentException expected for empty input");
     }
 
     @Test
     public void testLang381() {
-        assertEquals(1.2, new IEEE754rUtils().min(1.2, 2.5, Double.NaN), 0.01);
+        assertEquals(1.2, IEEE754rUtils.min(1.2, 2.5, Double.NaN), 0.01);
-        assertEquals(2.5, new IEEE754rUtils().max(1.2, 2.5, Double.NaN), 0.01);
+        assertEquals(2.5, IEEE754rUtils.max(1.2, 2.5, Double.NaN), 0.01);
-        assertTrue(Double.isNaN(new IEEE754rUtils().max(Double.NaN, Double.NaN, Double.NaN)));
+        assertTrue(Double.isNaN(IEEE754rUtils.max(Double.NaN, Double.NaN, Double.NaN)));
-        assertEquals(1.2f, new IEEE754rUtils().min(1.2f, 2.5f, Float.NaN), 0.01);
+        assertEquals(1.2f, IEEE754rUtils.min(1.2f, 2.5f, Float.NaN), 0.01);
-        assertEquals(2.5f, new IEEE754rUtils().max(1.2f, 2.5f, Float.NaN), 0.01);
+        assertEquals(2.5f, IEEE754rUtils.max(1.2f, 2.5f, Float.NaN), 0.01);
-        assertTrue(Float.isNaN(new IEEE754rUtils().max(Float.NaN, Float.NaN, Float.NaN)));
+        assertTrue(Float.isNaN(IEEE754rUtils.max(Float.NaN, Float.NaN, Float.NaN)));
 
         final double[] a = { 1.2, Double.NaN, 3.7, 27.0, 42.0, Double.NaN };
-        assertEquals(42.0, new IEEE754rUtils().max(a), 0.01);
+        assertEquals(42.0, IEEE754rUtils.max(a), 0.01);
-        assertEquals(1.2, new IEEE754rUtils().min(a), 0.01);
+        assertEquals(1.2, IEEE754rUtils.min(a), 0.01);
 
         final double[] b = { Double.NaN, 1.2, Double.NaN, 3.7, 27.0, 42.0, Double.NaN };
-        assertEquals(42.0, new IEEE754rUtils().max(b), 0.01);
+        assertEquals(42.0, IEEE754rUtils.max(b), 0.01);
-        assertEquals(1.2, new IEEE754rUtils().min(b), 0.01);
+        assertEquals(1.2, IEEE754rUtils.min(b), 0.01);
 
         final float[] aF = { 1.2f, Float.NaN, 3.7f, 27.0f, 42.0f, Float.NaN };
-        assertEquals(1.2f, new IEEE754rUtils().min(aF), 0.01);
+        assertEquals(1.2f, IEEE754rUtils.min(aF), 0.01);
-        assertEquals(42.0f, new IEEE754rUtils().max(aF), 0.01);
+        assertEquals(42.0f, IEEE754rUtils.max(aF), 0.01);
 
         final float[] bF = { Float.NaN, 1.2f, Float.NaN, 3.7f, 27.0f, 42.0f, Float.NaN };
-        assertEquals(1.2f, new IEEE754rUtils().min(bF), 0.01);
+        assertEquals(1.2f, IEEE754rUtils.min(bF), 0.01);
-        assertEquals(42.0f, new IEEE754rUtils().max(bF), 0.01);
+        assertEquals(42.0f, IEEE754rUtils.max(bF), 0.01);
     }
 
 }

src/test/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetTest.java

@@ -17,6 +17,7 @@
 
 package ch.usi.inf.sdm.sdm04.util;
 
+import ch.usi.si.codelounge.jsicko.Contract;
 import org.apache.commons.lang3.ArrayUtils;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
@@ -207,7 +208,8 @@ public class FluentBitSetTest {
         eightFbs.clear(165);
         assertFalse(eightFbs.get(165), "Failed to clear bit");
         // Try out of range
-        assertThrows(IndexOutOfBoundsException.class, () -> eightFbs.clear(-1));
+        // Changed to Throwable to allow JSicko violations
+        assertThrows(Throwable.class, () -> eightFbs.clear(-1));
 
         final FluentBitSet bs = newInstance(0);
         assertEquals(0, bs.length(), "Test1: Wrong length,");
@@ -375,17 +377,20 @@ public class FluentBitSetTest {
 
         // test illegal args
         bs = newInstance(10);
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(-1, 3),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(-1, 3),
             "Test1: Attempt to flip with negative index failed to generate exception");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(2, -1),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(2, -1),
             "Test2: Attempt to flip with negative index failed to generate exception");
 
         bs.set(2, 4);
         bs.clear(2, 2);
         assertTrue(bs.get(2), "Bit got cleared incorrectly ");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(4, 2),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(4, 2),
             "Test4: Attempt to flip with illegal args failed to generate exception");
 
         bs = newInstance(0);
@@ -443,7 +448,8 @@ public class FluentBitSetTest {
         eightFbs.clear(165);
         assertFalse(eightFbs.get(165), "Failed to clear bit");
         // Try out of range
-        assertThrows(IndexOutOfBoundsException.class, () -> eightFbs.clear(-1));
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> eightFbs.clear(-1));
 
         final FluentBitSet bs = newInstance(0);
         assertEquals(0, bs.length(), "Test1: Wrong length,");
@@ -552,7 +558,8 @@ public class FluentBitSetTest {
         assertFalse(bs.get(9), "Failed to flip bit");
         assertFalse(bs.get(10), "Failed to flip bit");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance().flip(-1), "Attempt to flip at negative index failed to generate exception");
+        // changed to Throwable to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance().flip(-1), "Attempt to flip at negative index failed to generate exception");
 
         // Try setting a bit on a 64 boundary
         bs.flip(128);
@@ -730,21 +737,24 @@ public class FluentBitSetTest {
         try {
             bs.flip(-1, 3);
             fail("Test1: Attempt to flip with  negative index failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
 
         try {
             bs.flip(2, -1);
             fail("Test2: Attempt to flip with negative index failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
 
         try {
             bs.flip(4, 2);
             fail("Test4: Attempt to flip with illegal args failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
     }