liquidjava/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java at edb012b2d05e0048810fe6689e304cc66a72eb23 · cheestree/liquidjava · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorArithmeticFP {

    private static void arithmetic1() {
        @Refinement("_ > 5.0")
        double a = 5.0; // Refinement Error
    }

    private static void arithmetic2() {
        @Refinement("_ > 5.0")
        double a = 5.5;

        @Refinement("_ == 10.0")
        double c = a * 2.0; // Refinement Error
    }

    private static void arithmetic3() {
        @Refinement("_ > 5.0")
        double a = 5.5;

        @Refinement("_ < -5.5")
        double d = -a; // Refinement Error
    }

    private static void arithmetic4() {
        @Refinement("_ > 5.0")
        double a = 5.5;

        @Refinement("_ < -5.5")
        double d = -(a - 2.0); // Refinement Error
    }
}