adding two post conditions and 1 pre-condition

README.md

@@ -22,9 +22,9 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
   - `boolean get(int)` and overloads
   - `boolean isEmpty()`
   - `FluentBitSet flip(int)` and overloads
-  - (TODO) `FluentBitSet xor(FluentBitSet)`
+  - (TODO) `FluentBitSet xor(FluentBitSet)`==> done/ to review
   - (TODO) `byte[] toByteArray()` and `byte[] toLongArray()`
-  - (TODO) `FluentBitSet set(int)` 
+  - (TODO) `FluentBitSet set(int)` ==> done/ to review
   - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)`
   - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)`
 

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

@@ -158,6 +158,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @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);
@@ -453,6 +454,8 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("set_not_negative_input")
+    @Ensures("set_")
     public FluentBitSet set(final int... bitIndexArray) {
         for (final int e : bitIndexArray) {
             bitSet.set(e);
@@ -480,6 +483,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+
     public FluentBitSet set(final int bitIndex, final boolean value) {
         bitSet.set(bitIndex, value);
         return this;
@@ -614,6 +618,7 @@ public final class FluentBitSet implements Cloneable, Serializable, FluentBitSet
      * @param set a bit set
      * @return this.
      */
+    @Ensures("xor_fbs")
     public FluentBitSet xor(final BitSet set) {
         bitSet.xor(set);
         return this;

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

@@ -21,6 +21,7 @@ package ch.usi.inf.sdm.sdm04.util;
 
 import ch.usi.si.codelounge.jsicko.Contract;
 
+import java.util.Arrays;
 import java.util.BitSet;
 import java.util.function.Supplier;
 import java.util.stream.IntStream;
@@ -71,6 +72,30 @@ public interface FluentBitSetContracts extends FluentBitSetContractsContracts, C
     default boolean or_fbs(final FluentBitSet returns, final FluentBitSet set) {
         return test_cardinality(returns, false) && test_length(returns, set::length);
     }
+    @Pure
+    default boolean xor_fbs(final FluentBitSet returns, final BitSet set) {
+        //final FluentBitSet notSet = new FluentBitSet(set).flip(0, set.length());
+        final boolean bool1 = (old(this).cardinality()-set.cardinality())  == this.cardinality();
+        final boolean bool2 = (set.cardinality()- old(this).cardinality())  == this.cardinality();
+        return (bool1 || bool2)&& test_length(returns, set::length);
+    }
+    @Pure
+    default boolean set_not_negative_input(final int ...bitIndexArray) {
+        return Arrays.stream(bitIndexArray).allMatch(p -> p >= 0 || p <(this).length() );
+    }
+    @Pure
+    default boolean set_(final FluentBitSet returns, final int ...bitIndexArray) {
+        int len = bitIndexArray.length;
+        for(final int i: bitIndexArray){
+            if(i<0 || i>=returns.length()){
+                len--;
+            }
+        }
+        //System.err.println("array: "+ Arrays.toString(bitIndexArray));
+        //System.err.println("len array: "+len);
+        return (old(this).cardinality()+len) >= this.cardinality();
+
+    }
 
     @Pure
     default boolean and_not_fbs(final FluentBitSet returns, final FluentBitSet set) {