程序的不变式是一种逻辑断言，用于描述程序执行期间变量的状态。它在程序执行的特定点（通常是循环或函数体）恒定为真。不变式有助于理解和验证程序的正确性，检测和调试错误。根据其范围和目的，程序不变式可以分为以下几类：
局部不变式：
仅适用于程序的特定部分，例如循环或函数体。它们描述程序执行期间变量在一个特定范围内保持不变的条件。
全局不变式：
适用于整个程序，描述程序在整个执行期间变量间的关系。
不变式在安全性关键系统中发挥着至关重要的作用，可以提高软件质量，增强系统的可靠性和安全性，减少潜在的故障和安全漏洞。它们可以通过形式化规范、代码注释、单元测试等多种方式来定义和实现。
在循环的停机性验证中，程序不变式用于描述程序变量的取值关系。线性不变式可以帮助描述程序变量间的线性关系，而循环不变式能够有效刻画循环中的变量关系。基于这些不变式，可以自动地验证程序的停机性，并给出循环的复杂度上界。
总结来说，程序的不变式是程序设计和验证中一种重要的逻辑工具，用于确保程序在特定条件下始终为真，从而提高软件质量和系统的安全性。