我当时想回大学的一年级(五年前)，当时我参加了一次初级计算机科学专业的考试。有一个关于循环不变式的问题，我想知道在这种情况下是否真的需要循环不变式，或者这个问题仅仅是一个不好的例子……问题是为阶乘函数编写一个迭代定义，然后证明该功能是正确的。
我为阶乘函数提供的代码如下:
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)中有大约一半是非常理论化和证明繁重的类(class)，而大约一半是非常关于实现和编码的繁琐类(class)，没有任何正式的或理论的 Material 。这些在实践中有多少重叠？如果您确实在行业中使用过证明，那么什么时候应用它们(总是，只有在它很复杂，很少，永远不会使用时)？
编辑
如果我们自己确信某段代码是正确的，是否可以(非正式地)使其他人相信该代码是正确的，并且已经进行了单元测试，则在多大程度上需要形式上正确的证明？
最佳答案
当然，这取决于条件，但是我认为对于程序员来说，重要的是要知道如何编写不易出错的代码，而该代码在构造上往往是正确的。
一个示例是“预读”的概念，例如在解析中，其中输入的下一个标记不是“读取”，然后是“查看”，如果不是想要的，则可能是“放回”，而是“看了看”，如果想要的话，则可能“接受了”。例如，当编写循环遍历数据库记录和提取小计的循环时，这种简单的视角变化可能会导致更简单，更可靠的代码。
另一个示例是differential execution，这是我很多年前偶然发现的一项技术。它似乎允许增量算法重新执行，从而增量更新其结果。我在内容可以动态更改的用户界面中广泛使用了它。很长一段时间，我觉得它在所有情况下都有效，但是直到我最终证明它为as at the bottom of my Wikipedia page时，才能确定。之后，我知道如果坚持一些简单的约束，无论有多少代码依赖它，我都可以依靠它来工作。
同时，我们可能对某种算法的正确性有最大的信心，但是由于我们的证明技术很差，因此很难正式证明。考虑低气泡排序。它显然可以工作，但是请尝试通过对源代码应用规则来正式证明它。我已经做到了，但这并不容易。我没有尝试过更高级的排序算法。
关于language-agnostic - 对 “loop invariants”的看法，这些在业界是否经常使用？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2590518/