主页 / coding / 问题 / 77104592
Accepted
MogicFrog
Asked: 2023-09-14 19:47:30 +0800 CST

一个奇怪的谓词，无法证明体内已经定义的断言

  • 772

假设我们有一个名为 的数据类型Tree，以及一个size计算其大小的函数

datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)
function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

现在由于某些原因，我想让这棵树以某种方式“平衡”。具体来说，就是

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= alpha*(size(t) as real)
    && size(t.right) as real <= alpha*(size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

当成alpha_weight_balanced立时，树的每个子节点的大小t都小于alpha*size(t)。自然地，这个引理应该成立

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= alpha*(size(t) as real)
{}

然而，达夫尼无法证明这个“明显”的引理。我什至尝试过size像这样包裹

function f(a: int): int
// there is no implemetion for `f`

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    f(size(t.left)) as real <= alpha*f(size(t)) as real
    && f(size(t.right)) as real <= alpha*f(size(t)) as real
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures     f(size(t.left)) as real <= alpha*f(size(t)) as real
              && f(size(t.right)) as real <= alpha*f(size(t)) as real
{
}

达夫尼成功地证明了这一点。但是如果我修改这个函数f

function f(a: int): int
ensures f(a) == a

证明又失败了。

我对此很困惑，有人知道为什么吗？

verification

1 个回答

  1. Best Answer

    避免验证失败的一种方法是将实数乘法隐藏在函数内。在 nat 和 int 中进行此类验证时不需要这样做的原因是 dafny 会自动为您做。

    datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)

function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

function multiply(a: real, b: real): real { a * b }

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= multiply(alpha, size(t) as real)
    && size(t.right) as real <= multiply(alpha, size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= multiply(alpha, size(t) as real)
{}
    • 1

相关问题