Adding 3 pre/post conditions

This commit is contained in:
filippocasari 2022-12-05 20:00:11 +01:00 committed by Claudio Maggioni
parent 0000122175
commit 5404877d2d
3 changed files with 38 additions and 1 deletions

View file

@ -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) {

View file

@ -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 ||

View file

@ -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