关于"循环不变量"的观点,这些在行业中经常使用吗？

Question

我正在回想起我在大学一年级的那一年(五年前),当时我参加了一个考试,从而完成了计算机科学的入门课程.有一个关于循环不变的问题,我想知道如果循环不变是真的有必要在这种情况下,或者如果问题只是一个坏榜样......问题是写一个迭代定义为一个阶乘函数,然后证明功能是正确的.

我为阶乘函数提供的代码如下:

public static int factorial(int x)
{
     if ( x < 0 ){
         throw new IllegalArgumentException("Parameter must be >= 0");
     }else if ( x == 0 ){
         return 1;
     }else{
         int result = 1;
         for ( int i = 1; i <= x; i++ ){
             result*=i;
         }
         return result;
     }
}

我自己的正确性证明是一个案例的证明,并且每一个我断言它的定义是正确的(x!对于负值是未定义的,0!是1,x!是1*2*3 ......*x对于x)的正值.教授希望我用循环不变量来证明循环; 但是,我的论点是"按定义"是正确的,因为"x!"的定义 对于正整数x是"1 ... x的整数的乘积",而else子句中的for循环只是该定义的字面翻译.在这种情况下,真正需要一个循环不变量作为正确性的证明吗？在循环不变量(以及正确的初始化和终止条件)成为正确性证明之前,循环必须有多复杂？

另外,我想知道......行业中使用这种正式证据的频率是多少？我发现我的课程大约有一半是非常理论性和证据性的,大约一半是非常实施和编码,没有任何正式或理论材料.这些在实践中重叠多少？如果您确实使用了行业中的样张,那么何时应用它们(总是,只有它很复杂,很少,从不)？

编辑
如果我们自己,相信这一块的代码是正确的,可以说服别人(非正式)它是正确的,并有到位的单元测试,以被正确性的形式证明需要什么样的程度？

Answer 1

教授希望我用循环不变量来证明循环;

你的教授想确保你理解循环不变量,而不只是证明一个非常简单的函数.

在这种情况下,真正需要一个循环不变量作为正确性的证明吗？

嗯,从技术上讲,没有.通过这种推理,您不需要编写阶乘函数:只需使用库函数!但这不是演习的重点.

在循环不变量(以及正确的初始化和终止条件)成为正确性证明之前,循环必须有多复杂？

我认识一些聪明的人,他们可以证明几乎没有不变量的东西,然后有人需要使用它们,即使是像上面那样的琐碎案例.这就像问"在需要独轮车移动之前,岩石有多重？".

另外,我想知道......行业中使用这种正式证据的频率是多少？

明确写出来了吗？可能很少,除非你在某些行业.但是在编写除最简单循环之外的任何东西时我仍然会考虑它们.

这有点像我不用图表句子,但这并不意味着我从不考虑语法,特别是如果我正在写一些非常重要的文本.我可以告诉你我的代词的前因是什么,即使我从来都不想把这个事实写在纸上.

Answer 2

在何种程度上需要正式的正确性证明？

当然，这取决于情况，但我认为对于程序员来说重要的是知道如何编写不易出错的代码，并且通过构造往往是正确的。

一个例子是“向前看”的概念，例如在解析中，输入的下一个标记不是“读取”，然后是“查看”，如果不是想要的，则可能“放回”，而是“查看”然后可能“接受”（如果这是想要的）。例如，当编写循环来循环数据库记录并提取小计时，这种简单的视角改变可以产生更简单、更可靠的代码。

另一个例子是差异执行，这是我多年前偶然发现的一种技术。它似乎允许任何算法被增量地重新执行，从而增量地更新其结果。我在内容可以动态更改的用户界面中广泛使用它。很长一段时间，我觉得它在所有情况下都有效，但无法确定，直到我最终证明了这一点，正如我的维基百科页面底部所示。之后，我知道，如果我坚持一些简单的约束，我就可以依靠它来工作，无论有多少代码依赖于它。

同时，我们可能对某些算法的正确性抱有极大的信心，但却发现很难形式化地证明，因为我们的证明技术很差。考虑一下低级的冒泡排序。它显然有效，但尝试通过将规则应用于源代码来正式证明它。我已经做到了，但这并不容易。我还没有尝试过更高级的排序算法。