software-design-skill

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)——落地为可执行的工程纪律。

本技能回答一个贯穿始终的问题：我们凭什么相信代码是对的？ 答案分三层：

1. 规范：用前置条件、后置条件、表示不变量、抽象函数，把"该做什么"写成精确、可检查的断言。
2. 推理：用霍尔逻辑、最弱前置条件、循环不变量，从数学上证明实现满足规范。
3. 验证：用 pytest + hypothesis 属性测试，在工程尺度上逼近"证明"的保证。

何时使用本技能

• 用户要写一个函数/类，但边界条件、错误行为、输入输出约束没说清 → 先写规范。
• 用户问"这段代码对吗"、"怎么证明这个循环正确"、"不变量怎么写" → 推理章节。
• 用户要设计数据结构/类，纠结字段该不该暴露、怎么封装 → 抽象数据类型章节。
• 用户要覆写 __eq__/__hash__、设计继承体系、判断子类型该不该继承 → 子类型/相等性章节。
• 用户写重复代码想用泛型消除、问协变/逆变 → 泛型章节。
• 用户要选设计模式、重构解耦、做可测试的架构 → 设计模式章节。
• 用户写测试但只测了几个手写例子 → 属性测试章节。

核心纪律（贯穿所有主题）

1. 规范先行：写实现前先写规范（前置/后置/不变量），否则无从判断"对错"。
2. 记号统一：见 references/glossary.md，全书只此一份，各主题引用。
3. 尽早失败 (fail fast)：前置条件违反、表示不变量被破坏，立即 assert 崩溃，不静默错。
4. 现代 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 对齐记号，再读对应主题章节。

典型工作流

1. 写规范：用 docstring（requires/modifies/effects）+ 类型注解 + assert 表达前置/后置/不变量。
2. 写测试：先写示例测试覆盖已知边界，再写 hypothesis 属性测试表达"对所有输入成立"的性质。
3. 推理（可选但推荐对关键路径）：对循环/递归，写出不变量，验证初始化/保持/终止三条义务。
4. 抽象：把字段藏起来，写清 RI 与 AF，在构造器 assert RI，用属性测试验证操作保 RI/AF。
5. 落地：需要复用就泛型化，需要解耦就套模式，Web 层用分层 + 依赖注入保持业务逻辑可测。

参考文件使用说明

• 参考章节是自包含的中文技术讲解（含数学推导 + 可运行 Python），按主题取用。
• 章节底部有前后章导航（HTML），index.md 提供全书目录与依赖图。
• 代码示例面向 Python 3.12+，测试依赖 pytest + hypothesis（pip install pytest hypothesis）。