确定循环不变式的最佳方法是什么？
当使用形式方面创建一些代码时，是否有确定循环不变式的通用方法，或者根据问题的不同，它会完全不同吗？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（5）
已经有人指出，同一个循环可以有多个不变量，而可计算性对你不利。这并不意味着你不能尝试。
事实上，您正在寻找一个归纳不变量：“不变量”这个词也可以用于表示在每次迭代中都为真的属性，但仅仅知道它在一次迭代中保持不变还不够。推断它在下一个成立。如果I是归纳不变量，则I的任何结果都是不变量，但可能不是归纳不变量。
您可能试图获得归纳不变量来证明循环在某些定义的情况（前提条件）下的特定属性（后置条件）。
有两种启发式方法效果很好：
从你所拥有的（前提条件）开始，然后减弱，直到你得到归纳不变量。为了直观地了解如何弱化，请应用一次或多次前向循环迭代，并查看您所拥有的公式中哪些不再为真。
从你想要的（后置条件）开始并加强，直到你有了归纳不变量。要直观地了解如何强化，请向后应用一个或多个循环迭代，并查看需要添加哪些内容，以便推导出后置条件。
如果你想让电脑帮助你练习，我可以推荐Jessie演绎验证插件-用于 Frama-C 的 C 程序。还有其他的，特别是 Java 和 JML 注释，但我对它们不太熟悉。尝试你想到的不变量比在纸上计算它们要快得多。我应该指出，验证一个属性是否是归纳不变量也是不可判定的，但现代自动证明器在许多简单的例子上做得很好。如果您决定走这条路，请从列表中尽可能多地选择：Alt-ergo、Simplify、Z3。
通过可选的（安装稍微困难的）库 Apron，Jessie 还可以自动推断一些简单的不变量。
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.
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.
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.
With the optional (and slightly difficult to install) library Apron, Jessie can also infer some simple invariants automatically.
生成循环不变量实际上很简单。例如，
true就是一个很好的例子。它满足您想要的所有三个属性：但您所追求的可能是最强循环不变量。然而，找到最强的循环不变量有时甚至是一个不可判定的任务。请参阅文章可计算循环不变量的不足。
It's actually trivial to generate loop invariants.
trueis a good one for instance. It fulfills all three properties you want:But what you're after is probably the strongest loop invariant. Finding the strongest loop invariant however, is sometimes even an undecidable task. See article Inadequacy of Computable Loop Invariants.
我认为实现自动化并不容易。来自维基：
I don't think it's easy to automate this. From wiki:
有许多用于查找循环不变量的启发式方法。关于这一点的一本好书是 Ed Cohen 的《Programming in the 90s》。这是关于如何通过手动操作后置条件来找到一个好的不变量。例如：用变量替换常量、加强不变量、...
There are a number of heuristics for finding loop invariants. One good book about this is "Programming in the 1990s" by Ed Cohen. It's about how to find a good invariant by manipulating the postcondition by hand. Examples are: replace a constant by a variable, strengthen invariant, ...
我在博客中写过有关编写循环不变量的文章，请参阅 验证循环第 2 部分。证明循环正确所需的不变量通常包括两部分：
(2) 简单明了。要导出 (1)，请从表达终止后所需状态的谓词开始。它很可能包含某个数据范围内的“forall”或“exists”。现在更改“forall”或“exists”的边界，以便（a）它们依赖于循环修改的变量（例如循环计数器），以及（b）以便首次进入循环时不变式为真（通常通过将“forall”或“exists”的范围设为空）。
I've written about writing loop invariants in my blog, see Verifying Loops Part 2. The invariants needed to prove a loop correct typically comprise 2 parts:
(2) is straightforward. To derive (1), start with a predicate expressing the desired state after termination. Chances are it contains a 'forall' or 'exists' over some range of data. Now change the bounds of the 'forall' or 'exists' so that (a) they depend on variables modified by the loop (e.g. loop counters), and (b) so that the invariant is trivially true when the loop is first entered (usually by making the range of the 'forall' or 'exists' empty).