Beginner question: limitations of Dafny

Aug 27, 2013 at 1:10 PM
Hi!
I've just started to experiment with Dafny and is considering using it for teaching. In translating some of my examples into Dafny, I came across some (to me) unexpected behaviour.

The following small program has one method which sets a boolean field depending on whether the a secret number has been guessed:
http://rise4fun.com/Dafny/8DaR

There are two conditional ensures-clauses, depending on right/wrong guess. As seen in the programs Main method, I'd expect to assert that after a correct guess, the secret is indeed known, but this assertion fails. Is it the case that Dafny cannot figure out which of the two conditional ensures clauses hold after the call? It looks as if it does not try to instantiate them, is that correct?
Developer
Aug 27, 2013 at 1:57 PM
Hi,

great to hear that you are thinking about using Dafny for teaching!

In your example, the assertion can't be verified because the modifies clause of method 'guess' is too liberal. If you change it to "modifies this`known" or if you add a postcondition that ensures that the 'secret' did not change, the assertion can be verified.

Btw, if you are using the Visual Studio extension you can easily spot this issue by inspecting the counterexample: simply click on the red dot for the assertion violation and compare the value of field 'secret' in the Boogie Verification Debugger window by selecting a blue dot (intermediate state in the counterexample trace) before and after the method call.

Best regards,

Valentin
Sep 16, 2013 at 6:24 PM
Thanks for your help. I'm not using Visual Studio, which is probably why I didn't spot the (obvious) mistake.

So, out of curiosity, I'm wondering if there are any support (or plans for) something like the "assignable" keyword in JML? We were using JML in the course before, and in translating some of our slightly larger examples to Dafny, I find myself writing a lot of frame-conditions of things that don't change, which quickly becomes a bit verbose.
Developer
Sep 28, 2013 at 4:29 PM
I'm not quite sure what you mean by "something like the 'assignable' keyword in JML", but it possible to specify that only certain fields (e.g., field 'f' of object 'o') have been modified using the following syntax:

modifies o`f;

Please let me know if that's not what you were looking for.

Valentin
Sep 30, 2013 at 1:36 PM
Well, the problem sees to be that Dafny does not allow to put fields that are of primitive types (e.g. bool, int) in modifies clauses. Supposing I have some method which only modifies a boolean field b, I put:

modifies this.b;

...

However, I then get an error message from the compiler:
Error: a modifies-clause expression must denote an object or a collection of objects (instead got bool)

So, if instead I put

modifies this;

it works, but then requires me to write lots of ugly frame-conditions saying that all the other fields does not change. Guessing I'm missing something here.
Developer
Sep 30, 2013 at 2:43 PM
This is exactly what the syntax I had mentioned in my previous posts is good for. Note that you need to use a backtick character before the field name, not a period.

Valentin
Coordinator
Dec 4, 2013 at 12:57 AM
The JML "assignable" clause has the same meaning as Dafny's "modifies" clause (except perhaps in some advanced cases with JML's purity or other things, which I have not kept up with completely). A difference is that Dafny's modifies clause takes as argument a list of expressions that can either be objects or sets of objects, whereas JML uses l-values. This is because Dafny, in the common case, reasons about such modifications at the granularity of objects, not at the granularity of fields. As Valentin showed above, you can get the field-granularity behavior in Dafny if you use the backtick notation (which is syntax borrowed from Region Logic).

Rustan