多面体抽象域

约束方向随程序关系而变化 ​

区间只保存每个变量独立的范围；多面体则可以保存 $y=2x$、$3x-5y\le 7$ 等关系，约束的方向不受预设模板限制。赋值、过滤和汇合分别对应投影、半空间相交和闭凸包。每一步都在操作同一个对象：当前程序点可能状态的外包络。

这种表达力仍受凸性约束。若程序只可能落在两条分离线段上，多面体必须同时包含线段之间的凸组合。单条仿射赋值即使精确地映射了这个外包络，也不会自动识别哪些输入点来自汇合时填入的空隙。“转移精确”与“整个分析等于真实可达集”是两个不同结论。

消元为什么在实数上精确 ​

消去一个实数旧变量 $u$ 时，把含 $u$ 的每行按系数正负整理成上界 $u\le U_i(z)$ 或下界 $u\ge L_j(z)$；系数为零的行只约束剩余变量 $z$，原样保留。存在满足这些界的 $u$ 当且仅当

以及所有不含 $u$ 的行同时成立。必要性来自任一下界不超过任一上界；充分性来自有限个下界的最大值不超过有限个上界的最小值，可在两者之间选取 $u$。若只有上界或只有下界，总能向无界的一侧选择实数；若两侧都没有，任选 $u$ 即可。

这就是 Fourier–Motzkin 消元的一步。反复消去旧变量便得到赋值后的 H-表示，同时也说明其成本来源：一次消元可能把上、下界成对组合，约束数量会迅速增长。冗余删除能减少表示长度，却不改变所得集合。

从两个分支到一份完整断言证书 ​

下面的 nondet() 非确定地选择任一分支；所有变量均为无界精度实数。

x := input_real(); assume 0 <= x <= 2
if nondet(): y := 2*x
else:        y := 2*x+2
assume y <= 3
x := 2*x+y
assert 2*y-2 <= x and x <= 2*y and x <= 6

赋值后的两个分支分别是线段

它们的 join 为

验证等号的两边也很直接：右侧是包含两段的凸集；反过来，每个 $(x,y)\in J$ 都是同一横坐标处 $(x,2x)$ 与 $(x,2x+2)$ 的凸组合，权重为 $(y-2x)/2\in [0,1]$。四个顶点依次是 $(0,0),(2,4),(2,6),(0,2)$。点 $(0,1)$ 已被 join 纳入，却不属于任一分支。

guard 将 $J$ 与 $y\le 3$ 相交。所得 $H$ 的顶点依次为

最后一次赋值需要区分旧 $x$ 与新 $x$。把旧值记为 $u$，保留未改变的 $y$，完整关系是

用 $u=(x-y)/2$ 消元，先得到

其中 $y\le x\le 2y$ 蕴含 $y\ge 0$；又因为 $y\le 3<4$，有 $x\le 2y\le y+4$，所以 $x\le y+4$ 冗余。最终结果是

这不是只列出必要条件：若 $(x,y)\in Q$，取 $u=(x-y)/2$，上述推导可逆，便恢复完整旧状态关系。于是 $Q$ 正好是 $H$ 的仿射像。其顶点是 $(0,0),(6,3),(4,3),(2,2)$，分别由 $H$ 的四个顶点映射而来。

断言的前两项直接是 $Q$ 的约束；第三项由 $x\le 2y\le 6$ 得出。上界 $6$ 在第一分支的旧状态 $(u,y)=(3/2,3)$ 处达到，故它还是本例真实执行的精确最大值。

这份安全证书没有声称 $Q$ 中每个点都可达。真实终态只有

例如 $(1,1)\in Q$，却不在这两段上；它来自先前的伪状态 $(0,1)$。沿控制流复合可靠包含关系，足以证明所有真实执行满足断言，无需把这个空隙重新分开。

为什么 join 要取闭包 ​

取原点 $O=\{(0,0)\}$ 与直线 $L=\{(1,y):y\in \mathbb{R}\}$。普通凸包在 $x>0$ 时包含整条竖线，但在 $x=0$ 时只包含原点：

例如 $(1/k,1)$ 都在其中，极限 $(0,1)$ 却不在。因此普通凸包不是闭多面体，域内 join 必须补入极限，得到条带 $0\le x\le 1$。这与前例有界线段的 join 不同，不能把有界图形的直觉直接推广到无界输入。

整性、严格性与机器运算 ​

本页的消元依赖实数见证。若 $u$ 是整数，赋值 $x^{\prime }=2u$ 只产生偶整数；把该关系当实数系统投影会得到整条实线，不能保留奇偶性。用多面体外包络分析整数程序仍可可靠，但必须把“精确实数投影”与“精确整数可达集”分开。

非严格闭半空间也无法精确表达实数 guard $x<0$；换成 $x\le 0$ 是可靠外近似，会加入边界。浮点舍入、NaN 与机器整数回绕则改变赋值或比较的语义，必须另建可靠转移，不能套用这里的数学实数等式。

有限行删除如何迫使迭代停止 ​

关系更丰富并不会消除无限上升链。考虑

使用加宽与收窄公理库Widening 与 NarrowingWidening and narrowing · Widening operator · Narrowing operator以 widening 强制抽象迭代有限稳定，再用 narrowing 在可靠上界内恢复部分精度。时，一种容易核验的有限行删除方案是：固定 $R_0$ 的行表示，只保留被新候选 $N$ 蕴含的旧行。此处 $x\le 1$ 被删去，$x\ge 0$ 与表示 $y=2x$ 的两行保留，结果为

每条保留行原先在 $R_0$ 上成立，也经检查在 $N$ 上成立，所以结果同时包含两者。它保存了斜率关系，却主动放弃正在增长的上界。

终止论证有一个表示层面的前提：后续迭代始终从同一初始有限行集中删除，不能重新生成或插回已经删除的行。若初始有 $m$ 行，约束集合至多严格缩小 $m$ 次。对于单调程序方程 $F$，每步令候选包含 $R_k\cup F(R_k)$；当不再删除任何行时，全部当前行都被候选满足，故 $F(R_k)\subseteq R_k$，得到归纳不变量。

这里介绍的是带有明确历史限制的、依赖行表示的删除加宽。冗余行的选取会影响保留下来的信息，任意重新规范化后再删行不能沿用这份终止证明；完整的标准多面体加宽还需处理最小表示与约束替换等条件。加宽所得不变量也不保证是最小不动点。

选择此域需要的收益与代价 ​

本例的关键关系是斜率为二的边界。允许任意有理系数使这些边界在赋值后继续可表示，因而可以直接读取安全断言。收益来自保存程序所需的关系，不只是把每个变量的独立范围算得更紧。

代价同样来自自由方向：消元可能制造大量约束，凸包可能需要 H/V 表示转换，包含检查还要证明每条目标不等式被输入蕴含。实际分析常按变量组使用多面体，并在循环头谨慎安排加宽。本页提供的终点是可逐步复核的前向安全证书；若目标变成非凸路径区分、整数同余或非线性不变量，还需要另外的表示能力。