- [√ ] 我已搜索现有 issue,确认此功能之前未被提议过
这解决了什么问题?
解决以下几个部分:
1、设计逻辑是否正确的自动化验证。
2、实现是否和设计完全一致的自动化验证。
建议的方案
想法-》头脑风暴-》需求文档-》bdd建模验证-》tla+建模验证-》lean4证明-》特定开发工作测试验证夹具(例如rust可以Kani(AWS,基于 CBMC)进行模型检测;Prusti(基于 Viper)支持契约推理;Creusot(基于 Why3)翻译为 SMT 验证条件)-》编码实现-》利用夹具自动测试验证回归-》验收通过后提交
你考虑了哪些替代方案?
可能特定语言开发有更加方便地证明验证工具,但当前方案对多种软件开发工作都有效
这适合放在核心 Superpowers 中吗?
合适,这是在补全工作流
上下文
这解决了什么问题?
解决以下几个部分:
1、设计逻辑是否正确的自动化验证。
2、实现是否和设计完全一致的自动化验证。
建议的方案
想法-》头脑风暴-》需求文档-》bdd建模验证-》tla+建模验证-》lean4证明-》特定开发工作测试验证夹具(例如rust可以Kani(AWS,基于 CBMC)进行模型检测;Prusti(基于 Viper)支持契约推理;Creusot(基于 Why3)翻译为 SMT 验证条件)-》编码实现-》利用夹具自动测试验证回归-》验收通过后提交
你考虑了哪些替代方案?
可能特定语言开发有更加方便地证明验证工具,但当前方案对多种软件开发工作都有效
这适合放在核心 Superpowers 中吗?
合适,这是在补全工作流
上下文