loops - Dafny：快速指数计算（循环）

问题描述

我正在尝试在 Dafny 中实现和编译快速指数算法，但遇到了几个问题。

语境：

所有代码都在下面可用；
快速指数 ( FastExp) 引理本身是迭代的；
一个exp函数用于确保计算正确（这个函数递归执行传统的指数）；
我不会讨论数学是如何完成的，或者它是否有效。这不是问题，数学是正确的。

现在，我遇到的主要问题是：

我不知道在循环的减少和不变量中放什么；
FastExp引理的后置条件“可能不成立” ；

如果有人可以帮助我解决这个简单的（我假设）问题，我会很高兴。

先感谢您。

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

function exp(x: int, n: int): int
    requires n > 0;
{
    if n == 1 then
        x
     else 
        x * exp(x, n-1)
}

lemma FastExp(x: int, n: int) returns (r: int)
requires n >= 0
ensures r == exp(x,n)
{
    var expo:int := n;
    var c:int := x;
    var tempR:int := 1;

    while expo > 0
        invariant 0 <= expo
        decreases expo
    {
        if isEven(expo) {
            tempR := tempR * c;
        }
        c := c * c;
        expo := expo / 2;
    }
    r := tempR;
}

标签： loopsdafnyinvariantsloop-invariant

解决方案

一个decreases子句用于解释终止。为了证明循环终止，您需要找到一些表达式，其值随着每次迭代而减小（以有根据的顺序）。在您的情况下，expo是这样一个表达式，因此您的decreases子句就是证明循环终止所需的全部内容。（事实上，这比你需要的要多。如果你完全去掉这个decreases子句，Dafny 会自动猜到这个。）

推理循环的方法是找到一些条件，称为循环不变量，它在每次迭代的最顶端都成立（即，每次评估循环保护时都为真的条件）。您已经编写了一个这样的不变量，即0 <= expo. tempR但是，关于变量和，或者关于这些变量与、和c之间的关系，没有不变量。因此，验证者在循环迭代开始时或循环后对这些变量的值一无所知。expoxn

因此，要验证您的程序是否执行正确的数学运算，您需要通过编写不变条件来说服验证者。

让我开始吧。您的不变量需要做三件事。0：最初需要保持，当第一次到达循环时。也就是说，对于变量的初始值，条件必须为真。1：循环守卫的不变量和否定（只有这些，没有其他你可能认为也成立的事实）必须足以证明后置条件。例如，您唯一可以从当前循环不变量和守卫的否定中推断出的是expo == 0循环之后的内容。2：不变量必须由循环体维护。也就是说，给定循环体开头的不变量和保护，您必须证明在循环体之后不变量再次成立。

在你弄清楚循环不变量应该是什么之后，你需要证明一个关于幂运算的数学事实。你到了那里就会看到。

祝你好运！

PS。以下是有关您的程序的其他一些评论：

您当前在exp调用FastExp. 这意味着您的后置条件定义不明确并且并不总是有意义（这将使尝试建立后置条件的任务变得不可能）。问题是FastExp允许n是0，但你的功能exp没有。您将需要exp定义一个指数0来证明FastExp. 所以，改变exp允许n存在的前提条件0。（然后您必须修复的主体exp。）
Dafny 有一个 type nat，它代表非负整数。因此，如果您愿意，您可以简单地声明和删除这些先决条件，而不是声明n: int和添加先决条件。0 <= nn: nat
有一种更短的定义方式isEven，即a % 2 == 0。
您不需要引入局部变量tempR。你可以直接使用r。
FastExp声明为lemma有点奇怪。Dafny 确实允许引理具有超出参数（这有时非常有用），并且您确实可以使用循环编写引理的证明。但写作的原因FastExp并不是为了表明你可以分配一些价值r来r == exp(x, n)实现——你可以通过 assignment 做到这一点r := exp(x, n);。相反，声明的原因FastExp是您需要一个计算它的程序。为此，请声明FastExp为method. （在 Dafny 中，引理和方法之间唯一的技术区别是方法被编译，而引理被编译器删除。）

loops - Dafny：快速指数计算（循环）

问题描述

解决方案

推荐阅读