程序循环变式与不变式循环变式（Loop variant）及循环不变式（Loop invariant）是判断循环正确性的工具
循环变式是一个初值不为负的整数表示式，在每次运行循环时循环变式的数值需减少，但在正常的循环运行过程中循环变式的数值不会变成负值
循环变式用来确保循环会结束
循环不变式是一个和循环有关的判断式，在第一次进入循环之前，循环不变式的值需为真，在后续每一次运行循环时，其值也要为真
当循环正确的结束时，其终止条件和循环不变式都会成立
循环不变式可用来监控在循环进行时，某一指定性质的状态
像是Eiffel之类的编程语言本身就有支持循环变式及循环不变式，其他语言可能需要有附加组件才能支持此功能，例如Java就需要配合Java建模语言（Java Modeling Language）规范的loop statements才能支持此机能
以上内容由大学时代综合整理自互联网，实际情况请以官方资料为准。
