1

Dafny has no problem with this definition of a set intersection function.

function method intersection(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A && x in B
}

But when it comes to union, Dafny complains, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'". A and B are finite, and so, clearly the union is, too.

function method union(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A || x in B
}

What explains this, to-a-beginner seemingly discrepant, behavior?

Kevin S
  • 497
  • 2
  • 10

1 Answers1

1

This is indeed potentially surprising!

First, let me note that in practice, Dafny has built-in operators for intersection and union that it knows preserve finiteness. So you don't need to use set comprehensions to express these ideas. Instead you could just say A * B and A + B respectively.

However, my guess is that you're running into a more complicated example where you're using a set comprehension with a disjunction and are confused about why Dafny can't prove it finite.

Dafny uses syntactic heuristics to determine whether a set comprehension is finite. Unfortunately, these heuristics are not well documented anywhere. For purposes of this question, the key point is that the heuristics either depend on the type of the comprehension's bound variables, or look for a conjunct that constrains elements to be bounded in some other way. For example, Dafny can prove 

set x: int | 0 <= x < 10 && ...

finite, as well as 

set x:A | x in S && ...

In both cases, it is essential that the relevant bounds be conjuncts. Dafny has no syntactic heuristic for proving a bound for disjunctions, although one could imagine adding one. That is why Dafny cannot prove your union function finite.

As an aside, another work around would be to use potentially infinite sets (written iset in Dafny). If you don't need use the cardinality of the sets, then these might work better.

James Wilcox
  • 5,307
  • 16
  • 25
  • Our use case for Dafny is pedagogy. So we'd like to be able to write all the usual definitions, of things like what "union" means, in Dafny, in a way that one can actually also run. It'd be good to be able to write such a simple definition as "set union" and not have Dafny reject it. Is there any theoretical difficulty with implementing a reasonably effective heuristic, or is it really just a matter of this being a missing feature that could be added to good effect at a reasonable cost? (Thanks for the help.) – Kevin S Mar 15 '18 at 03:29
  • There's no theoretical difficulty, just a matter of adding the implementation. Indeed, if the expression was first refactored into a disjunction, then the current heuristics could be run on each disjunct and then the results could be combined. The implementation is already set up to handle different kinds of "bounded pools", so adding an overarching "disjunction bounded pool" would fit in. (This would be a great student project. :)) – Rustan Leino Mar 15 '18 at 17:45