Refinement in Dafny

Mar 7, 2014 at 6:02 PM
Edited Mar 8, 2014 at 10:34 AM
Hi,
1- Is there any comprehensive documentation or tutorial for refinement in Dafny? (or any publication?)

2- Is it possible to change the signature of a refined method (add or remove parameters...)? Usually during a stepwise development and in more concrete levels of refinements, it is useful to be able to change the structure of the model/program in a consistent way.
abstract module m0 {
method abc(x:int)
ensures true; // whatever
requires true; // whatever
{
//body
}
}

module m1 refines m0{
method abc(x:int, y:nat) returns (r:nat) // this is not allowed
...;
{
...;
//body of concrete method
}
}
Sadegh
Coordinator
Mar 18, 2014 at 6:14 PM
Hi Sadegh,

I'm happy to see your interest in using the refinement features in Dafny. I'm not convinced that Dafny provides the right feature set at the moment, so your feedback is very useful. More examples of what you would like to write and what you wish to express would be awesome.
  1. I'm afraid there's no comprehensive documentation at this time. There's a body of examples in the test suite (search the *.dfy files for the keyword "refines", and note that the Test/dafny0 directory only contains "boring" functionality-test examples). It is possible that my talk at SPLASH 2012 (including the last demo I gave in that talk) sheds some light on how the refinement features (but given what you say above, you may already know all I say in that talk). Btw, if you're not already, I would suggest using the Dafny IDE in Visual Studio, because then you can hover the mouse over each "..." and "}" to see what code is inherited from the refined module.
  2. At this time, you cannot change the signature of class members, except for switching between ghost and non-ghost entities. Given that Event-B users in effect change the signature of events has made me think that this would be a good idea in Dafny, too. However, I lacked particular examples. My idea had been that Dafny could support the addition of parameters, and that any parameter you wanted to remove could be turned into a ghost parameter -- this would mean that, as long as the refined method resolves and type checks, the verification of that method would not need to be redone.
As I said, I'd be happy to see wishful examples. Also, depending on your interest level, I would also welcome either contributions to or collaboration on these features.

Rustan
Marked as answer by dalvandi on 4/18/2014 at 10:23 AM
Apr 18, 2014 at 6:29 PM
Edited Apr 18, 2014 at 6:42 PM
Hi Rustan,

Many thanks. The SPLASH talk was very informative. I am working on some Event-B models and trying to implement them in Dafny, so I may find interesting examples for this. About the mouse hover, it dose not work in my VS 2012 with the latest version of Dafny installed. It works for other things like variables but not for "...".

Sadegh
Coordinator
Apr 20, 2014 at 3:59 AM
Hi Sadegh,

Might it be that you have more than one version of the Dafny extension on your machine? If you think this might be the case, then uninstall the previous version(s) and reinstall the new. There are some instructions for how to do this on here.

If you don't think that's the problem, then perhaps the latest binaries dropped at dafny.codeplex.com didn't have the right version. I will make a new drop of a binary there later today. If you think that's the problem, try that new version.

Or, are you building from sources? In that case, could it be that you have one version of the Dafny extension in your Visual Studio but the one you're building yourself is going to the Experimental Instance of Visual Studio? (That's where it ends up by default when you build it yourself.) If this may be the case, then make sure that when you want to use the Dafny IDE, start the Experimental Instance of Visual Studio.

I hope one of these will work.

Rustan
Apr 20, 2014 at 5:43 PM
Hi Rustan,

Thanks for your reply. I installed the latest binaries and the problem solved.


Sadegh