FilesExpand file tree

 main

/

MathRefinements.java

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

65 lines (49 loc) · 1.72 KB

 main

/

MathRefinements.java

Top

File metadata and controls

• Code
• Blame

65 lines (49 loc) · 1.72 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

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);

}