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

---
 .../ch/usi/inf/sdm/sdm04/math/Fraction.java   |  6 ++++
 .../inf/sdm/sdm04/math/FractionContracts.java | 31 +++++++++++++++++++
 .../usi/inf/sdm/sdm04/math/FractionTest.java  |  2 +-
 3 files changed, 38 insertions(+), 1 deletion(-)

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 69d3d20..13515bf 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
@@ -357,6 +357,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      *
      * @return the numerator fraction part
      */
+
     public int getNumerator() {
         return numerator;
     }
@@ -366,6 +367,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      *
      * @return the denominator fraction part
      */
+    @Ensures("non_negative_den")
     public int getDenominator() {
         return denominator;
     }
@@ -406,6 +408,7 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      *
      * @return the whole number fraction part
      */
+
     @Override
     public int intValue() {
         return numerator / denominator;
@@ -493,6 +496,9 @@ public final class Fraction extends Number implements Comparable<Fraction>, Frac
      *
      * @return a new fraction instance with the opposite signed numerator
      */
+    //@Requires("check_if_non_min_val")
+    @Ensures("check_if_negative")
+    @Requires("check_if_non_min_val")
     public Fraction negate() {
         // the positive range is one smaller than the negative range of an int.
         if (numerator==Integer.MIN_VALUE) {
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 4921426..6e55ba4 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
@@ -21,9 +21,40 @@ package ch.usi.inf.sdm.sdm04.math;
 
 import ch.usi.si.codelounge.jsicko.Contract;
 
+import static ch.usi.si.codelounge.jsicko.Contract.old;
+
 @SuppressWarnings("unused") // used by jSicko
 public interface FractionContracts extends Contract {
 
+    default boolean non_negative_den(final int returns) {
+        return returns != 0.;
+    }
+
+    @Pure
+    Fraction negate();
+
+    @Pure
+    int getDenominator();
+
+    @Pure
+    int getNumerator();
+
+    @Pure
+    default boolean check_if_non_min_val() {
+        return this.getNumerator() != Integer.MIN_VALUE;
+    }
+
+    @Pure
+    default boolean check_if_negative(final Fraction returns) {
+
+
+        if ((this.getNumerator() > 0 && this.getDenominator() > 0) || (this.getNumerator() < 0 && this.getDenominator() < 0)) {
+
+            return returns.getNumerator() < 0;
+        }
+        return returns.getNumerator() > 0;
+    }
+
     @Pure
     static boolean get_fraction_pre(final int numerator, final int denominator) {
         return denominator != 0 && (denominator > 0 ||
diff --git a/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java b/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java
index beb9587..0edd5cf 100644
--- a/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java
+++ b/src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java
@@ -737,7 +737,7 @@ public class FractionTest {
         assertEquals(Integer.MIN_VALUE+2, f.getNumerator());
         assertEquals(Integer.MAX_VALUE, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).negate());
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).negate());
     }
 
     @Test