从相关程序到反例与归纳证书

本练习把三种证据接起来：依赖闭包说明为何可以缩小程序；一份重放输入说明断言确实失败；初始、保持和目标义务说明某个转移系统所有可达状态都安全。每份证据回答不同问题，不能互相替代。

配套：Python复算脚本、一次完整输出。脚本只用标准库，运行 python foundations-program-evidence-checker.py 即打印JSON；显式检查在 python -O 下仍启用。它不是一般源语言解析器或SMT后端；程序以固定语法对象输入，路径求解明确枚举 $[-2,2]^2$ ，状态系统明确枚举其给定有限全集。

任务一：给返回值建立完整相关性

模型是无循环结构化顺序程序，纯且总定义的数学整数表达式、每条读取有定义、无异常/堆/并发/I/O，唯一末尾返回。观察只包括返回值。

text

0  input x, y
1  a := x + 1
2  junk := y * y
3  r := 0
4  if x > 0:
5      if y == a:
6          r := 1
       else:
7          r := 2
8  junk := junk + 1
9  return r
10 exit

列出4、5、6、7的反身后支配集合
从每条分支出边的后支配集合差发出控制边
列出所有定义到使用边，对9说明为何有三个 r 来源
从9反向闭合，重建可执行切片；不能把互斥分支拼成顺序赋值

复算与检查点

四个后支配集合分别为 {4,8,9,10}、{5,8,9,10}、{6,8,9,10}、{7,8,9,10}。控制边恰为4→5(T)、5→6(T)、5→7(F)。数据边为0→1(x)、0→2(y)、0→4(x)、0→5(y)、1→5(a)、2→8(junk)、3→9(r)、6→9(r)、7→9(r)。

反向闭包保留 {0,1,3,4,5,6,7,9}，删除2和8；余下if结构不变。有限域25组输入上原程序和切片返回值逐一一致；对全部数学整数输入的保证来自静态切片中的语义对应证明。

迁移：把8改成 r:=junk，重新构图。切片应保留0、2、8、9，返回 $y^2$ 。若只往旧切片追加8，会读未定义变量。另说明把2改成可能除零的表达式后，当前删除保证为何不再适用。

任务二：从符号路径生成可重放错误

回到原程序，检查规格“返回值不等于1”。

用 $X,Y$ 代表输入，手算 a 的符号值
列出全部终端路径条件及返回表达式
在 $[-2,2]^2$ 内数出各路径包含的输入数量
从具体种子 $(0,0)$ 开始，采用最深未覆盖前缀优先、字典序首个模型，运行混合执行

复算与检查点

$a=X+1$ 。三条路径为 $X\le0$ 返回0； $X>0\land Y=X+1$ 返回1； $X>0\land Y\ne X+1$ 返回2。在25组输入中分别有15、1、9组。失败输入为 $(1,2)$ ，重放时 a=2，两个判断均真，6将 r 写为1。

混合执行依次运行 $(0,0)$ 、 $(1,-2)$ 、 $(1,2)$ 。第一次翻转4得到 $X>0$ ；第二次保持此前4T并翻转5F，得到 $X>0\land Y=X+1$ 。第三轮发现错误。每个SAT输入都必须重新运行并核对前缀，未完整处理的目标不能视为已覆盖。

迁移一：把6改成 r:=a-y。真路径有 $Y=X+1$ ，故返回0；其他路径返回0或2，当前断言在数学模型中成立。脚本也在有限域复算，二者证据范围分别报告。

迁移二：原程序输入域缩成 $\{-1,0,1\}^2$ ，5T不可行。只证明这个小域里没有错误，域外 $(1,2)$ 仍是反例。改变输入域必须使旧可行性缓存失效。

任务三：把乐观候选变成归纳事实

给定 $S=\{0,1,2,3,4\}$ 、 $I=\{0\}$ ，边为0→1、1→2、2→2、3→4、4→4。候选为

p_0:s>0,\quad p_1:s\ne1,\quad p_2:s\ne2,\quad p_3:s\le2,\quad p_4:s\ne4.

每轮采用同一当前合取，列出初始或保持失败见证
解释为什么候选删除后要重新检查其余候选
对最终合取分别检查初始化、一步保持和蕴涵 $s\ne4$
枚举32个候选子集，核验所有归纳子集均包含于最终保留集合

复算与检查点

先因初态0删除 $p_0$ ，再因0→1删除 $p_1$ ，再因1→2删除 $p_2$ ，第四轮不删除。剩余 $\{p_3,p_4\}$ ，合取允许0、1、2。初态包含、所有出边闭合、排除4三项均通过。枚举32个子集与正文的最大性证明一致；不把这32次枚举作为任意候选集合定理的证明。

迁移：新增2→3。接下来先删 $p_3$ ，再因3→4删 $p_4$ 。这次实际可达错误路径是0、1、2、3、4；应同时说明真实错误和候选失败，不只打印“推断失败”。

任务四：分开base与任意状态窗口

另取 $S=\{0,1,2,3\}$ 、 $I=\{0\}$ ，边为0→1、1→1、2→3、3→3，安全性质为 $P:s\ne3$ 。

按k归纳页约定，base检查深度0到 $k-1$ ，step检查 $k$ 个安全前态后的一步错误
给出 $k=1$ 的step反例，并判断它是否可达
证明 $k=2$ 两个义务均通过
添加2→2，构造对任意 $k$ 都失败的step窗口

复算与检查点

$k=1$ 的初态0安全，但step允许任意源状态，得到2、3。 $k=2$ 的base只有0和1；step要从某个安全状态进入2，再到3，可图上没有进入2的边，因此UNSAT。

加入2→2后，对任意 $k$ 可取 $k$ 个2再接3。这个无限族窗口不可达，却使基础k归纳一直失败。辅助不变式 $Q:s\le1$ 可独立通过初始化和一步保持，并蕴涵P，从而给出一步加强证书。脚本验证前8个深度，任意深度结论由该构造证明。

迁移：将初态改成2。原图的 $D_2$ 仍UNSAT，但 $B_2$ 在深度1发现2→3，所以系统不安全。再试“坏初态没有后继”的模型，检查base不能要求强制走满长度后才看错误。

验收清单

每条边有类型、方向及正文中可复算的来源
切片准则包含观察位置和值，静态结论不借用单次轨迹
反例输入满足完整路径条件并在原程序重放
有限域枚举、无界语义证明和工具求解结果分别标注
候选最终集合经过初始化与保持，安全目标另行检查
k归纳的base含I，step不含I；任意状态的失败不冒充可达错误
改变程序、初态或输入域后重新计算证据

从相关程序到反例与归纳证书 ​

任务一：给返回值建立完整相关性 ​

任务二：从符号路径生成可重放错误 ​

任务三：把乐观候选变成归纳事实 ​

任务四：分开base与任意状态窗口 ​

验收清单 ​

从相关程序到反例与归纳证书

任务一：给返回值建立完整相关性

任务二：从符号路径生成可重放错误

任务三：把乐观候选变成归纳事实

任务四：分开base与任意状态窗口

验收清单