问题描述
在使用形式化方面来创建一些代码时，是否存在确定循环不变性的通用方法，或者根据问题而定，它会完全不同吗?
When using formal aspects to create some code is there a generic method of determining a loop invariant or will it be completely different depending on the problem?
推荐答案
已经指出，一个相同的循环可以具有多个不变量，并且可计算性不利于您.这并不意味着您无法尝试.
It has already been pointed out that one same loop can have several invariants, and that Calculability is against you. It doesn't mean that you cannot try.
实际上，您正在寻找归纳不变性:不变性一词也可以用于每次迭代都为真的属性，但是仅仅知道它是否成立在一次迭代中推断出它在下一次保持不变.如果 I 是归纳不变式，则 I 的任何结果都是不变式，但可能不是归纳不变式.
You are, in fact, looking for an inductive invariant: the word invariant may also be used for a property that is true at each iteration but for which is it not enough to know that it hold at one iteration to deduce that it holds at the next. If I is an inductive invariant, then any consequence of I is an invariant, but may not be an inductive invariant.
您可能正在尝试获取一个归纳不变式，以证明在某些定义的情况(前提条件)下循环的某个属性(前提条件).
You are probably trying to get an inductive invariant to prove a certain property (post-condition) of the loop in some defined circumstances (pre-conditions).
有两种启发式方法可以很好地发挥作用:
There are two heuristics that work quite well:
-
从拥有的东西开始(前提条件)，然后减弱直到具有归纳不变式.为了直观了解如何削弱，请应用一次或多次前向循环迭代，然后看看在您拥有的公式中哪些不再是正确的.
start with what you have (pre-conditions), and weaken until you have an inductive invariant. In order to get an intuition how to weaken, apply one or several forward loop iterations and see what ceases to be true in the formula you have.
从所需的内容(后置条件)开始，并进行增强，直到您具有归纳不变式为止.要获得如何加强直觉的方法，请向后应用一个或多个循环迭代，并查看需要添加哪些内容，以便可以推导出后置条件.
start with what you want (post-conditions) and strengthen until you have an inductive invariant. To get the intuition how to strengthen, apply one or several loop iterations backwards and see what needs to be added so that the post-condition can be deduced.
如果您希望计算机在实践中为您提供帮助，我可以推荐 Jessie 演绎法用于 Frama-C 的C程序的验证插件.还有其他一些，尤其是对于Java和JML注释，但是我对它们并不熟悉.尝试您想到的不变式要快于在纸上进行计算.我应该指出，也无法确定属性是否为归纳不变式，但现代自动证明在许多简单示例中都非常有用.如果您决定走这条路，请从列表中获取尽可能多的内容:Alt-ergo，Simplify，Z3.
If you want the computer to help you in your practice, I can recommend the Jessie deductive verification plug-in for C programs of Frama-C. There are others, especially for Java and JML annotations, but I am less familiar with them. Trying out the invariants you think of is much faster than working out if they work on paper. I should point out that verifying that a property is an inductive invariant is also undecidable, but modern automatic provers do great on many simple examples. If you decide to go that route, get as many as you can from the list: Alt-ergo, Simplify, Z3.
借助可选的(且安装起来有点困难)的围裙库，Jessie还可以推断一些简单的不变式自动.
With the optional (and slightly difficult to install) library Apron, Jessie can also infer some simple invariants automatically.
这篇关于确定循环不变性的最佳方法是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！