From abdcf305729fe10a7197b213c36c5a6608419e37 Mon Sep 17 00:00:00 2001
From: filippocasari <fili9941@gmail.com>
Date: Mon, 5 Dec 2022 20:38:51 +0100
Subject: [PATCH] Adding 3 pre/post conditions

---
 README.md                                     |  4 ++++
 .../ch/usi/inf/sdm/sdm04/math/Fraction.java   |  3 +++
 .../inf/sdm/sdm04/math/FractionContracts.java | 21 +++++++++++++++++++
 3 files changed, 28 insertions(+)

diff --git a/README.md b/README.md
index a31e5fc..72a7229 100644
--- a/README.md
+++ b/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`
diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java b/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java
index 13515bf..476eb39 100644
--- a/src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java
+++ b/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;
diff --git a/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java b/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java
index 6e55ba4..77497f3 100644
--- a/src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java
+++ b/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 ||