Why does Dafny complain about this use of a set constructor: `set i: int | Contains(i)`?

Question

Why does Dafny complain about this use of a set constructor: set i: int | Contains(i)? Here is an example:

module test {

  ghost const things: set<int>

  predicate Contains(t: int) 
  {
    t in things
  }

  function ThisIsOk(): set<int> {
    set i: int | i in things && i > 0
  }

  function ThisIsNotOk(): set<int> {
    set i: int | Contains(i) && i > 0
  }

}

which produces the error “the result of a set comprehension must be finite, but Dafny’s heuristics can’t figure out how to produce a bounded set of values for ‘i’”.

Answer

In constructing a set, which must be finite, Dafny must prove that the set is indeed finite. When the constructor has i in things inlined, Dafny can see that the set of values of i for which the predicate is true can be no larger than things, which is already known by declaration to be a finite set. However, when the predicate is Contains, Dafny cannot in general see that fact. The Dafny’s heuristic for determining that the constructor is producing a finite set does not inspect the body of Contains even though that is a transparent function. Note that if the constructor and the return type of ThisIsNotOK is made iset, Dafny does not complain.

An alternate general way to refine a set is given by this example:

module test {

  ghost const things: set<int>

  function RefineThings(condition: int -> bool): set<int>
  {
    set t: int | t in things && condition(t)
  }

  function ThisIsOk(): set<int> {
    set i: int | i in things && i > 0
  }

  function ThisIsOkAgain(): set<int> {
    RefineThings(i => i > 0)
  }
}