0

下面是证明各种简单定理的第一次尝试，在这种情况下是关于奇偶性的。达芙妮 /v. 1.9.9.40414/ 验证将 2 添加到偶数会产生偶数，但不接受任何已注释掉的条件。

function IsEven(a : int) : bool
requires a >= 0
{
    if a == 0 then      true 
    else if a == 1 then false 
    else                IsEven(a - 2)
}

method Check1(a : int)
requires a >= 0
ensures IsEven(a) ==> IsEven(a + 2)
//ensures IsEven(a) ==> IsEven(a + a)
//ensures IsEven(a) ==> IsEven(a * a)
{
}

由于我刚刚开始研究这个很棒的工具，我的方法或实现可能不正确。任何意见，将不胜感激。

4

1 回答 1

1

这里发生了一些不同的事情。我将依次讨论这三个后置条件。

第一个和第二个后置条件

因为IsEven是一个递归定义的谓词，一般来说，关于它的事实需要归纳证明。您的第一个后置条件很简单，不需要归纳，这就是它通过的原因。

您的第二个后置条件确实需要证明归纳。Dafny 具有自动执行归纳的启发式方法，但这些启发式方法仅在某些上下文中调用。特别是，Dafny 只会尝试对“幽灵方法”（也称为“引理”）进行归纳。

如果您在 in 前面添加关键字（ghost或更改为等效的 ），您将看到第二个后置条件通过。这是因为 Dafny 的归纳启发式被调用并设法完成了证明。methodCheck1methodlemma

第三个后置条件

第三个后置条件更复杂，因为它涉及非线性算术。（换句话说，它涉及将两个变量相乘的非平凡推理。）Dafny 的底层求解器难以推理这些事情，因此通过归纳的启发式证明没有通过。

a * a即使a是偶数的证明

证明它的一种方法是在这里。我已经考虑IsEven(a) ==> IsEven(a * a)到它自己的引理，称为EvenSquare. 我也将其更改为 requireIsEven(a)作为前置条件，而不是在后置条件中添加含义。（类似的证明也适用于蕴涵，但是像这样在引理上使用先决条件而不是蕴涵是惯用的 Dafny。）

的证明EvenSquare是通过（手动）归纳对a。基本情况会自动处理。在归纳情况（if语句的主体）中，我调用归纳假设（即，我进行递归方法调用EvenSquare以建立(a - 2) * (a - 2)偶数）。然后我断言a * a可以写为总和(a - 2) * (a - 2)和一些偏移量。断言是自动分派的。如果我能证明这个等式的右边是偶数，证明就会完成。

为此，我已经知道它(a - 2) * (a - 2)是偶数，所以我首先调用另一个引理来表明偏移量是偶数，因为它是其他值的两倍。最后，我引用最后一个引理来证明两个偶数之和是偶数。

假设有两个引理，这就完成了证明。

两个引理的证明

它仍然证明任何事物的两倍是偶数，并且两个偶数的和是偶数。虽然并非完全微不足道，但也没有EvenSquare.

引理EvenDouble证明任何事物都是偶数的两倍。（这实际上是您的第二个后置条件的更强大的版本。您的第二个后置条件说将任何偶数加倍是偶数。事实上，将任何（非负，根据您的偶数定义）数加倍都是偶数。）证明EvenDouble通过（手动）感应获得的收益a。基本情况会自动处理。归纳案例只需要明确地调用归纳假设。

EvenPlusDafny 的归纳启发式几乎自动证明了这个引理，除了它遇到了一个错误或其他导致求解器循环的问题。经过一点调试，我确定注释{:induction x}（或者{:induction y}，就此而言）使证明不循环。这些注释告诉 Dafny 的启发式方法要尝试对哪些变量进行归纳。默认情况下，在这种情况下，Dafny 会尝试对和 x进行感应y，由于某种原因，这会导致求解器循环。但是单独对任一变量进行归纳都是有效的。我正在进一步调查这个问题，但目前的解决方案有效。

于 2017-07-29T02:03:23.810 回答