不变式

在程序执行过程中始终为真的断言，用于表达规格和进行程序推理，是形式化验证的核心概念之一。