Dafny: about strength of proving

Oct 1, 2012 at 10:38 PM

I study refinement in Dafny (later I studied refinement in theory only). It's really cool! Thanks, Rustan, for refinement in Dafny! I write and verify simple implementation of FIFO: http://rise4fun.com/Dafny/6RqT. And I'm frustrated about how many proofs I has to do manually in this simple implementation. I'm sorry if I wrong use refinement in Dafny. For example, I think Dafny should prove (automatically) assertion on the line #171 (instead of this I has to write assertion on lines #168 which repeats postcondition of the method "enqueue"). The same issue is on line #173 (To prove it I has to write assertion on line #169 which repeats postcondition of the method "dequeue").

Are these additional assertions really needed or I use refinement in Dafny incorrectly ?

Oct 2, 2012 at 9:53 AM

The same question about datatypes only (without refinement) : Dafny unrolls recursion by 1 step (by default) so Dafny can't automatically prove assertion on line #22 in the following program: http://rise4fun.com/Dafny/7slC . I can prove this assertion manually (see line #23). But I'm interesting in way of automatically proving the assertion on the line #22 (i.e. without changing of the assertion, as in line #23, and without additional lemmas), is it possible ?

Coordinator
Oct 18, 2012 at 2:51 AM

Recently, I changed the way method specifications are encoded for intra-module calls and refinement.  That change seems to have fixed the problem you reported of having to repeat the postconditions.

I am able to get your first example through with no supporting lemmas in test() and test2().  You are using the refinement features along the lines of their intended use.

I am not surprised that you need the two inductive lemmas in dequeue(), since the a_Queue representation is quite different from the sequence representation, and in particular, the a_Queue representation is inside-out from what dequeue() needs (whereas enqueue does fine with it and does not need inductive lemmas).

As a syntactic matter, there's an implicit "...;" at the end of every block statement (that is, at the end of every curly-brace pair).  So, you can omit those "...;" if you think that makes your program cleaner (but I realize you may also thinking that having the "...;" makes the program text easier to understand).  By the way, if you're interested in seeing how Dafny stiches together the states after filling in the ...'s, then use the /rprint command-line switch.  For example, "dafny Prog.dfy /rprint:-" will print the resolved and expanded program to standard output.  You will notice that the assign-such-that statement in Q_1.dequeue has been replaced by an ordinary assignment statement followed by an assert.

I filled in the proof of Lemma1, for which I used Dafny's new really-cool "calc" features.  I also did some other minor modifications of the program, mostly just to demonstrate some alternative features.  Here is the result: http://rise4fun.com/Dafny/3i1R, but it doesn't go through rise4fun today, because of the newer Dafny features I'm using (I will update the version on rise4fun before I speak at SPLASH next week).  I added various comments in the program to explain the features.  (In the process, I also noticed a compilation bug, which I haven't fixed yet.)

  Rustan

Coordinator
Oct 18, 2012 at 2:57 AM

Eugene,

For the question in your second post above:  No, you need to tickle Dafny into unrolling "size" or "push" more than once, which is what your line 23 is doing.  You could render line 23 slightly differently, but the idea is still the same.  For example, you could shorten line 23 to:

  assert size(s1) == 1 + size(push(empty, 10)) == 2;

or you can use the new "calc" construct:

  calc {
    size(s1);
    1 + size(push(empty, 10));
    2;
  }

(Yeah, I told you "calc" was cool!)

  Rustan

Oct 19, 2012 at 2:14 PM
rustanleino wrote:

I will update the version on rise4fun before I speak at SPLASH next week

  Rustan

And will rise4fun support "calc" cool feature after update ?

Happy speaking at SPLASH ! I think your topic is very interesting. Are you planning to publish an article about staged development (using Dafny) ?

 

Eugene

Coordinator
Oct 19, 2012 at 6:35 PM

Yes, the "calc" feature (which is joint work with Nadia Polikarpova) will be in the release.

And yes, Jason Koenig and I hope to write something about the staged development featuers in Dafny, but haven't yet done so.

  Rustan