liquid-java-external-libs/MathRefinements.java at main · liquid-java/liquid-java-external-libs · 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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
package repair.regen.math.correctInvocation;

import repair.regen.specification.ExternalRefinementsFor;
import repair.regen.specification.Refinement;

/**
	Refinements for the Math class
	Only modeling int, long and float functions
	(long and float functions take more time to be verified)
*/
@ExternalRefinementsFor("java.lang.Math")
public interface MathRefinements {

	@Refinement("_ == 3.141592653589793")
	public double PI = 0;

	@Refinement("_ == 2.7182818284590452354")
	public double E = 0;

	@Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
	public int abs(int arg0);
	@Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
	public int abs(long arg0);
	@Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
	public int abs(float arg0);
	@Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
	public int abs(double arg0);

	@Refinement(" _ == a+b")
	public int addExact(int a, int b);
	@Refinement(" _ == a+b")
	public long addExact(long a, long b);

	@Refinement(" _ == a-b")
	public int subtractExact(int a, int b);
	@Refinement(" _ == a*b")
	public int multiplyExact(int a, int b);
	@Refinement("_ == (-a)")
	public int negateExact(int a);

	@Refinement("_ == (a-1)")
	public int decrementExact(int a);
	@Refinement("_ == (a-1)")
	public int decrementExact(long a);

	@Refinement("_ == (a+1)")
	public int incrementExact(int a);
	@Refinement("_ == (a+1)")
	public int incrementExact(long a);


	@Refinement("(a > b)? (_ == a):(_ == b)")
	public int max(int a, int b);
	@Refinement("(a > b)? (_ == b):(_ == a)")
	public int min(int a, int b);


	@Refinement(" _ > 0.0 && _ < 1.0")
	public long random(long a, long b);

	@Refinement("((sig > 0)?(_ > 0):(_ < 0)) && (( _ == arg)||(_ == -arg))")
	public float copySign(float arg, float sig);


}