用形式化方法做规格驱动开发：捕捉需求冲突

文章用一个文档应用加回收站与恢复功能的最小案例，演示形式化方法如何在需求变更时捕捉彼此合理却无法同时成立的冲突。作者用 FizzBee 编写规格，以 UniqueNames 安全属性和 FreeNamesUsable 活性属性检查硬删除版本，并指出仅改一行、加一行的需求变更就可能引入难以察觉的不一致。