主页 / coding / 问题 / 76937544
Accepted
Carl
Asked: 2023-08-20 08:39:47 +0800 CST

在 Dafny 中，证明一系列唯一元素与相同元素的集合具有相同的大小

  • 772

我在 Dafny 中创建了一个经过验证的 SortedMap。它是（键，值）对的序列。键是排序的、不同的整数。我不知道如何表明“KeySet”的长度必须等于序列的长度。

——卡尔

错误：

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

简化代码：

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);

}
dafny

1 个回答

  1. Best Answer

    该性质需要归纳证明。由于定义函数的方式不是递归的，因此在 Dafny 中这并不容易做到。您可以 (1) 在单独的归纳引理中证明该属性，或者 (2) 将定义更改为递归。

    (1)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
{
  set i | i in sorted_seq :: i.0
}

lemma KeySetSize(sorted_seq: seq<(int, int)>)
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  if sorted_seq == [] {
  } else {
    assert KeySet(sorted_seq) == {sorted_seq[0].0} + KeySet(sorted_seq[1..]);
    KeySetSize(sorted_seq[1..]);
  }
}

// You can optionally then recombined the bare function and lemma 
// into a function with the right specification.
function KeySetWithPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySetWithPost(sorted_seq)| == |sorted_seq|
{
  KeySetSize(sorted_seq);
  KeySet(sorted_seq)
}

    (2)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
  ensures KeySet(sorted_seq) == set i | i in sorted_seq :: i.0
{
  if sorted_seq == [] then
    {}
  else
    {sorted_seq[0].0} + KeySet(sorted_seq[1..])
}

// Notice the extra postcondition above, which is required for the proof
// to go through. Once the proof is done, you can wrap it in a function
// with no extra postcondition.
function KeySetWithoutExtraPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  KeySet(sorted_seq)
}
    • 2

相关问题