ShreyankGopal
ShreyankGopal

Reputation: 11

Getting unexpected results in Design By Contract style programming

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

Answers (0)

Related Questions