【问题标题】:What is an invariant?什么是不变量?
【发布时间】:2010-09-11 20:12:14
【问题描述】:

这个词似乎在很多情况下都被使用了。我能想到的最好的是它们意味着一个无法改变的变量。这不就是常量/finals(该死的 Java!)的用途吗?

【问题讨论】:

标签: language-agnostic invariants


【解决方案1】:

这是一个您知道在逻辑中的特定位置始终为真的条件,并且可以在调试时检查以找出问题所在。

【讨论】:

  • 除非它并不总是正确的,研究论文证明了这一点。也许在某些点之前和之后总是正确的。但这是一个误会
【解决方案2】:

我通常更多地从算法或结构的角度来看待它们。

例如,您可以有一个可以断言的循环不变量——在每次迭代的开始或结束时始终为真。也就是说,如果您的循环应该处理从一个堆栈到另一个堆栈的对象集合,您可以说 |stack1|+|stack2|=c,位于循环的顶部或底部。

如果不变量检查失败,则表明出现问题。在此示例中,这可能意味着您忘记将处理后的元素推送到最终堆栈等。

【讨论】:

    【解决方案3】:

    维基百科的魔力:Invariant (computer science)

    在计算机科学中,一个谓词, 如果为真,将在整个 具体的操作顺序是 称为(一个)不变的 顺序。

    【讨论】:

    • 链接?技术术语?读? WTF? ;) 说真的,很好的链接,但有一点总结会很好。
    【解决方案4】:

    不变量比变量更“概念化”。通常,它是程序状态的属性,始终为真。确保不变量成立的函数或方法被称为保持不变量。

    例如,二叉搜索树可能具有这样的不变量,即对于每个节点,该节点的左孩子的键小于该节点自己的键。正确编写此树的插入函数将保持该不变量。

    如您所知,这不是您可以存储在变量中的那种东西:它更像是一个关于程序的声明。通过弄清楚你的程序应该维护什么样的不变量,然后检查你的代码以确保它确实维护了这些不变量,你可以避免代码中的逻辑错误。

    【讨论】:

    • 这个很好的例子如果在维基百科链接中包含cero的答案会更好。
    • 父母的年龄大于其亲生子女的年龄。周围的上下文会改变,但不变量永远不会改变。例如,可能是史密斯一家有 2 个孩子。或者它可能存在于任何哺乳动物的其他物种中。上下文会改变,但不变量不会改变。
    • “...程序状态的属性始终为真...” - @jacob baskin - 写得很好,谢谢。
    • “...程序状态的属性,它始终为真...” - 我同意它写得很好,但它可能会产生误导。首先我把它理解为布尔值,但我很确定它的意思是“......总是不变的”(但也许只是因为英语不是我的第一语言)
    • 值得一提的是,我认为,不变量可以帮助您编写inductive proof,表明您的函数或程序是正确的。可能还有其他用途,但仅此一项就非常有用。
    【解决方案5】:

    从本质上讲,不变量在编写干净的代码时非常有用,因为从概念上了解代码中应该存在哪些不变量可以让您轻松决定如何组织代码以达到那些目标。如前所述,它们在调试中也很有用,因为检查不变量是否得到维护通常是一种很好的方法,可以查看您尝试执行的任何操作是否确实在执行您想要的操作。

    【讨论】:

      【解决方案6】:

      在代码块中不会改变的东西

      【讨论】:

        【解决方案7】:

        ADT 不变量指定关系 在数据字段中(实例变量) 之前和之后必须始终正确 任何实例方法的执行。

        【讨论】:

          【解决方案8】:

          正如这一行所说:

          在计算机科学中,如果一个谓词为真,则在整个特定的操作序列中将保持为真,被称为对该序列不变量。

          为了更好地理解这一点,希望这个 C++ 示例有所帮助。

          考虑一个场景,您必须获取一些值并在名为 count 的变量中获取它们的总数,然后将它们添加到名为 sum 的变量中

          不变量(再次更像是一个概念):

          // invariant:
          // we have read count grades so far, and
          // sum is the sum of the first count grades
          

          上面的代码是这样的,

          int count=0;
          double sum=0,x=0;
          while (cin >> x) {
          ++count;
          sum+=x;
          }
          

          上面的代码做了什么?

          1) 从cin 读取输入并将它们放入x

          2) 一次成功读取后,递增countsum = sum + x

          3) 重复 1-2 直到读取停止(即 ctrl+D)

          循环不变量:

          不变量必须为真总是。所以最初你只用这个开始你的代码

          while(cin>>x){
            }
          

          此循环从标准输入读取数据并存储在 x 中。好和好。但是 invariant 变为 false,因为我们的 invariant 的第一部分没有被遵循(或保持为真)。

          // we have read count grades so far, and
          

          如何保持不变量为真?

          简单!增加计数。

          所以++count; 会做得很好!。现在我们的代码变成了这样,

          while(cin>>x){
           ++count; 
           }
          

          但是

          即使现在我们的 invariant(一个必须为 TRUE 的概念)也是 False,因为现在我们没有满足 我们的不变量的第二部分。

          // sum is the sum of the first count grades
          

          那么现在该怎么办?

          x 添加到sum 并将其存储在sum (sum+=x) 和下一次 cin>>x 会将新值读入 x。

          现在我们的代码变成了这样,

          while(cin>>x){
           ++count; 
           sum+=x;
           }
          

          让我们检查一下

          代码是否匹配我们的不变量

          // invariant:
          // we have read count grades so far, and
          // sum is the sum of the first count grades
          

          代码:

          while(cin>>x){
           ++count; 
           sum+=x;
           }
          

          啊!现在循环不变量是 True always 并且代码工作正常。

          以上示例取自 Andrew-koening 和 Barbara-E 的Accelerated C++一书

          【讨论】:

            【解决方案9】:

            它通常是在某些数学运算下不会改变的量。 示例是一个标量,在旋转时不会改变。例如,在磁共振成像中,通过旋转不变量来表征组织特性是有用的,因为它的估计理想情况下不依赖于扫描仪中身体的方向。

            【讨论】:

              【解决方案10】:

              Java Concurrency in Practice 一书中有一个关于不变量及其重要性的绝佳示例。

              尽管以 Java 为中心,但该示例描述了一些负责计算所提供整数的因数的代码。示例代码尝试缓存提供的最后一个数字,以及为提高性能而计算的因素。在这种情况下,示例代码中没有考虑到一个不变量,这使得代码在并发场景中容易受到竞争条件的影响。

              【讨论】:

                【解决方案11】:

                这里的所有答案都很棒,但我觉得我可以更清楚地说明这个问题:

                从语言的角度来看,不变意味着永远不会改变的东西。虽然这个概念实际上来自数学,但它是与归纳法相结合的流行证明技术之一。

                这是一个证明的过程,如果你能找到一个处于初始状态的不变量,并且无论对该状态应用任何 [合法] 转换,该不变量仍然存在,那么你可以证明如果某个状态确实如果没有这个不变量,那么它就永远不会发生,无论对初始状态应用什么变换序列。

                现在,以前的思维方式(再次与归纳结合)使得预测计算机软件的逻辑成为可能。当执行在循环中时尤其重要,其中不变量可用于证明某个循环会产生某个结果,或者它永远不会以某种方式改变程序的状态。

                当不变量用于谓词循环逻辑时,它称为loop invariant。它可以在循环之外使用,但对于循环来说它真的很重要,因为你经常有很多可能性,或者无限多的可能性。

                请注意,我使用“谓词”一词是计算机软件的逻辑,而不是证明。这是因为虽然在数学中invariant 可以用作证明,但它永远无法证明计算机软件在执行时会产生预期的结果,因为该软件是在许多抽象之上执行的,这永远不可能证明它们会产生预期的结果(例如考虑硬件抽象)。

                最后,虽然理论上和严格地预测软件逻辑仅对医疗和军事等高度关键的应用程序很重要。在调试时,不变量仍可用于帮助典型的程序员。它可以用来知道某个位置的位置 程序失败是因为它未能维护某个不变量 - 我们中的许多人无论如何都在使用它而不考虑它。

                【讨论】:

                  【解决方案12】:

                  这个答案是给我 5 岁的孩子的。不要将不变量视为常数或固定数值。但它可以。然而,它不止于此。

                  相反,不变量类似于不同实体之间的固定关系。例如,与亲生父母相比,您的年龄将永远小于您的年龄。你的年龄和你父母的年龄都会随着时间的推移而变化,但我上面提到的关系是不变的。

                  不变量也可以是数值常数。例如,pi 的值是圆的周长与其直径之间的不变比率。不管圆圈有多大或多小,这个比例永远是pi

                  【讨论】:

                    【解决方案13】:

                    Class Invariant 是在调用相关函数之前和之后应该始终为真的条件

                    例如,平衡树有一个Invariant,称为isBalanced。当您通过某些方法(例如 addNode、removeNode...)修改树时 - isBalanced 在修改树之前和之后应该始终为 true

                    【讨论】:

                      猜你喜欢
                      • 2011-03-14
                      • 1970-01-01
                      • 1970-01-01
                      • 2015-01-06
                      • 1970-01-01
                      • 1970-01-01
                      • 1970-01-01
                      • 2012-02-12
                      • 1970-01-01
                      相关资源
                      最近更新 更多