代码之家 › 专栏 › 技术社区 › Michael Aaron Safyan

对“循环不变量”的看法,这些是工业上常用的吗?

language-agnostic

Michael Aaron Safyan · 技术社区 · 14 年前

当我参加一个计算机科学入门考试的时候,我想起了我在大学一年级(五年前)的时候。有一个关于循环不变量的问题,我想知道在这种情况下循环不变量是否真的是必要的,或者这个问题只是一个糟糕的例子…问题是为阶乘函数编写一个迭代定义,然后证明该函数是正确的。

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

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的整数的乘积…而else子句中的for循环只是这个定义的直译。在这种情况下,真的需要循环不变量作为正确性的证明吗?在循环不变量(以及适当的初始化和终止条件)成为证明正确性所必需的条件之前,循环必须有多复杂?

另外,我想知道…这种正式的证据在这个行业里多久使用一次?我发现我的课程中有一半是理论性和证明性很强的课程,一半是实现性和编码性很强的课程,没有任何形式或理论性的材料。在实践中这些重叠有多少?如果你在这个行业使用校样,你什么时候使用它们(总是,只有在它很复杂,很少,从来没有)?

编辑
如果我们自己确信一段代码是正确的,就可以(非正式地)让其他人相信它是正确的,并且已经有了单元测试,那么在多大程度上需要正确性的正式证明呢?

4 回复 | 直到 12 年前

Community CDub 7 年前

在多大程度上需要正确性?

当然,这要看情况,但我认为程序员必须知道如何编写不易出错的代码,以及在哪些地方可以通过构造进行更正。

一个例子是“向前看”的概念,例如在解析中,下一个输入标记不是“读”,然后是“看”,如果是的话可能是“放回去” 不什么是需要的,但更确切地说是“看”然后可能“接受” 是想要什么。例如,当编写循环遍历数据库记录和提取小计的循环时,透视图中的这种简单更改可以导致更简单、更可靠的代码。

另一个例子是 differential execution ,这是我多年前偶然发现的一种技术。它似乎允许以增量方式重新执行任何算法,以便以增量方式更新其结果。我在用户界面中广泛使用它,其中的内容可以动态更改。很长一段时间以来,我觉得它在所有情况下都有效,但不确定,直到我最终证明了它, as at the bottom of my Wikipedia page . 在那之后,我知道如果我坚持一些简单的约束,我可以依赖它来工作,不管代码有多依赖它。

同时,我们可能对某些算法的正确性有最大的信心,但由于我们的证明技术很差,发现很难进行形式化证明。想想那些低级的泡沫。很明显,它是有效的,但是试着通过对源代码应用规则来正式地证明它。我做过,但它是不容易的。我没有尝试过更先进的排序算法。

Ken 14 年前

教授要我用循环不变量证明循环;

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

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

好吧,从技术上讲,不是。根据这个推理,你也不需要写一个阶乘函数:只要使用一个库函数!但这不是练习的重点。

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

我认识一些聪明人 任何东西 如果没有不变量,那么就有人需要使用它们,即使是像上面这样的小情况。这就像问“在你需要手推车来移动石头之前,它必须有多重?”.

另外,我想知道…这种正式的证据在这个行业里多久使用一次?

写得很清楚?可能很少,除非你在 certain industries . 但我在写除了最简单的循环之外的任何循环时都会考虑它们。

这有点像我不画句子图,但这并不意味着我从不考虑语法,尤其是当我写一些非常重要的文本时。我可以告诉你我的代词的先行词是什么,尽管我从不费心把这个事实写在纸上。

dthorpe 14 年前

当你在解决棘手的问题和编写代码,这些代码将在你继续工作很长一段时间后被重用时,你(应该)每天都要经历证明你所编写的每一个例程正确性的过程。测试驱动开发是这个想法的一种形式化,但它的核心是:你至少需要向自己证明,最好向他人证明(代码审查!)您编写的代码将以适当的方式处理所有可能的输入和路径。

我们是否在代码不变量上争论不休?不,在你登记入住之前,我们会评分吗?某种程度上。如果团队对您的代码或“证明”不满意,您可以返回到您的框中进行修复,直到它通过审查。

Daniel Earwicker 14 年前

近年来,以各种名称命名的“测试驱动开发”是大多数人最费心去推理的代码。与逻辑推理相比,这更像是非常谨慎和可重复的实验。科学与数学!

在像埃菲尔这样的语言中,有一些使用了前置条件、后置条件和循环/类不变量,而.net 4.0中即将推出的“契约”支持可能有助于进一步普及这些思想。

就我个人而言,这些天我很少使用断言;当我在一个结构中循环时,我通常不再将其作为循环来编写。我把它写成一个查询,比如用c语言编写linq,或者用js等其他语言编写类似的东西。因此,没有必要进行状态操作来出错(通常没有)。任何关于结果的断言都是多余的,因为它只需重申查询中的条件:在查询方法中,您可以描述所需的结果。

这并不是说我从不使用断言;但我倾向于将它们与单元测试结合使用,并且只用于执行集合的一些复杂的“就地”变异的非常复杂的算法;在这种情况下,没有“内置”的方法来要求得到我想要的结果;我必须编写该算法是必需的(可能是因为复制整个数据结构会非常昂贵),所以我用断言来覆盖它,以便帮助我的单元测试标记出内部问题。