language-agnostic - 关于 "loop invariants"的意见，这些在行业中是否经常使用？

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 循环只是这个定义的字面翻译。在这种情况下，真的需要循环不变量作为正确性证明吗？在循环不变量(以及适当的初始化和终止条件)成为正确性证明所必需的循环之前，循环必须有多复杂？

此外，我想知道......行业中使用这种正式证明的频率如何？我发现我的类(class)中大约有一半是非常理论和大量证明的，大约一半是非常注重实现和编码的，没有任何正式或理论 Material 。这些在实践中重叠多少？如果你确实在行业中使用了证明，你什么时候应用它们(总是，只有在它很复杂的时候，很少，从不)？

编辑
如果我们自己确信一段代码是正确的，可以(非正式地)说服其他人它是正确的，并且有适当的单元测试，那么在多大程度上需要正确性的正式证明？

Answer 1

The professor wanted me to prove the loop using a loop invariant;

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

Is a loop invariant really needed as a proof of correctness in this case?

好吧，从技术上讲，没有。根据这个推理，您也不需要编写阶乘函数:只需使用库函数即可!但这不是练习的重点。

How complicated must a loop be before a loop invariant (and proper initialization and termination conditions) become necessary for a proof of correctness?

我认识一些聪明的人，他们可能可以在没有不变量的情况下证明任何事情，然后有些人甚至需要在像上面这样的微不足道的情况下使用它们。这就像问“在你需要手推车来移动它之前，一块石头必须有多重？”。

Additionally, I was wondering... how often are such formal proofs used in the industry?

明确写出来？可能很少，除非你在 certain industries .但是在编写除最简单的循环之外的任何循环时，我仍然会考虑它们。

这有点像我不绘制句子的方式，但这并不意味着我从不考虑语法，特别是如果我正在写一些非常重要的文本。我可以告诉你我的代词的先行词是什么，即使我从不费心把这个事实写在纸上。