主页 / coding / 问题

问题[verification](coding)

Martin Hope
MogicFrog
Asked: 2023-09-14 19:47:30 +0800 CST
  • 6

假设我们有一个名为 的数据类型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
Martin Hope
Carl
Asked: 2023-08-18 00:54:53 +0800 CST
  • 5

我想计算 Dafny 中设置小于阈值的元素，但我无法弄清楚“确保”。

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |{i in numbers | i < threshold}|
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }

  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

错误是：this operator chain cannot continue with an ascending operator

verification