adding post conditions

README.md

@@ -25,8 +25,8 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
   - (TODO) `FluentBitSet xor(FluentBitSet)`==> done/ to review
   - (TODO) `byte[] toByteArray()` and `byte[] toLongArray()`
   - (TODO) `FluentBitSet set(int)` ==> done/ to review
-  - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)`
+  - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` ==> done
-  - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)`
+  - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` ==>done
 
 ## Run Tests
 

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

@@ -339,6 +339,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return the index of the next clear bit.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Ensures("nice_range_next_previous_ClearBit_post")
     public int nextClearBit(final int fromIndex) {
         return bitSet.nextClearBit(fromIndex);
     }
@@ -364,6 +365,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return the index of the next set bit, or {@code -1} if there is no such bit.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Ensures("nice_range_next_previous_SetBit_post")
     public int nextSetBit(final int fromIndex) {
         return bitSet.nextSetBit(fromIndex);
     }
@@ -420,6 +422,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return the index of the previous clear bit, or {@code -1} if there is no such bit.
      * @throws IndexOutOfBoundsException if the specified index is less than {@code -1}.
      */
+    @Ensures("nice_range_next_previous_ClearBit_post")
     public int previousClearBit(final int fromIndex) {
         return bitSet.previousClearBit(fromIndex);
     }
@@ -442,6 +445,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return the index of the previous set bit, or {@code -1} if there is no such bit
      * @throws IndexOutOfBoundsException if the specified index is less than {@code -1}
      */
+    @Ensures("nice_range_next_previous_SetBit_post")
     public int previousSetBit(final int fromIndex) {
         return bitSet.previousSetBit(fromIndex);
     }

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

@@ -28,6 +28,7 @@ import java.util.stream.IntStream;
 
 import static ch.usi.si.codelounge.jsicko.Contract.old;
 
+
 @SuppressWarnings("unused") // methods used by jSicko
 public interface FluentBitSetContracts extends FluentBitSetContractsContracts, Contract {
 
@@ -74,10 +75,21 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
     }
     @Pure
     default boolean xor_fbs(final FluentBitSet returns, final BitSet set) {
-        //final FluentBitSet notSet = new FluentBitSet(set).flip(0, set.length());
+        int card1 = old(this).cardinality();
-        final boolean bool1 = (old(this).cardinality()-set.cardinality())  == this.cardinality();
+        int card2 = set.cardinality();
-        final boolean bool2 = (set.cardinality()- old(this).cardinality())  == this.cardinality();
+        //System.err.println("card1: "+card1);
-        return (bool1 || bool2)&& test_length(returns, set::length);
+        //System.err.println("card2: "+card2);
+        //System.err.println("this.card: "+this.cardinality());
+        final boolean bool;
+        // example 1 test: (1st bit stream).card()=(1st bit stream).card() = 8, this.card()=0, this.len() = 8
+        if(card1+card2>this.length()){
+            bool = (card1 + card2 -this.length()) >=this.cardinality();// (8+8 - 8)>=0
+            return (bool) && test_length(returns, set::length);
+        }
+        else{
+            // example 2 test: (1st bit stream).card()= 0, (1st bit stream).card() = 8, this.card()=8, this.len() = 8
+             return (card1+card2) >=this.cardinality(); // (8+0)>=8
+        }
     }
     @Pure
     default boolean set_not_negative_input(final int ...bitIndexArray) {
@@ -195,4 +207,21 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
     default boolean intersects_fbs(final boolean returns, final FluentBitSet set) {
         return intersects_bs(returns, set.bitSet());
     }
+    @Pure
+    default boolean nice_range_next_previous_SetBit_post(int returns, final int fromIndex) {
+
+
+
+         //  we return an index that is in the range [0, len),
+        return (-1<= returns  && returns<this.length());// -1 if we do not find it or findIndex is out of bound
+    }
+    @Pure
+    default boolean nice_range_next_previous_ClearBit_post(int returns, final int fromIndex) {
+        if(fromIndex>=-1){ //if fromIndex is equal to -1 or greater, than the result will be -1(if index not found) or the index itself
+            return (-1<= returns);
+        }
+        else{
+            return false; // an exception is thrown
+        }
+    }
 }