Adding 3 pre/post conditions

README.md

@@ -12,6 +12,10 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
   - `static Fraction getFraction(int, int)` and `static Fraction getFraction(int, int, int)`
   - `static Fraction getReducedFraction(int, int)`
   - (TODO PICK OTHER 3 FROM HERE)
+  - `public int getDenominator()`
+  - `public Fraction negate()`
+  - `public Fraction abs()`
+  - `public Fraction reduce()`
 - Class `CharRange`
   - `boolean contains(CharRange)`
 - Class `util.FluentBitSet`

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

@@ -316,6 +316,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      * @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
@@ -456,6 +457,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      *
      * @return a new reduced fraction instance, or this if no simplification possible
      */
+    @Ensures("must_be_reduced")
     public Fraction reduce() {
         if (numerator == 0) {
             return equals(ZERO) ? this : ZERO;
@@ -516,6 +518,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      * @return {@code this} if it is positive, or a new positive fraction
      *  instance with the opposite signed numerator
      */
+    @Ensures("must_positive")
     public Fraction abs() {
         if (numerator >= 0) {
             return this;

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

@@ -44,6 +44,11 @@ public interface FractionContracts extends Contract {
         return this.getNumerator() != Integer.MIN_VALUE;
     }
 
+    @Pure
+    default boolean must_positive(Fraction returns) {
+        return returns.getNumerator() >= 0;
+    }
+
     @Pure
     default boolean check_if_negative(final Fraction returns) {
 
@@ -55,6 +60,22 @@ public interface FractionContracts extends Contract {
         return returns.getNumerator() > 0;
     }
 
+    @Pure
+    default boolean must_be_reduced(Fraction returns) {
+        int den = returns.getDenominator();
+        int num = returns.getNumerator();
+        if(num==0){
+            return true;
+        }
+        if( num>den){
+            return (num % den == num);
+        } else if (num<den && num>0 ) {
+            return (num%den == num);
+        }
+        return true;
+
+    }
+
     @Pure
     static boolean get_fraction_pre(final int numerator, final int denominator) {
         return denominator != 0 && (denominator > 0 ||