1谓词作为状态集合
闭卷重建谓词作为状态集合的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2最强后置条件
闭卷重建最强后置条件的对象、公式、算例、算法与失败边界。
3最弱前置条件
闭卷重建最弱前置条件的对象、公式、算例、算法与失败边界。
4谓词蕴含与条件强弱
闭卷重建谓词蕴含与条件强弱的对象、公式、算例、算法与失败边界。
5替换、捕获与旧值
闭卷重建替换、捕获与旧值的对象、公式、算例、算法与失败边界。
6关系语义与框架
闭卷重建关系语义与框架的对象、公式、算例、算法与失败边界。
7规约一致性与可实现性
闭卷重建规约一致性与可实现性的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：sp(P,C)描述从任一P状态执行C后可达到的最精确后状态集合。；公式：sp(P,x:=E)=∃x0.P[x0/x]∧x=E[x0/x]。；算例：P:x=2，执行x:=x+3，sp为x=5。；边界：直接在P中把新旧x混为同一值。。
对象：断言P既是状态上的布尔谓词，也表示所有满足P的状态集合。；公式：[[P]]={σ|P(σ)=true}。；算例：P:x≥0，在x∈{-1,0,1}中满足状态有0和1，共2个。；边界：把程序布尔值与元逻辑真假混淆。。
对象：更强条件满足状态更少；P⇒Q表示P的状态集合包含于Q。；公式：P stronger Q iff [[P]]⊆[[Q]]。；算例：x>5蕴含x>0，因此x>5更强，反向不成立。；边界：把“数值更大”误当逻辑更强；忽略域约束。。
对象：wp(C,Q)是保证C终止且Q成立的最宽输入集合。；公式：wp(x:=E,Q)=Q[E/x]。；算例：Q:x>5，C:x:=x+2，代入得前置x+2>5即x>3。；边界：代入方向反；数组赋值别名未处理。。
对象：命令可视为前后状态关系；框架条件约束未列出的变量保持。；公式：R_C(σ,σ′)∧∀v∉M.σ′(v)=σ(v)。；算例：命令只改x，初态y=7，则所有正常后态y仍为7。；边界：规格没写frame导致任意变量可改变。。
对象：逻辑替换必须避免变量捕获；规约需用old(x)区分调用前值。；公式：Q[E/x]为捕获避免替换。；算例：后置x=old(x)+1明确新旧关系；写x=x+1在纯逻辑中自相矛盾。；边界：量词变量捕获；old值在调用后才取样。。
对象：前置、后置和框架可能互相矛盾；应先检查是否存在实现关系。；公式：∃σ,σ′.P(σ)∧Q(σ,σ′)∧Frame。；算例：P:x=0，Q:x=1，frame禁止改x，则合取不可满足。；边界：矛盾规约使任意程序“证明”成立的爆炸效应。。