1循环不变量的三项义务
闭卷重建循环不变量的三项义务的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2计数循环不变量设计
闭卷重建计数循环不变量设计的对象、公式、算例、算法与失败边界。
3搜索与最大值不变量
闭卷重建搜索与最大值不变量的对象、公式、算例、算法与失败边界。
4排列、排序与多重集合
闭卷重建排列、排序与多重集合的对象、公式、算例、算法与失败边界。
5终止变式与良基关系
闭卷重建终止变式与良基关系的对象、公式、算例、算法与失败边界。
6嵌套循环与字典序变式
闭卷重建嵌套循环与字典序变式的对象、公式、算例、算法与失败边界。
7不变量发现与反例增强
闭卷重建不变量发现与反例增强的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：从已处理前缀、待处理后缀和目标关系系统构造不变量。；公式：I:0≤i≤n ∧ acc=Σ_{k< i}a[k]。；算例：a=[2,3,4]，i=2时acc=5，未处理a[2]=4。；边界：只写0≤i≤n没有功能信息。。
对象：不变量需初始化成立、循环体保持，退出时与守卫否定推出后置。；公式：P⇒I；{I∧b}C{I}；I∧¬b⇒Q。；算例：求和循环I:sum=i(i+1)/2且0≤i≤n；退出i=n得目标。；边界：只证明保持未证初始化；不变量太弱推不出Q。。
对象：排序证明需要有序性和元素守恒两部分；仅有序会允许丢元素。；公式：sorted(out) ∧ multiset(out)=multiset(in)。；算例：输入[2,1,2]输出[1,2,2]两性质均满足；[1,2]只满足有序。；边界：把集合代替多重集合丢掉重复计数。。
对象：遍历算法常用“结果是已扫描部分的最优值”作为不变量。；公式：I:maxv=max(a[0:i])，1≤i≤n。；算例：a=[3,1,5,2]，i=3时已扫[3,1,5]，maxv=5。；边界：初始化maxv=0使全负数组错误。。
对象：多层循环可用字典序元组；外分量下降时内分量可重置。；公式：(V1,V2) lexicographically decreases。；算例：从(2,0)到(1,100)仍字典序下降，因为首分量2→1。；边界：用分量和时重置造成上升而误判。。
对象：变式在循环中取良基集合值并每轮严格下降，证明不能无限执行。；公式：I∧b⇒V≥0 ∧ V′<V。；算例：i从0增到n，V=n−i；n=5,i=2时V=3，下一轮2。；边界：只证不增而非严格下降；自然数下界遗漏。。
对象：可从后置削弱、程序切点、模板求解和失败反例逐步增强候选不变量。；公式：I_{k+1}=I_k∧lemma(counterexample)。；算例：候选I:i≤n被反例i=-1击破，加入0≤i得到更强候选。；边界：盲目加入x=c过拟合单个反例；候选不可达却被接受。。