1

一些算法（分配二叉树......）需要计算以 2 为底的指数。如何为这种原生类型计算它？

newtype {:nativeType "uint"} u32 =
  x: nat | 0 <= x < 2147483648

这是一个明显的尝试：

function pow2(n: u32): (r: u32)
  requires n < 10
{
  if n == 0 then 1 else 2 * pow2(n - 1)
}

它失败了，因为 Dafny 怀疑产品是否低于u32的最大值。如何证明它的值低于 2**10？

4

2 回答 2

1

有点作弊，但是域如此狭窄，这很好用。

const pow2: seq<u32> :=
  [0x1, 0x2, 0x4, 0x8, 0x10, 0x20];

lemma pow2_exponential(n: u32)
  ensures n == 0    ==> pow2[n] == 1
  ensures 0 < n < 6 ==> pow2[n] == 2 * pow2[n - 1]  
{}
于 2017-09-29T07:42:03.437 回答
1

在这种情况下，更方便的是首先定义函数的无界版本，然后证明一个引理表明当n < 10（或n < 32，甚至）它在有界时。

function pow2(n: nat): int
{
  if n == 0 then 1 else 2 * pow2(n - 1)
}

lemma pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{ /* omitted here; two proofs given below */ }

function pow2u32(n: u32): u32
    requires n < 32
{
    pow2Bounds(n as nat);
    pow2(n as nat) as u32
}

直觉上，我们可能期望引理自动通过，因为只有少数情况需要考虑：n = 0, n = 1, ... n = 31。但 Dafny 不会自动执行此类案例分析。相反，我们有几个选择。

第一个证明

首先，我们可以证明一个更普遍的性质，通过归纳推理的魔力，它更容易证明，尽管它比我们需要的要强。

lemma pow2Monotone(a: nat, b: nat)
    requires a < b
    ensures pow2(a) < pow2(b)
{}  // Dafny is able to prove this automatically by induction.

然后引理随之而来。

lemma pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{
    pow2Monotone(n, 32);
}

第二个证明

另一种证明它的方法是告诉 Dafny 它应该pow2使用:fuel属性展开最多 32 次。这 32 次展开基本上与要求 Dafny 对每个可能的值进行案例分析相同。然后，Dafny 无需额外帮助即可完成证明。

lemma {:fuel pow2,31,32} pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{}

该:fuel属性（轻微地）记录在Dafny 参考手册的第 24 节中。

于 2017-09-28T23:07:39.313 回答