知识卡片
不变量形式化思考的价值
内容
不变量（永远为真的断言，如”一个人不能和同一个人建立多次联系”）可以用导航（沿关联在模型中遍历）精确描述，甚至写成对象约束语言（OCL）这样的形式化表达式。即使没有工具能真正校验这段OCL，把它写出来的过程本身就有价值：用自然语言写不变量时会不自觉想让它更精确，一旦感到模糊就会逼自己重新推敲——这是贯穿架构建模的更大主题：不一定要用形式化机制，但要懂得如何形式化，这本身就能带来更高质量的模型。
参考来源
- 位置：《恰如其分的软件架构》第8章《领域模型》8.3节《导航和不变量》（源文件：_epub-src/OEBPS/text00079.html）
- 结论依据：原文举例用OCL精确表达不变量，并指出即使没有工具校验OCL、写形式化表达的过程本身也有价值，用自然语言写不变量时会不自觉追求精确，说明"懂得如何形式化"本身就能提升模型质量。
- 原始内容：除非计算机能帮助你读取并检查OCL，否则，花这么大的力气来写，似乎有点得不偿失。不管怎样，OCL的确对精确思考有很大的帮助……即使你并没有采用形式化的机制，也要懂得如何对某些事情进行形式化，从而获得高质量的模型。