temporal-logic

无需学习时序逻辑即可对代码进行模型检验

像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。

使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。…