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