Dafny：快速指数计算（循环）答案

【问题标题】：Dafny: Fast Exponent Calculation (Loops)Dafny：快速指数计算（循环）
【发布时间】：2021-07-14 00:35:37
【问题描述】：

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

上下文：

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

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

我不知道在循环的decrease和invariants中放什么；
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;
}

【问题讨论】：

标签： loops dafny invariants loop-invariant

【解决方案1】：

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

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

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

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

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

祝你好运！

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

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

【讨论】：