| name | software-design-skill |
| description | 软件设计与正确性工程技能，把"代码为什么是对的"变成可写、可证、可测的工程实践。 覆盖规范与契约(前置/后置条件)、霍尔逻辑与循环不变量、抽象数据类型(表示不变量 RI / 抽象函数 AF)、子类型与相等性(Liskov 替换、__eq__/__hash__ 契约)、泛型与变型、 设计模式，以及用现代 Python(类型注解、dataclass、pytest/hypothesis 属性测试) 实现正确软件。当用户需要编写/审查/证明软件正确性、写规范或契约、设计抽象数据类型、 做属性测试、讨论继承与相等性、或问及 Hoare 逻辑/不变量/里氏替换/设计模式时使用—— 即使用户没有明说"软件设计"、只是问"这段代码对吗"或"怎么写这个函数"也应主动触发。 |
软件设计技能 (Software Design Skill)
用现代 Python 把 UW CSE 331《Software Design & Implementation》的核心思想——
规范 (specification)、推理 (reasoning)、抽象 (abstraction)——落地为可执行的工程纪律。
本技能回答一个贯穿始终的问题：我们凭什么相信代码是对的？ 答案分三层：
- 规范：用前置条件、后置条件、表示不变量、抽象函数，把"该做什么"写成精确、可检查的断言。
- 推理：用霍尔逻辑、最弱前置条件、循环不变量，从数学上证明实现满足规范。
- 验证：用 pytest + hypothesis 属性测试，在工程尺度上逼近"证明"的保证。
何时使用本技能
- 用户要写一个函数/类，但边界条件、错误行为、输入输出约束没说清 → 先写规范。
- 用户问"这段代码对吗"、"怎么证明这个循环正确"、"不变量怎么写" → 推理章节。
- 用户要设计数据结构/类，纠结字段该不该暴露、怎么封装 → 抽象数据类型章节。
- 用户要覆写
__eq__/__hash__、设计继承体系、判断子类型该不该继承 → 子类型/相等性章节。
- 用户写重复代码想用泛型消除、问协变/逆变 → 泛型章节。
- 用户要选设计模式、重构解耦、做可测试的架构 → 设计模式章节。
- 用户写测试但只测了几个手写例子 → 属性测试章节。
核心纪律（贯穿所有主题）
- 规范先行：写实现前先写规范（前置/后置/不变量），否则无从判断"对错"。
- 记号统一：见
references/glossary.md，全书只此一份，各主题引用。
- 尽早失败 (fail fast)：前置条件违反、表示不变量被破坏，立即
assert 崩溃，不静默错。
- 现代 Python：类型注解覆盖公共 API；值对象用
@dataclass(frozen=True, slots=True)；
接口用 abc.ABC / typing.Protocol；泛型用 PEP 695（class Box[T]）；联合类型 int | None；
模式匹配 match/case；异常用 raise ... from 保留链。
主题 → 参考章节映射
| 主题 | 参考文件 | 关键内容 |
|---|
| 规范与过程抽象 | references/ch01_规范与过程抽象.md | 前置/后置条件、modifies、规范强弱关系 |
| 测试与属性测试 | references/ch02_测试与交互式程序.md | 示例 vs 属性测试、Hypothesis、覆盖率、异常 |
| 程序推理 | references/ch03_程序推理与霍尔逻辑.md | Hoare triple {P} S {Q}、最弱前置 wp(S,Q) |
| 循环不变量 | references/ch04_循环不变量.md | 初始化/保持/终止、归纳法、循环变体 |
| 抽象数据类型 | references/ch05_抽象数据类型.md | 表示不变量 RI、抽象函数 AF、表示泄漏 |
| 子类型与相等性 | references/ch06_子类型与相等性.md | LSP、等价关系、__eq__/__hash__ 契约 |
| 泛型与类型 | references/ch07_泛型与类型系统.md | PEP 695 泛型、协变/逆变/不变 |
| 设计模式 | references/ch08_设计模式.md | 9 个 GoF 模式的 Python 惯用法 |
| Web 工程应用 | references/ch09_Python_Web应用开发.md | FastAPI、分层、依赖倒置落地 |
| 记号约定 | references/glossary.md | 全书记号与中英术语对照 |
| 章节总览 | references/index.md | 目录、依赖关系、映射表 |
原则：按需读取相关章节，不必一次读完。写作/审查代码前，先 references/glossary.md
对齐记号，再读对应主题章节。
典型工作流
- 写规范：用 docstring（
requires/modifies/effects）+ 类型注解 + assert 表达前置/后置/不变量。
- 写测试：先写示例测试覆盖已知边界，再写
hypothesis 属性测试表达"对所有输入成立"的性质。
- 推理（可选但推荐对关键路径）：对循环/递归，写出不变量，验证初始化/保持/终止三条义务。
- 抽象：把字段藏起来，写清 RI 与 AF，在构造器
assert RI，用属性测试验证操作保 RI/AF。
- 落地：需要复用就泛型化，需要解耦就套模式，Web 层用分层 + 依赖注入保持业务逻辑可测。
参考文件使用说明
- 参考章节是自包含的中文技术讲解（含数学推导 + 可运行 Python），按主题取用。
- 章节底部有前后章导航（HTML），
index.md 提供全书目录与依赖图。
- 代码示例面向 Python 3.12+，测试依赖
pytest + hypothesis（pip install pytest hypothesis）。
