Dafny: strange assertion violation

Oct 1, 2012 at 6:00 PM

Why does Dafny say "assertion violation" ( http://rise4fun.com/Dafny/slg0 ) if this assertion is the same as precondition and assertion is the first statement in the method body ?

Oct 1, 2012 at 6:33 PM

It has to do with triggering of quantifiers.  The δ (by the way, how cool is that!) only appears together with a plus inside the quantifier body, and that renders it essentially useless for a trigger.  This (semantically equivalent) variation of the program verifies:  http://rise4fun.com/Dafny/Qpqc

To explain triggers in more detail would take a lot longer.  If you'd like to learn more, I recommend the following paper:

Reasoning about Comprehensions with First-Order SMT Solvers. <small>[PDF]</small>
K. Rustan M. Leino and Rosemary Monahan.
SAC 2009.


Oct 2, 2012 at 9:25 AM

Oh, yes, matching triggers! I've added it and my program is verified now. Thank you, Rustan!