标签: proof-of-correctness

为了找到树的直径,我可以从树中获取任何节点,执行BFS以找到距离它最远的节点,然后在该节点上执行BFS.与第二个BFS的最大距离将产生直径.

不过我不知道如何证明这一点？我尝试过对节点数量的归纳,但是有太多的情况.

任何想法将不胜感激......

我理解像Coq和Idris这样的语言如何用于证明用这些语言编写的程序的属性(根据我在该主题中的一点经验来判断.)但是我想知道是否有一种平易近人的方式在外部做同样的事情,在现有的代码库.

有没有办法使用像Coq或其他专业工具这样的工具来证明用C++编写的算法的正确性？如果是这样,这样做有什么要求？

让我说我有

data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}

和该类型的谓词,

data WineStock : Fruit -> Type where
    CanonicalWine : WineStock Grape
    CiderIsWineToo : WineStock Apple

这并不适用于Banana,Orange,Lemon和其他人.

它可以说,这定义WineStock为上一个谓语Fruit; WineStock Grape是真的(因为我们可以构造该类型的值/证明:) CanonicalWine以及WineStock Apple但是WineStock Banana是假的,因为该类型不是任何值/证明所居住的.

那么,我该怎么去使用有效Not (WineStock Banana),Not (WineStock Lemon)等等？似乎对于每个Fruit构造函数除了Grape和Apple,我不得不编写一个案例分裂WineStock,某处,充满 …

嗨,大家好我想比较2个算法,并认为我可以尝试为他们写一个证明!(我的数学很糟糕因此问题)

通常在去年的数学课上我们会遇到类似的问题

证明:(2r + 3)= n(n + 4)

那么我会做所需的4个阶段并在最后得到答案

我被困的地方是证明prims和Kruskals - 我怎样才能将这些算法变成上面的数学形式所以我可以继续证明

注意:我不是要求别人为我回答 - 只是帮我把它放到一个我可以自己去的地方

谢谢

获取以下C++ 14代码段:

unsigned int f(unsigned int a, unsigned int b){
    if(a>b)return a;
    return b;
}

声明: 该函数f返回其参数的最大值.

现在,该陈述"显然"是正确的,但我未能严格证明ISO/IEC 14882:2014(E)规范.

第一:我不能以正式的方式陈述财产.

形式化版本可以是:对于每个语句s,当抽象机器(在规范中定义)处于状态P并且s看起来像"f(expr_a,expr_b)"并且s中的 'f' 被解析为有问题的函数,s(P).return = max(expr_a(P).return,expr_b(P).return).

这里对于状态P和表达式s,s(P)是在评估s之后的机器的状态.

问题:该陈述的正确形式化版本是什么？如何使用上述规范强加的属性来证明声明？对于每个演绎步骤,请参考允许所述步骤的标准中的适用片段(片段的数量足够).

编辑:也许在Coq中正式化

我的目标是证明霍纳法则是正确的。为此，我将 Horner 当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码：

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
      end loop;
      pragma Assert (Y = Z); …

大多数证明助手都是具有依赖类型的函数式编程语言.他们可以证明程序/算法.相反,我感兴趣的是最适合数学的证明助手,而且只有(例如微积分).你能推荐一个吗？我听说过Mizar,但我不喜欢源代码已关闭,但如果最好是数学,我会使用它.Agda和Idris等新语言如何适用于数学证明？

我在想我们可以证明一个程序有错误.我们可以对其进行测试,以评估它是否或多或少具有抗虫性.

但有没有办法(甚至在理论上)证明程序没有错误？

对于简单的程序,例如"Hello World",我想我们应该能够做到.但是大型项目呢？

这是算法:

// Precondition: n > 0

l = -1;
r = n;

while (l+1 != r) {
    m = (l+r)/2;

    // I && m == (l+r)/2

    if (a[m] <= x) {
        l = m;
    } else {
        r = m;
    }
}
// Postcondition: -1 <= l < n

我做了一些研究,并将不变量缩小到了if x is in a[0 .. n-1] then a[l] <= x < a[r].

我不知道如何从那里进步.前提似乎过于宽泛,所以我很难显示出来P -> I.

非常感谢任何帮助.这些是可用于证明算法正确性的逻辑规则:

优化编译器的最终目的是在程序空间中搜索与原始程序等效但速度更快的程序。这已在实践中针对非常小的基本块完成：https : //en.wikipedia.org/wiki/Superoptimization

听起来困难的部分是搜索空间的指数性质，但实际上并非如此；困难的部分是，假设你找到了你正在寻找的东西，你如何证明新的、更快的程序真的等同于原始程序？

上次我研究它时，在证明某些上下文中程序的某些属性方面取得了一些进展，特别是在讨论标量变量或小的固定位向量时在很小的范围内，但在证明程序的等效性方面并没有真正取得进展当您谈论复杂的数据结构时，规模更大。

有没有人想出一种方法来做到这一点，甚至“模解决这个我们还不知道如何解决的 NP 难搜索问题”？

编辑：是的，我们都知道停机问题。它是根据一般情况定义的。人类是一个存在证明，这可以用于许多感兴趣的实际案例。