CODEWITHSUNDEEP
dafnyformal-verification
Carl
Carl

Reputation: 383

In Dafny, show that a sequence of unique elements has the same size as the set of the same elements

I've created a verified SortedMap in Dafny. It is a sequence of (key, value) pairs. The keys are sorted, distinct integers. I can't figure how to show that the length of the "KeySet" must be equal to the length of the sequence.

-- Carl

Error:

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

Simplifed code:

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);

}

Upvotes: 1

Views: 111

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

This property requires a proof by induction. Since the way you defined the function is not recursive, this is not easy to do in Dafny. You can either (1) prove the property in a separate inductive lemma, or (2) change the definition to be recursive.

(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)
}

Upvotes: 2

Related Questions