1类型安全的进展与保持
闭卷重建类型安全的进展与保持的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2精化类型
闭卷重建精化类型的对象、公式、算例、算法与失败边界。
3依赖类型与命题即类型
闭卷重建依赖类型与命题即类型的对象、公式、算例、算法与失败边界。
4证明助理与内核检查
闭卷重建证明助理与内核检查的对象、公式、算例、算法与失败边界。
5归纳证明与递归程序
闭卷重建归纳证明与递归程序的对象、公式、算例、算法与失败边界。
6程序抽取与已验证组件
闭卷重建程序抽取与已验证组件的对象、公式、算例、算法与失败边界。
7证明维护、自动化与可读性
闭卷重建证明维护、自动化与可读性的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：精化类型把普通类型与逻辑谓词结合，让函数接口携带数值或结构约束。；公式：{x:Int|x>0}。；算例：除法器分母类型要求d≠0，调用d=2通过，d=0产生VC失败。；边界：精化谓词含不可判定函数导致检查不终止。。
对象：类型安全常由进展与保持组成：良类型项非值则能走一步，走步后类型不变。；公式：Progress∧Preservation⇒no stuck。；算例：整数1+2良类型且一步到3，结果仍为Int。；边界：有异常/IO仍使用纯语言进展定义；把终止当进展。。
对象：证明助理的策略生成证明项，小可信内核只检查证明项是否有目标类型。；公式：Γ⊢term:P。；算例：若已有p:P和f:P→Q，应用f p得到Q的证明项。；边界：只保存交互会话；引入classical/choice未披露。。
对象：依赖类型可让类型依赖值；证明项是命题类型的居民。；公式：Vec A n；proof:P。；算例：长度3向量与长度2向量不能直接zip；类型层阻止尺寸错。；边界：用不安全公理填洞后仍声称证明无假设。。
对象：从构造性证明可抽取程序，或证明手写程序实现函数规约；仍需验证外部接口和性能。；公式：proof ∃y.R(x,y) yields witness program。；算例：证明每个自然数n存在n+1，见证函数f(n)=n+1。；边界：证明数学函数后忽略栈溢出和机器整数。。
对象：递归数据和函数通常用结构归纳；归纳假设对应递归调用的正确性。；公式：P([])∧(P(xs)⇒P(x::xs))⇒∀xs.P(xs)。；算例：证明length(append xs ys)=length xs+length ys：空表成立，cons步用IH。；边界：对错误变量归纳导致IH不够强；循环论证。。
对象：稳定证明依赖合适抽象和命名引理；过度依赖脆弱自动化会随实现小改大面积失败。；公式：maintenance_cost≈changed_obligations/total。；算例：100个义务因改动失效15个，失效率15%。；边界：一条万能自动化脚本无中间意图；证明靠未固定依赖。。