1抽象解释与保守近似
闭卷重建抽象解释与保守近似的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2区间域
闭卷重建区间域的对象、公式、算例、算法与失败边界。
3符号域与常量传播
闭卷重建符号域与常量传播的对象、公式、算例、算法与失败边界。
4数据流方程与不动点
闭卷重建数据流方程与不动点的对象、公式、算例、算法与失败边界。
5加宽与变窄
闭卷重建加宽与变窄的对象、公式、算例、算法与失败边界。
6空值、别名与逃逸分析
闭卷重建空值、别名与逃逸分析的对象、公式、算例、算法与失败边界。
7污点、信息流与误报管理
闭卷重建污点、信息流与误报管理的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：区间域跟踪变量上下界，连接取包络，精度有限但便宜。；公式：[a,b]⊔[c,d]=[min(a,c),max(b,d)]。；算例：[0,2]与[5,7]连接为[0,7]，引入不存在的3、4。；边界：除法跨零未处理；把区间内每值都当可达。。
对象：抽象解释在有限抽象域上计算所有具体行为的过近似，保证不漏真错误但可能误报。；公式：γ(F#(a))⊇F(γ(a))。；算例：区间x∈[0,2]执行x:=x+1得到[1,3]，覆盖全部具体结果。；边界：使用欠近似却声称安全；抽象运算不保序。。
对象：静态分析在CFG上反复传播，直到所有节点抽象状态稳定。；公式：IN[n]=⊔_{p∈pred(n)}OUT[p]。；算例：节点两个前驱OUT区间[0,1]和[2,3]，IN为[0,3]。；边界：只扫一遍带回边CFG；错误初始化导致漏报。。
对象：常量传播抽象值为具体常量、未知Top和不可达Bottom。；公式：join(3,3)=3；join(3,4)=⊤。；算例：if分支分别令x=1和x=2，汇合后x=Top。；边界：Top与Bottom混淆；未执行分支参与连接。。
对象：对象分析需近似指向集合，别名使一次写影响多个名字。；公式：Pts(x)∩Pts(y)≠∅表示可能别名。；算例：Pts(x)={o1,o2},Pts(y)={o2}，交集{o2}非空，可能别名。；边界：把may-alias当must-alias；反射/外部调用未建模。。
对象：无限升链上用widening强制收敛，再用narrowing恢复部分精度。；公式：[0,n]▽[0,n+1]=[0,+∞]（典型区间加宽）。；算例：循环x从0递增，区间0,1,2…加宽为[0,+∞]。；边界：过早全变Top导致无用；变窄不保证终止仍无限迭代。。
对象：污点分析追踪不可信源到敏感汇的路径，sanitizer需按上下文建模。；公式：taint(out)=join(taint(inputs)) unless validated。；算例：用户输入经字符串拼接到SQL汇，未参数化则存在路径；HTML转义不能净化SQL。；边界：只按函数名认净化；压制告警不记录理由。。