Skip to content

Commit 92af25d

Browse files
dbenndbenn
authored
Merge pull request #566 from AAVSO/additional-pbt
Add property-based tests as foundation for formal verification
2 parents 84c9e64 + aa5620d commit 92af25d

4 files changed

Lines changed: 629 additions & 3 deletions

File tree

‎test/org/aavso/tools/vstar/data/PropertyPBTTest.java‎

Lines changed: 215 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,215 @@
1+
/**
2+
* VStar: a statistical analysis tool for variable star data.
3+
* Copyright (C) 2009 AAVSO (http://www.aavso.org/)
4+
*
5+
* This program is free software: you can redistribute it and/or modify
6+
* it under the terms of the GNU Affero General Public License as
7+
* published by the Free Software Foundation, either version 3 of the
8+
* License, or (at your option) any later version.
9+
*
10+
* This program is distributed in the hope that it will be useful,
11+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
12+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13+
* GNU Affero General Public License for more details.
14+
*
15+
* You should have received a copy of the GNU Affero General Public License
16+
* along with this program. If not, see <http://www.gnu.org/licenses/>.
17+
*/
18+
package org.aavso.tools.vstar.data;
19+
20+
import junit.framework.TestCase;
21+
22+
import org.quicktheories.WithQuickTheories;
23+
import org.quicktheories.core.Gen;
24+
25+
/**
26+
* Property-based tests for the Property class, verifying algebraic contracts
27+
* of equals, hashCode, and compareTo.
28+
*
29+
* These properties are the Java equivalents of the axioms that a formal
30+
* verification (e.g. in KeY or Lean) would prove unconditionally.
31+
*/
32+
public class PropertyPBTTest extends TestCase implements WithQuickTheories {
33+
34+
public PropertyPBTTest(String name) {
35+
super(name);
36+
}
37+
38+
// -- Generators for Property instances --
39+
40+
private Gen<Property> intProperties() {
41+
return integers().all().map(Property::new);
42+
}
43+
44+
private Gen<Property> realProperties() {
45+
return doubles().between(-1e15, 1e15).map(Property::new);
46+
}
47+
48+
private Gen<Property> boolProperties() {
49+
return booleans().all().map(Property::new);
50+
}
51+
52+
private Gen<Property> stringProperties() {
53+
return strings().basicLatinAlphabet().ofLengthBetween(0, 20)
54+
.map(Property::new);
55+
}
56+
57+
// -- equals: reflexivity --
58+
59+
public void testEqualsReflexiveIntProperty() {
60+
qt().forAll(intProperties()).check(p -> p.equals(p));
61+
}
62+
63+
public void testEqualsReflexiveRealProperty() {
64+
qt().forAll(realProperties()).check(p -> p.equals(p));
65+
}
66+
67+
public void testEqualsReflexiveBoolProperty() {
68+
qt().forAll(boolProperties()).check(p -> p.equals(p));
69+
}
70+
71+
public void testEqualsReflexiveStringProperty() {
72+
qt().forAll(stringProperties()).check(p -> p.equals(p));
73+
}
74+
75+
// -- equals: symmetry (via two identical constructions) --
76+
77+
public void testEqualsSymmetricIntProperty() {
78+
qt().forAll(integers().all()).check(v -> {
79+
Property a = new Property(v);
80+
Property b = new Property(v);
81+
return a.equals(b) == b.equals(a);
82+
});
83+
}
84+
85+
public void testEqualsSymmetricRealProperty() {
86+
qt().forAll(doubles().between(-1e15, 1e15)).check(v -> {
87+
Property a = new Property(v);
88+
Property b = new Property(v);
89+
return a.equals(b) == b.equals(a);
90+
});
91+
}
92+
93+
public void testEqualsSymmetricStringProperty() {
94+
qt().forAll(strings().basicLatinAlphabet().ofLengthBetween(0, 20))
95+
.check(v -> {
96+
Property a = new Property(v);
97+
Property b = new Property(v);
98+
return a.equals(b) == b.equals(a);
99+
});
100+
}
101+
102+
// -- hashCode: consistency with equals --
103+
104+
public void testHashCodeConsistentWithEqualsIntProperty() {
105+
qt().forAll(integers().all()).check(v -> {
106+
Property a = new Property(v);
107+
Property b = new Property(v);
108+
return !a.equals(b) || a.hashCode() == b.hashCode();
109+
});
110+
}
111+
112+
public void testHashCodeConsistentWithEqualsRealProperty() {
113+
qt().forAll(doubles().between(-1e15, 1e15)).check(v -> {
114+
Property a = new Property(v);
115+
Property b = new Property(v);
116+
return !a.equals(b) || a.hashCode() == b.hashCode();
117+
});
118+
}
119+
120+
public void testHashCodeConsistentWithEqualsStringProperty() {
121+
qt().forAll(strings().basicLatinAlphabet().ofLengthBetween(0, 20))
122+
.check(v -> {
123+
Property a = new Property(v);
124+
Property b = new Property(v);
125+
return !a.equals(b) || a.hashCode() == b.hashCode();
126+
});
127+
}
128+
129+
// -- compareTo: antisymmetry (sgn(a.compareTo(b)) == -sgn(b.compareTo(a))) --
130+
131+
public void testCompareToAntisymmetricIntProperty() {
132+
qt().forAll(integers().all(), integers().all()).check((v1, v2) -> {
133+
Property a = new Property(v1);
134+
Property b = new Property(v2);
135+
return Integer.signum(a.compareTo(b)) == -Integer
136+
.signum(b.compareTo(a));
137+
});
138+
}
139+
140+
public void testCompareToAntisymmetricRealProperty() {
141+
qt().forAll(doubles().between(-1e15, 1e15),
142+
doubles().between(-1e15, 1e15)).check((v1, v2) -> {
143+
Property a = new Property(v1);
144+
Property b = new Property(v2);
145+
return Integer.signum(a.compareTo(b)) == -Integer
146+
.signum(b.compareTo(a));
147+
});
148+
}
149+
150+
public void testCompareToAntisymmetricStringProperty() {
151+
qt().forAll(strings().basicLatinAlphabet().ofLengthBetween(0, 20),
152+
strings().basicLatinAlphabet().ofLengthBetween(0, 20))
153+
.check((v1, v2) -> {
154+
Property a = new Property(v1);
155+
Property b = new Property(v2);
156+
return Integer.signum(a.compareTo(b)) == -Integer
157+
.signum(b.compareTo(a));
158+
});
159+
}
160+
161+
// -- compareTo: consistency with equals --
162+
163+
public void testCompareToConsistentWithEqualsIntProperty() {
164+
qt().forAll(integers().all()).check(v -> {
165+
Property a = new Property(v);
166+
Property b = new Property(v);
167+
return a.equals(b) && a.compareTo(b) == 0;
168+
});
169+
}
170+
171+
public void testCompareToConsistentWithEqualsRealProperty() {
172+
qt().forAll(doubles().between(-1e15, 1e15)).check(v -> {
173+
Property a = new Property(v);
174+
Property b = new Property(v);
175+
return a.equals(b) && a.compareTo(b) == 0;
176+
});
177+
}
178+
179+
public void testCompareToConsistentWithEqualsStringProperty() {
180+
qt().forAll(strings().basicLatinAlphabet().ofLengthBetween(0, 20))
181+
.check(v -> {
182+
Property a = new Property(v);
183+
Property b = new Property(v);
184+
return a.equals(b) && a.compareTo(b) == 0;
185+
});
186+
}
187+
188+
// -- compareTo: transitivity --
189+
190+
public void testCompareToTransitiveIntProperty() {
191+
qt().forAll(integers().all(), integers().all(), integers().all())
192+
.check((v1, v2, v3) -> {
193+
Property a = new Property(v1);
194+
Property b = new Property(v2);
195+
Property c = new Property(v3);
196+
if (a.compareTo(b) <= 0 && b.compareTo(c) <= 0) {
197+
return a.compareTo(c) <= 0;
198+
}
199+
return true;
200+
});
201+
}
202+
203+
// -- equals: null safety --
204+
205+
public void testEqualsNullReturnsFalseIntProperty() {
206+
qt().forAll(intProperties()).check(p -> !p.equals(null));
207+
}
208+
209+
// -- NO_VALUE sentinel --
210+
211+
public void testNoValueEquality() {
212+
assertTrue(Property.NO_VALUE.equals(new Property()));
213+
assertEquals(Property.propType.NONE, Property.NO_VALUE.getType());
214+
}
215+
}

‎test/org/aavso/tools/vstar/util/date/HJDConverterPBTTest.java‎

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
1+
/**
2+
* VStar: a statistical analysis tool for variable star data.
3+
* Copyright (C) 2010 AAVSO (http://www.aavso.org/)
4+
*
5+
* This program is free software: you can redistribute it and/or modify
6+
* it under the terms of the GNU Affero General Public License as
7+
* published by the Free Software Foundation, either version 3 of the
8+
* License, or (at your option) any later version.
9+
*
10+
* This program is distributed in the hope that it will be useful,
11+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
12+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13+
* GNU Affero General Public License for more details.
14+
*
15+
* You should have received a copy of the GNU Affero General Public License
16+
* along with this program. If not, see <http://www.gnu.org/licenses/>.
17+
*/
18+
package org.aavso.tools.vstar.util.date;
19+
20+
import junit.framework.TestCase;
21+
22+
import org.aavso.tools.vstar.util.coords.DecInfo;
23+
import org.aavso.tools.vstar.util.coords.EpochType;
24+
import org.aavso.tools.vstar.util.coords.RAInfo;
25+
import org.quicktheories.WithQuickTheories;
26+
27+
/**
28+
* Property-based tests for the J2000 HJD converter.
29+
*
30+
* These tests express universal properties of the HJD correction and
31+
* angle-normalization helpers, suitable for later promotion to formal
32+
* proofs (e.g. in Lean 4 or via JML/OpenJML).
33+
*/
34+
public class HJDConverterPBTTest extends TestCase implements WithQuickTheories {
35+
36+
private J2000HJDConverter converter;
37+
38+
public HJDConverterPBTTest(String name) {
39+
super(name);
40+
}
41+
42+
protected void setUp() throws Exception {
43+
super.setUp();
44+
converter = (J2000HJDConverter) AbstractHJDConverter
45+
.getInstance(EpochType.J2000);
46+
}
47+
48+
// -- degsInRange properties --
49+
50+
/**
51+
* degsInRange always returns a value in [0, 360).
52+
*/
53+
public void testDegsInRangeOutputRangeProperty() {
54+
qt().forAll(doubles().between(-1e6, 1e6)).check(degs -> {
55+
double result = converter.degsInRange(degs);
56+
return result >= 0 && result < 360.0;
57+
});
58+
}
59+
60+
/**
61+
* degsInRange is idempotent: applying it twice gives the same result.
62+
*/
63+
public void testDegsInRangeIdempotentProperty() {
64+
qt().forAll(doubles().between(-1e6, 1e6)).check(degs -> {
65+
double once = converter.degsInRange(degs);
66+
double twice = converter.degsInRange(once);
67+
return Math.abs(once - twice) < 1e-10;
68+
});
69+
}
70+
71+
/**
72+
* degsInRange respects 360-degree periodicity.
73+
*/
74+
public void testDegsInRangePeriodicProperty() {
75+
qt().forAll(doubles().between(-1e4, 1e4)).check(degs -> {
76+
double r1 = converter.degsInRange(degs);
77+
double r2 = converter.degsInRange(degs + 360.0);
78+
return Math.abs(r1 - r2) < 1e-9;
79+
});
80+
}
81+
82+
// -- radsInRange properties --
83+
84+
/**
85+
* radsInRange always returns a value in [0, 2*pi).
86+
*/
87+
public void testRadsInRangeOutputRangeProperty() {
88+
final double TWOPI = 2 * Math.PI;
89+
qt().forAll(doubles().between(-1e4, 1e4)).check(rads -> {
90+
double result = converter.radsInRange(rads);
91+
return result >= 0 && result < TWOPI + 1e-12;
92+
});
93+
}
94+
95+
/**
96+
* radsInRange is idempotent.
97+
*/
98+
public void testRadsInRangeIdempotentProperty() {
99+
qt().forAll(doubles().between(-1e4, 1e4)).check(rads -> {
100+
double once = converter.radsInRange(rads);
101+
double twice = converter.radsInRange(once);
102+
return Math.abs(once - twice) < 1e-10;
103+
});
104+
}
105+
106+
/**
107+
* radsInRange respects 2*pi periodicity.
108+
*/
109+
public void testRadsInRangePeriodicProperty() {
110+
final double TWOPI = 2 * Math.PI;
111+
qt().forAll(doubles().between(-1e3, 1e3)).check(rads -> {
112+
double r1 = converter.radsInRange(rads);
113+
double r2 = converter.radsInRange(rads + TWOPI);
114+
return Math.abs(r1 - r2) < 1e-9;
115+
});
116+
}
117+
118+
// -- HJD correction bound --
119+
120+
/**
121+
* The HJD correction is bounded by R_max/c where R_max ~ 1.017 AU and
122+
* c = 173.14 AU/day, giving a maximum correction of ~0.00588 days
123+
* (~8.5 minutes). We use 0.006 days as a generous bound.
124+
*
125+
* This property holds for any sky position and any JD in a reasonable
126+
* historical/future range.
127+
*/
128+
public void testHJDCorrectionBoundProperty() {
129+
final double MAX_CORRECTION_DAYS = 0.006;
130+
131+
qt().forAll(
132+
doubles().between(2415000, 2470000),
133+
doubles().between(0.0, 360.0),
134+
doubles().between(-90.0, 90.0))
135+
.check((jd, raDeg, decDeg) -> {
136+
RAInfo ra = new RAInfo(EpochType.J2000, raDeg);
137+
DecInfo dec = new DecInfo(EpochType.J2000, decDeg);
138+
double hjd = converter.convert(jd, ra, dec);
139+
double correction = Math.abs(hjd - jd);
140+
return correction <= MAX_CORRECTION_DAYS;
141+
});
142+
}
143+
144+
// -- julianCenturies is linear --
145+
146+
/**
147+
* julianCenturies(jd) is a linear function of jd:
148+
* T(jd + delta) - T(jd) = delta / 36525.
149+
*/
150+
public void testJulianCenturiesLinearProperty() {
151+
qt().forAll(
152+
doubles().between(2415000, 2470000),
153+
doubles().between(0.1, 365.25))
154+
.check((jd, delta) -> {
155+
double t1 = converter.julianCenturies(jd);
156+
double t2 = converter.julianCenturies(jd + delta);
157+
double expected = delta / 36525.0;
158+
return Math.abs((t2 - t1) - expected) < 1e-12;
159+
});
160+
}
161+
162+
// -- Radius vector bound --
163+
164+
/**
165+
* The Earth-Sun radius vector R is bounded: approximately
166+
* 0.983 AU (perihelion) <= R <= 1.017 AU (aphelion).
167+
* We use slightly wider bounds for robustness with the low-accuracy model.
168+
*/
169+
public void testRadiusVectorBoundProperty() {
170+
qt().forAll(doubles().between(2415000, 2470000)).check(jd -> {
171+
double T = converter.julianCenturies(jd);
172+
int year = AbstractDateUtil.getInstance().jdToYMD(jd).getYear();
173+
SolarCoords coords = converter.solarCoords(T, year);
174+
double R = converter.radiusVector(T, coords.getTrueAnomaly(),
175+
coords.getEquationOfCenter());
176+
return R >= 0.97 && R <= 1.04;
177+
});
178+
}
179+
}

0 commit comments

Comments
 (0)