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;
}

解决方法

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

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

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

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

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

祝你好运！

附注。以下是关于您的程序的其他一些评论：

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

dafny invariants loop-invariant loops

Dafny：快速指数计算循环

问题描述

解决方法

相关问答