主页 / coding / 问题 / 79599041
Accepted
f1sherb0y
Asked: 2025-04-30 02:51:53 +0800 CST

Dafny 验证器无法证明多重集的结果

  • 772

我正在与 Dafny 合作，试图了解规范（特别是修改和确保多集）如何影响验证。

我有一个方法do_nothing，用于修改数组 a，但确保其元素的多集保持不变。该方法的主体为空。

method do_nothing(a: array<int>)
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  // nothing is done
}

method test()
{
  var a := new int[6] [2, -3, 4, 1, 1, 7];
  assert a[..] == [2, -3, 4, 1, 1, 7]; // Verifies
  assert a[0] !=0 ;                    // Verifies

  do_nothing(a);

  assert a[0] != 0; // <-- Verification Error: This assertion cannot be proved
}

我的期望：

a由于其中根本没有 0 ，并且 dafny 同意do_nothing确保multiset(a[..]) == multiset(old(a[..]))。因此，断言 a[0] != 0 应该成立并验证成功。

问题：

Dafny 无法验证最终断言 assert a[0] != 0;

functional-programming

2 个回答

  1. 您的方法do_nothing仅指定要保持multiset(a[..]) 完整，而不一定是数组a。由于多重集中的元素没有定义的顺序，因此即使您排列数组中的条目，此属性也会保留。例如，以下是do_nothingwhen的正确实现a.Length >1：

    method do_nothing(a: array<int>)
  requires a.Length>1
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
{ 
    a[0],a[1] := a[1],a[0]; 
}

    现在，在的调用站点do_nothing内部test，Dafny 并不关心您的实现do_nothing，它只考虑其规范——并且如上所述，这并不能保证a[0]可能不会被交换为其他的a[i]。

    • 0
  2. Best Answer

    多重集具有隐藏的触发器，以避免触发器压倒 Dafny 的验证器。

    您可以在之后添加此断言do_nothing以帮助 Dafny 触发多重集上的一些必要公理。

    assert 0 !in multiset(a[..]);

    这将使你的代码通过验证。请注意，由于这是关于触发器的，因此插入以下无操作代码也会产生同样的效果

    ghost var _ := 0 !in multiset(a[..]);
    • 0

相关问题