1小步操作语义
闭卷重建小步操作语义的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2大步操作语义
闭卷重建大步操作语义的对象、公式、算例、算法与失败边界。
3表达式求值与未定义行为
闭卷重建表达式求值与未定义行为的对象、公式、算例、算法与失败边界。
4顺序、条件与循环规则
闭卷重建顺序、条件与循环规则的对象、公式、算例、算法与失败边界。
5非确定选择
闭卷重建非确定选择的对象、公式、算例、算法与失败边界。
6异常、断言与卡死
闭卷重建异常、断言与卡死的对象、公式、算例、算法与失败边界。
7语义等价与精化
闭卷重建语义等价与精化的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：大步语义直接关联初始状态与终止结果，简洁但不直接表示发散和中间交错。；公式：⟨C,σ⟩⇓σ′。；算例：x=1执行x:=x+2;y:=x得终态x=3,y=3。；边界：用大步“无推导”区分不了发散与卡死。。
对象：小步语义用配置间单步转移刻画执行过程，适合并发与中间状态。；公式：⟨C,σ⟩→⟨C′,σ′⟩。；算例：σ(x)=2，执行x:=x+1一步后命令skip且σ′(x)=3。；边界：规则重叠导致非确定性；赋值先后状态混淆。。
对象：顺序把中间状态接力；条件由布尔守卫选分支；循环可展开为条件。；公式：while b do C ≡ if b then(C;while b do C) else skip。；算例：x=2时while x>0做x:=x−1，经过2轮到0。；边界：守卫在旧状态反复求值；分支条件未覆盖错误值。。
对象：语义必须明确整数宽度、除零、溢出、短路和求值顺序。；公式：eval(e,σ)∈Value∪Error。；算例：8位无符号255+1若模算术则0；若检查语义则overflow错误。；边界：数学整数证明直接套到有限整数实现。。
对象：assert失败、异常抛出和无可用转移要在语义中分别建模。；公式：assert b: b真→skip，b假→Error。；算例：x=0执行assert x>0进入Error而非正常终态。；边界：异常路径被后置条件忽略；卡死被误当成功终止。。
对象：非确定语义保留所有允许后继；验证通常要求所有选择满足性质。；公式：Post(s)=⋃_{a∈Enabled(s)}Post_a(s)。；算例：动作使x加1或减1，x=0后继集合{-1,1}。；边界：只验证幸运分支；把随机概率与非确定允许集混同。。
对象：程序等价要求可观察行为相同；精化允许实现减少非确定性但不得新增违规行为。；公式：Beh(Impl)⊆Beh(Spec)。；算例：规格允许返回1或2，实现固定返回1，行为集合{1}⊆{1,2}，是精化。；边界：忽略时间/异常等可观察行为；把子集方向写反。。