1Hoare三元组语义
闭卷重建Hoare三元组语义的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2赋值公理
闭卷重建赋值公理的对象、公式、算例、算法与失败边界。
3顺序组合规则
闭卷重建顺序组合规则的对象、公式、算例、算法与失败边界。
4条件规则
闭卷重建条件规则的对象、公式、算例、算法与失败边界。
5后果规则
闭卷重建后果规则的对象、公式、算例、算法与失败边界。
6数组读写与边界
闭卷重建数组读写与边界的对象、公式、算例、算法与失败边界。
7函数调用与模块契约
闭卷重建函数调用与模块契约的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：赋值规则从后置把目标变量替换为右侧表达式。；公式：{Q[E/x]} x:=E {Q}。；算例：要求后置x≥10，执行x:=y+1，前置为y+1≥10即y≥9。；边界：写成Q[x/E]；有副作用表达式仍按纯表达式处理。。
对象：三元组表示从任何满足P的状态执行C，若终止则结果满足Q。；公式：⊨{P}C{Q}。；算例：{x=2} x:=x+1 {x=3}有效；后置x=4无效，反例初态x=2。；边界：把一个成功运行当全称有效。。
对象：两个分支分别在P∧b和P∧¬b下证明同一Q。；公式：{P∧b}C1{Q}∧{P∧¬b}C2{Q}。；算例：程序取绝对值：x≥0保留x，否则取-x；两支都得x≥0。；边界：只证then分支；浮点NaN使b与¬b覆盖失败。。
对象：若第一段建立中间断言R且第二段从R建立Q，则顺序程序成立。；公式：{P}C1{R}∧{R}C2{Q}⇒{P}C1;C2{Q}。；算例：x=1先加2得R:x=3，再乘4得Q:x=12。；边界：中间断言前后变量版本不一致。。
对象：数组语义需同时证明索引合法、读写值关系和未修改位置。；公式：store(a,i,v)[j]=if i=j then v else a[j]。；算例：a=[4,5],写a[1]=9后a[0]=4,a[1]=9；i=2越界。；边界：只证目标位置；整数溢出使边界判断失效。。
对象：可加强前置或减弱后置，通过逻辑蕴含连接已证三元组。；公式：P⇒P′,{P′}C{Q′},Q′⇒Q。；算例：已证后置x=5，可推出较弱x>0；不能推出x=6。；边界：蕴含方向反；把等价当必要。。
对象：调用者只依赖被调函数契约；被调者证明实现满足契约，支持模块化验证。；公式：Pre_caller⇒Pre_f；Post_f⇒Need_caller。；算例：函数要求n≥0，调用点n=3满足；n=-1需先分支或加强前置。；边界：偷偷使用函数实现细节；别名让modifies范围扩大。。