用前置/后置条件与循环不变式形式化证明正确性

形式化正确性证明把程序验证变成一个逻辑推导过程：从前置条件（程序开始执行时假定成立的输入条件）出发，逐条语句推导出”若这条语句执行前某个断言成立，执行后什么断言随之成立”，一路推到程序末尾，如果得到的结论恰好等于期望的后置条件（输出规格），程序就被证明是正确的，而不是靠试跑几个例子来”相信”它正确。循环结构的证明依赖循环不变式——一个在循环每次做终止测试时都成立的断言（如插入排序里”每次测试时，列表前 N-1 个位置已排好序”），只要能证明这个不变式配合终止条件足以推出后置条件，循环部分的正确性就成立。发散：这种方法的价值在于把”正确性”从一种依赖直觉、容易被表面现象误导的判断（如金链问题的错误答案），转化成一条可以逐步验证的逻辑链条，SPARK 等语言把前置条件、后置条件和循环不变式直接写进代码本身，让编译器辅助完成这条推导链，这类技术已被用在航空和核安全等对正确性零容忍的关键系统里。