1错误处理：返回值
怎么减少啰嗦？
计算机原理 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2可恢复与不可恢复
为什么要分开？
3不要吞掉异常
至少要做什么？
4契约式设计
这和断言什么关系？
5霍尔逻辑
循环怎么处理？
6最弱前置条件
这为什么有用？
7形式化验证
它和测试的根本区别？
8验证的代价
那什么场景值得？
9规约本身可能错
这说明什么？
10模型检验
它的瓶颈是什么？
第 1 页 · 背面（答案）
参考答案（家长）：bug 应该立刻暴露，而不是被 catch 掉悄悄继续。
参考答案（家长）：用语法糖，比如一个符号表示"出错就直接往上返回"。
参考答案（家长）：断言是契约的可执行形式。
参考答案（家长）：记日志，并且想清楚为什么这里可以忽略。
参考答案（家长）：能自动化，是程序验证工具的核心机制。
参考答案（家长）：找循环不变量，你在算法课里学过。
参考答案（家长）：航空、轨道交通、医疗设备、密码库、操作系统内核。
参考答案（家长）：测试证明存在错误，验证证明不存在错误。
参考答案（家长）：状态爆炸，状态数随组件数指数增长。
参考答案（家长）：形式化不能消除人的理解错误，只能消除实现错误。
第 2 页 · 正面（题目）
11应对状态爆炸
抽象会带来什么风险？
12定理证明器
它和模型检验怎么选？
13柯里－霍华德对应
这个发现有多重要？
14依赖类型
它能保证什么？
15渐进式的形式化
投入产出比最高的一步是什么？
16属性测试
排序函数有什么性质？
17属性测试的威力
它能替代单元测试吗？
18用例缩小
为什么这个功能重要？
19动手：写属性测试
动手做。
20静态分析
它为什么会有误报？
第 2 页 · 背面（答案）
参考答案（家长）：有限状态用模型检验自动化程度高，无限状态用定理证明。
参考答案（家长）：抽象掉了关键细节，可能验证出假的正确结论。
参考答案（家长）：比如数组访问永不越界，编译期就证明了。
参考答案（家长）：它把逻辑学和计算机科学统一了起来。
参考答案（家长）：输出有序、且是输入的一个排列。
参考答案（家长）：通常是引入静态类型和关键处的断言。
参考答案（家长）：随机生成的反例往往很大很乱，缩小后才看得懂。
参考答案（家长）：不能替代，两者互补，具体用例更好定位问题。
参考答案（家长）：受莱斯定理限制，只能做保守近似。
参考答案（家长）：很多人第一次跑就能发现边界 bug。
第 3 页 · 正面（题目）
21误报与漏报的取舍
安全扫描该偏向哪边？
22抽象解释
这样能得到什么结论？
23符号执行
它的瓶颈是什么？
24模糊测试
它和属性测试的区别？
25编程范式：命令式
它的困难在哪？
26编程范式：函数式
它的门槛在哪？
27编程范式：面向对象
它容易被误用在哪？
28组合优于继承
什么时候继承才合适？
29编程范式：声明式
它的好处是什么？
30多范式
数据处理流水线适合哪种？
第 3 页 · 背面（答案）
参考答案（家长）：如"这个除数区间不含零"，从而证明不会除零。
参考答案（家长）：宁可误报，漏掉漏洞的代价更大。
参考答案（家长）：模糊测试主要找崩溃，属性测试检查语义性质。
参考答案（家长）：路径数随分支指数增长。
参考答案（家长）：思维转换，以及某些场景下性能需要额外考虑。
参考答案（家长）：状态多了以后，很难推理某一刻的整体状态。
参考答案（家长）：确实是"是一个"的关系，且父类接口稳定。
参考答案（家长）：过度继承、为了对象而对象、把过程硬套成类。
参考答案（家长）：函数式，映射过滤归约的组合天然适配。
参考答案（家长）：实现可以被优化和替换，而你的描述不用改。