predicate test(x: int)
{
exists y :: x % y == 0
}
When I code quantifiers in a format similar to the above function, Dafny says:
Quantifiers in non-ghost contexts must be compilable, but Dafny’s heuristics can’t figure out how to produce or compile a bounded set of values for ‘y’.
How to fix this problem?
Also, is there any way I can learn the detailed heuristics used in Dafny to prove quantifiers? I’ve found them quite abstract yet lacking learning material.
You need to convert this predicate into ghost predicate
ghost predicate test(x: int)
{
exists y :: y > 0 && x % y == 0
}
These are some resources about qualifiers to better understand them
- Qualifiers in Dafny – https://dafny.org/dafny/OnlineTutorial/guide#Quantifiers
- How Dafny handles Qualifiers – https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those
- How Dafny selects triggers for Qualifiers – https://pit-claudel.fr/clement/papers/dafny-trigger-selection-CAV16.pdf
Regarding proving qualifiers, it is no different than asserting method / function post condition. You assume some fixed value of bound variables with associated precondition and proceeds to prove using lemma and assert.