From 000012217537bfd23cb27055811e0233a0232e20 Mon Sep 17 00:00:00 2001 From: filippocasari Date: Sat, 3 Dec 2022 17:54:51 +0100 Subject: [PATCH] adding post conditions --- README.md | 4 +- .../usi/inf/sdm/sdm04/util/FluentBitSet.java | 4 ++ .../sdm/sdm04/util/FluentBitSetContracts.java | 37 +++++++++++++++++-- 3 files changed, 39 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 06c2781..a31e5fc 100644 --- a/README.md +++ b/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 nextClearBit(int)` and `int previousClearBit(int)` + - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` ==> done + - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` ==>done ## Run Tests diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSet.java b/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSet.java index 8b84a1a..2a96e0a 100644 --- a/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSet.java +++ b/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); } diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContracts.java b/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContracts.java index 323ea41..3494434 100644 --- a/src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContracts.java +++ b/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()); - 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); + int card1 = old(this).cardinality(); + int card2 = set.cardinality(); + //System.err.println("card1: "+card1); + //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=-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 + } + } }