Dafny: datatype indicators disjointness

Oct 2, 2012 at 12:00 AM

I'm wonder why Dafny can't automatically verify the following (simple, as I see) program (with assertion violation) : http://rise4fun.com/Dafny/idzf . Yes, I can prove this assertion manually (using additional ghost method), but why Dafny can't prove it itself ?

Oct 17, 2012 at 1:06 AM

The reason the property

model.a_empty? || model.a_append?

is not included is that it can give rise to really bad prover performance (the prover is now invited to consider the two cases).  I just tried adding it in just certain places, like just for method in-parameters, or function parameters and results, or just in places where a_empty? or a_append? is explicitly mentioned.  Unfortunately, with each such change, the Dafny test suite takes a big hit--in some cases taking 2 or 3 times as long to verify, and in some cases causing out-of-memory errors in the prover.  In most cases, things work just fine--the bad performance is caused by 1 or a few programs.

It is possible that this would improve if Dafny didn't roll its own datatypes but instead relied on the ones provided by Boogie and SMT Lib.

For now, I'm afraid you'll just have to write the lemma.


Oct 17, 2012 at 11:16 AM

Ok. Thank you, Rustan!

Oct 17, 2012 at 10:35 PM

After beefing up properties for just method in-parameters (see http://boogie.codeplex.com/discussions/398658), I went back and added the needed datatype property for method in-parameters as well.  So, in the example above, if "model" is a method in-parameter, then Dafny will know the property.