当使用形式化方面来创建一些代码时，是否存在确定循环不变性的通用方法，或者根据问题而定，它会完全不同吗？
最佳答案
已经指出，一个相同的循环可以具有多个不变量，并且可计算性不利于您。这并不意味着您无法尝试。
实际上，您正在寻找一个归纳不变式：“不变式”一词也可以用于在每次迭代中都是正确的属性，但是对于它而言，仅仅知道它在一次迭代中成立就不足以推论它在“迭代”中成立。下一个。如果I是一个归纳不变式，则I的任何结果都是一个不变式，但可能不是归纳不变式。
您可能正在尝试获取一个归纳不变式，以证明在某些已定义的情况（前提条件）下循环的某个属性（前提条件）。
有两种启发式方法非常有效：
从您拥有的东西（前提条件）开始，然后减弱直到您有一个归纳不变式。为了获得如何减弱的直觉，请应用一次或多次前向循环迭代，并查看公式中哪些不再是正确的。
从您想要的内容（后置条件）开始，并进行强化，直到您得到归纳不变式为止。要获得如何加强直觉的方法，请向后应用一个或多个循环迭代，并查看需要添加的内容，以便可以推导出后置条件。
如果您希望计算机在实践中为您提供帮助，我可以建议Jessie的C程序的Frama-C演绎验证插件。还有其他一些，尤其是对于Java和JML注释，但是我对它们并不熟悉。尝试您想到的不变式要快于在纸上进行计算。我应该指出，也无法确定属性是否为归纳不变式，但现代自动证明在许多简单示例中都非常有用。如果您决定走这条路线，请从列表中获取尽可能多的内容：Alt-ergo，Simplify，Z3。
有了可选的（且安装起来有点困难）的Apron库，Jessie也可以infer some simple invariants automatically。
关于loops - 确定循环不变性的最佳方法是什么？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2935295/