Map Comprehension Heuristics

[aferr]

Dafny fails to determine that set s in this code segment is finite.

datatype OUTER = b(x:INNER)

lemma l()
{
    var s := set r : OUTER | true;
}

[aferr]

There is a similar problem with map comprehensions.

[layus]

More generally, dafny does not "destruct" datatypes for bounds checking.
The error message is quite clear however : "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'".

datatype Point = P(x: int, y: int)

method squareSets(a: int, b: int, c: int, d: int) {
    // Finds bounds
    var byCoord := set i, j | a <= i < b && c <= j < d :: P(i, j);
    // Cannot find bounds
    var byPoint := set p: Point | a <= p.x < b && c <= p.y < d;
    // Cannot find bounds
    var byTuple := set t: (int, int) | a <= t.0 < b && c <= t.1 < d :: P(t.0, t.1);
}

@RustanLeino Would this be easy to implement ? It seems that DiscoverBestBounds_MultipleVars should be adapted to discover properties no only on bVars but also on their destructors.

[layus]

@aferr You can always use

lemma l()
{ var s := set a: INNER | true :: b(a); }

[RustanLeino]

@layus : Yes, this would be a possible--and good--thing to improve in the DiscoverBestBounds routines. It will also affect compilation, since the compiler needs to be able to enumerate the values in the set. Source contributions that fix this are welcome. :)

Speaking more broadly, even improved heuristics will remain just heuristics and will run out of steam in some examples. One possibility is to use the syntactic heuristics to cover most interesting cases and to use semantic checks (that is, conditions checked by the verifier) to let users convince the verifier that a given set is indeed finite. One way to do that is to have a way in Dafny to say "I'm declaring the following set and I'm claiming that is it finite because I can show that it is a subset of the following known-to-be finite set". If Dafny had such a feature, then @layus 's clever lemma could be used to convince the verifier that the original set above is indeed finite. We should consider such a language feature if situations like this come up frequently.

Rustan

PS. I have also noticed that heuristics can't figure out that false is a finite range. This would also be good to fix.