frontend/itl_expr design
Design goal
The ITF1788 project publishes interval test cases for IEEE 1788-201511 IEEE Std 1788-2015, IEEE Standard for Interval Arithmetic. The
set-based flavor, decorations (clause 8) and the overlap relation (clause
10.6.4) are the parts exercised here.
in a small language, ITL. This package executes those cases against
ball_float, so that the interval claims in the
ball_float conformance page rest on an
external, pinned corpus. Like the other frontends it is pure: text in,
results out, no IO.
Mathematical background
Intervals and tightest results
In the set-based model an interval is a closed connected subset of : the empty set, the whole line, or with (infinite ends are open). For an operation and intervals , the range is over the points where is defined. In a number format (here binary64) the tightest result is the smallest -interval containing the hull of the range:
ITF1788 cases list this tightest interval as the expected value for the operations IEEE 1788 requires to be tightest. A test that compares bounds for equality therefore checks two things at once: containment (the result encloses the range) and tightness (no bound is one or more ulps too wide).
Decorations
A decorated interval is a pair with in the chain , recording what is known about the evaluation that produced (for example, : defined and continuous on a bounded box with a bounded result). NaI (“not an interval”) is the decorated empty set with . Operations propagate decorations by taking the minimum of the inputs’ decorations and the decoration of the operation on that box.
Overlap states
The overlap relation of two intervals has sixteen values: the thirteen
relations of Allen’s interval algebra for two nonempty intervals (before,
meets, overlaps, starts, containedBy, finishes, equals and their
converses) and three values for empty arguments. The package also maps a
NaI argument to undefined.
The pass rule
For an interval-valued case with actual result and expected , the case passes when
where holds when both are empty or both are
nonempty with and , comparing bounds
numerically (BinFloat::compare == 0, so , as in IEEE 1788 where
intervals are sets of reals). A number-valued case passes when the actual
number compares equal to the expected bound; a boolean case when the booleans
are equal; an overlap case when the state names are equal.
Design decisions
Execute against the public ball_float API
Each ITL operation maps to one public method of
@ball_float.BallFloatDecorated (for example add to +, sqrt to
sqrt_interval, pown to pown, overlap to overlap_state), and
results are rounded with BallContext::binary64(). Testing through the
public API means the corpus checks exactly what users call, including the
decoration logic.
Reading bounds
Hexadecimal bounds 0x…p… are parsed exactly as an integer significand and a
binary exponent, then rounded to the working precision. Decimal bounds are
parsed as a decimal with digits and converted to binary with one
rounding to nearest-even at bits. For a literal with at most
significant digits the decimal parse is exact, so the bound is rounded once.
Rounding to nearest rather than outward is a simplification: it is exact for
bounds that are binary64 numbers, but a decimal bound such as 0.1 is read as
the nearest binary64 number, which may lie inside or outside the interval the
literal denotes.
Decorations only when the case states one
ITL writes undecorated expectations ([4.0,6.0]) for the set-based tests and
decorated ones ([4.0,6.0]_com) for the decoration tests. The executor parses
an undecorated literal as but compares decorations only when the
expected text contains _, so set-based cases are not failed by the decoration
the implementation attaches.
Three dispositions and a strict summary
Unsupported marks cases the library does not implement (unknown operations
such as the reverse operations mulRevToPair, or an expectation with a
signal annotation). Diagnostic marks cases whose data cannot be read.
RunSummary::success fails on any failed case and on any diagnostic,
because unreadable data in a pinned corpus is a defect of the parser or the
corpus, not an excluded feature. Unsupported cases do not fail success; the
CLI’s --strict-supported turns them into a failing exit code for the phases
that claim full support.
Correctness / invariants
Counter identities. Every result has exactly one disposition, so and .
Soundness of a pass. If an interval-valued case passes, the actual bounds equal the expected bounds. When the expected value is the tightest binary64 enclosure, the actual result is then both an enclosure of the range and tightest; when the corpus only promises an enclosure (accurate rather than tightest operations), a pass shows that the implementation reached the same bounds.
Determinism. Parsing and execution depend only on the text and
precision; results do not depend on the order in which cases are executed,
so a caller may filter or reorder cases freely.
Totality. Every completed statement becomes a case or a parse diagnostic,
and execute_case never aborts on case content: every unreadable input is
reported through a disposition.
Alternatives rejected
- Containment-only checking (). It would accept results that are many ulps too wide and hide accuracy regressions.
- Always comparing decorations. It would fail set-based cases on the default decoration, although those cases make no decoration claim.
- Treating signals as passes. IEEE 1788 signals (for example
UndefinedOperation) are not observable through the current API, so such cases are reported as not executed rather than silently passed.
Boundaries
- Reverse operations,
mulRevToPair, string conversions and exception signals are not executed. - Decimal bounds are rounded to nearest, not outward.
- Interval results are always rounded to binary64;
precisiononly affects how bounds are read. - Block comments are recognized only when
/*starts a line. - No file IO and no operation filtering; both are in
cli/itl_expr_cli.
Footnotes
-
IEEE Std 1788-2015, IEEE Standard for Interval Arithmetic. The set-based flavor, decorations (clause 8) and the overlap relation (clause 10.6.4) are the parts exercised here. ↩