Reputation: 11
I am new to Design by contract methodology. I am writing a jml code using openjml to specify the contractes to the methods in a class. I have implemented a Subtraction class with the method subtract, which takes two Double values and return the difference between them. But even if does the subtraction correctly it shows post condition is wrong. To understand my issue clearly I have posted my code below.
class Subtraction {
/*@ requires !Double.isNaN(minuend) && !Double.isNaN(subtrahend);
@ ensures \result == minuend - subtrahend;
@*/
public static double subtract(double minuend, double subtrahend) {
return minuend-subtrahend;
}
}
public class Main {
public static void main(String[] args) {
// Example usage
double minuend = 10.5;
double subtrahend = 4.3;
System.out.println("Performing subtraction...");
// Call the subtract method from the Subtraction class
double result = Subtraction.subtract(minuend, subtrahend);
System.out.println("The result of " + minuend + " - " + subtrahend + " is: " + result);
}
}
I have first compiled using the command openjml -rac Main.java
and then ran it using the command openjml-java Main
. However my output is the following
Performing subtraction...
Main.java:7: verify: JML postcondition is false
public static double subtract(double minuend, double subtrahend) {
^
Main.java:4: verify: Associated declaration: Main.java:7:
@ ensures \result == minuend - subtrahend;
^
Main.java:20: verify: JML postcondition is false
double result = Subtraction.subtract(minuend, subtrahend);
^
Main.java:4: verify: Associated declaration: Main.java:20:
@ ensures \result == minuend - subtrahend;
^
The result of 10.5 - 4.3 is: 6.2
Also a point to be noted is that this error does not occur if I use Integer values instead of Double values. I am not understanding why this is happening so i would like some assistance.
Upvotes: 0
Views: 19