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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
import org.checkerframework.checker.units.*;
import org.checkerframework.checker.units.qual.*;
public class BasicUnits {
void demo() {
// :: error: (assignment.type.incompatible)
@m int merr = 5;
@m int m = 5 * UnitsTools.m;
@s int s = 9 * UnitsTools.s;
// :: error: (assignment.type.incompatible)
@km int kmerr = 10;
@km int km = 10 * UnitsTools.km;
// this is allowed, unqualified is a supertype of all units
int bad = m / s;
@mPERs int good = m / s;
// :: error: (assignment.type.incompatible)
@mPERs int b1 = s / m;
// :: error: (assignment.type.incompatible)
@mPERs int b2 = m * s;
@mPERs2 int goodaccel = m / s / s;
// :: error: (assignment.type.incompatible)
@mPERs2 int badaccel1 = s / m / s;
// :: error: (assignment.type.incompatible)
@mPERs2 int badaccel2 = s / s / m;
// :: error: (assignment.type.incompatible)
@mPERs2 int badaccel3 = s * s / m;
// :: error: (assignment.type.incompatible)
@mPERs2 int badaccel4 = m * s * s;
@Area int ae = m * m;
@m2 int gae = m * m;
// :: error: (assignment.type.incompatible)
@Area int bae = m * m * m;
// :: error: (assignment.type.incompatible)
@km2 int bae1 = m * m;
@radians double rad = 20.0d * UnitsTools.rad;
@degrees double deg = 30.0d * UnitsTools.deg;
@degrees double rToD1 = UnitsTools.toDegrees(rad);
// :: error: (argument.type.incompatible)
@degrees double rToD2 = UnitsTools.toDegrees(deg);
// :: error: (assignment.type.incompatible)
@radians double rToD3 = UnitsTools.toDegrees(rad);
@radians double dToR1 = UnitsTools.toRadians(deg);
// :: error: (argument.type.incompatible)
@radians double rToR2 = UnitsTools.toRadians(rad);
// :: error: (assignment.type.incompatible)
@degrees double rToR3 = UnitsTools.toRadians(deg);
// speed conversion
@mPERs int mPs = 30 * UnitsTools.mPERs;
@kmPERh int kmPhr = 20 * UnitsTools.kmPERh;
@kmPERh int kmPhrRes = (int) UnitsTools.fromMeterPerSecondToKiloMeterPerHour(mPs);
@mPERs int mPsRes = (int) UnitsTools.fromKiloMeterPerHourToMeterPerSecond(kmPhr);
// :: error: (assignment.type.incompatible)
@mPERs int mPsResBad = (int) UnitsTools.fromMeterPerSecondToKiloMeterPerHour(mPs);
// :: error: (assignment.type.incompatible)
@kmPERh int kmPhrResBad = (int) UnitsTools.fromKiloMeterPerHourToMeterPerSecond(kmPhr);
// speeds
@km int kilometers = 10 * UnitsTools.km;
@h int hours = UnitsTools.h;
@kmPERh int speed = kilometers / hours;
// Addition/substraction only accepts another @kmPERh value
// :: error: (assignment.type.incompatible)
speed = speed + 5;
// :: error: (compound.assignment.type.incompatible)
speed += 5;
speed += speed;
speed = (speed += speed);
// Multiplication/division with an unqualified type is allowed
speed = kilometers / hours * 2;
speed /= 2;
speed = (speed /= 2);
}
void prefixOutputTest() {
@m int x = 5 * UnitsTools.m;
@m(Prefix.kilo) int y = 2 * UnitsTools.km;
@m(Prefix.one) int z = 3 * UnitsTools.m;
@km int y2 = 3 * UnitsTools.km;
// :: error: (assignment.type.incompatible)
y2 = z;
// :: error: (assignment.type.incompatible)
y2 = x;
// :: error: (assignment.type.incompatible)
y = z;
// :: error: (assignment.type.incompatible)
y = x;
// :: error: (assignment.type.incompatible)
y2 = x * x;
// :: error: (assignment.type.incompatible)
y2 = z * z;
}
}
|
