frontend/itl_expr 设计

设计目标

ITF1788 项目以一种小型语言 ITL 发布了针对 IEEE 1788-2015¹1 IEEE Std 1788-2015，IEEE Standard for Interval Arithmetic。此处涉及的是其中基于集合的风格（set-based flavor）、装饰（decoration）（第 8 条）以及重叠关系（第 10.6.4 条）。的区间测试用例。本包针对 ball_float 执行这些用例，使 ball_float 符合性页面中关于区间的结论建立在一个外部的、固定版本的测试语料之上。与其他前端一样，它是纯的：输入文本，输出结果，不做任何 IO。

数学背景

区间与最紧结果

在基于集合的模型中，区间是 $\mathbb{R}$ 的闭连通子集：空集、整条实数轴，或满足 $-\infty \le a \le b \le +\infty$ 的 $[a, b]$ （无穷端点为开）。对于运算 $f$ 和区间 $X_1, \dots, X_n$ ，其值域为在 $f$ 有定义之点上取的 $f(X_1, \dots, X_n) = \{ f(x_1, \dots, x_n) : x_i \in X_i \}$ 。在数值格式 $\mathbb{F}$ （此处为 binary64）中，最紧结果是包含值域凸包的最小 $\mathbb{F}$ -区间：

\operatorname{tight}_{\mathbb{F}}(f, X) = \Bigl[\, \max\{ a \in \mathbb{F} : a \le \inf f(X) \},\; \min\{ b \in \mathbb{F} : b \ge \sup f(X) \} \,\Bigr].

对于 IEEE 1788 要求必须最紧的运算，ITF1788 用例将这一最紧区间列为期望值。因此，对端点做相等比较的测试同时检验两件事：包含性（结果包络值域）与最紧性（没有任何端点宽出一个或更多 ulp）。

装饰

带装饰区间是一个二元组 $(X, d)$ ，其中 $d$ 取自链 $\mathsf{com} > \mathsf{dac} > \mathsf{def} > \mathsf{trv} > \mathsf{ill}$ ，用于记录关于产生 $X$ 的那次求值的已知信息（例如 $\mathsf{com}$ 表示：在有界盒上有定义且连续，且结果有界）。NaI（“not an interval”，非区间）是带有 $\mathsf{ill}$ 装饰的空集。运算传播装饰的方式是：取各输入装饰与该运算在此盒上的装饰中的最小者。

重叠状态

两个区间的重叠关系共有十六种取值：两个非空区间之间 Allen 区间代数的十三种关系（before、meets、overlaps、starts、containedBy、finishes、equals 及其逆关系），以及针对空参数的三种取值。本包还将 NaI 参数映射为 undefined。

通过规则

对于区间值用例，设实际结果为 $(A, d_A)$ 、期望值为 $(E, d_E)$ ，用例通过的条件是

\bigl(A = \text{NaI} \wedge E = \text{NaI}\bigr) \;\vee\; \Bigl( \operatorname{sets}(A, E) \wedge \bigl(\text{no `\_` in the expected text} \vee d_A = d_E\bigr) \Bigr),

其中 $\operatorname{sets}(A, E)$ 成立当且仅当二者均为空，或二者均非空且 $\inf A = \inf E$ 、 $\sup A = \sup E$ ；端点按数值比较（BinFloat::compare == 0，因此 $-0 = +0$ ，这与 IEEE 1788 中区间是实数集合的观点一致）。数值型用例在实际数值与期望端点比较相等时通过；布尔型用例在布尔值相等时通过；重叠用例在状态名相等时通过。

设计决策

针对公开的 `ball_float` API 执行

每个 ITL 运算对应 @ball_float.BallFloatDecorated 的一个公开方法（例如 add 对应 +，sqrt 对应 sqrt_interval，pown 对应 pown，overlap 对应 overlap_state），结果使用 BallContext::binary64() 舍入。通过公开 API 进行测试，意味着测试语料检验的正是用户实际调用的内容，包括装饰逻辑。

读取端点

十六进制端点 0x…p… 被精确解析为一个整数有效数字和一个二进制指数，然后舍入到工作精度。十进制端点被解析为具有 $2p + 16$ 位数字的十进制数，再以一次就近舍入（偶数优先）在 $p$ 位上转换为二进制。对于有效数字不超过 $2p + 16$ 位的字面量，十进制解析是精确的，因此端点只被舍入一次。采用就近舍入而非向外舍入是一种简化：对于本身就是 binary64 数的端点它是精确的，但像 0.1 这样的十进制端点会被读作最近的 binary64 数，而它可能位于该字面量所表示区间的内部或外部。

仅在用例声明装饰时比较装饰

ITL 对基于集合的测试写出不带装饰的期望值（[4.0,6.0]），对装饰测试写出带装饰的期望值（[4.0,6.0]_com）。执行器将不带装饰的字面量解析为 $\mathsf{com}$ ，但仅当期望文本包含 _ 时才比较装饰，因此基于集合的用例不会因实现附加的装饰而失败。

三种处置结果与严格汇总

Unsupported 标记库未实现的用例（未知运算，例如反向运算 mulRevToPair，或带有 signal 注解的期望值）。Diagnostic 标记数据无法读取的用例。RunSummary::success 在任何用例失败以及出现任何诊断时都会失败，因为固定版本语料中无法读取的数据是解析器或语料本身的缺陷，而不是被排除的功能。不支持的用例不会使 success 失败；CLI 的 --strict-supported 会将它们变为失败的退出码，用于那些声称完全支持的阶段。

正确性 / 不变式

计数恒等式。 每个结果恰有一种处置结果，因此 $\text{total} = \text{executable} + \text{unsupported} + \text{diagnostic}$ ，且 $\text{executable} = \text{passed} + \text{failed}$ 。

通过的可靠性。 若一个区间值用例通过，则实际端点等于期望端点。当期望值是最紧的 binary64 包络时，实际结果因此既包络值域又是最紧的；当语料只承诺包络（即精确（accurate）而非最紧的运算）时，通过表明实现得到了相同的端点。

确定性。 解析与执行只依赖于文本和 precision；结果不依赖于用例的执行顺序，因此调用者可以自由地筛选或重排用例。

完全性。 每个完整的语句都会成为一个用例或一条解析诊断，且 execute_case 绝不会因用例内容而中止：每个无法读取的输入都通过处置结果报告。

被否决的替代方案

仅检查包含性（ $E \subseteq A$ ）。这会接受宽出许多 ulp 的结果，从而掩盖精度退化。
始终比较装饰。 这会让基于集合的用例因默认装饰而失败，尽管这些用例并未对装饰作任何声明。
将信号视为通过。 IEEE 1788 的信号（例如 UndefinedOperation）无法通过当前 API 观察到，因此这类用例被报告为未执行，而不是被静默地判为通过。

边界

反向运算、mulRevToPair、字符串转换和异常信号均不执行。
十进制端点采用就近舍入，而非向外舍入。
区间结果总是舍入到 binary64；precision 只影响端点的读取方式。
仅当 /* 位于行首时才识别块注释。
不提供文件 IO，也不提供运算筛选；二者都在 cli/itl_expr_cli 中。

IEEE Std 1788-2015，IEEE Standard for Interval Arithmetic。此处涉及的是其中基于集合的风格（set-based flavor）、装饰（decoration）（第 8 条）以及重叠关系（第 10.6.4 条）。 ↩