Dafny: current documentation is out-of-date

Aug 19, 2012 at 7:46 PM

Is there any documentation about new interesting features of Dafny such as `module', `refines', `codatatype' statements ? What is semantics of `(==)' ?

Coordinator
Aug 20, 2012 at 1:31 AM

Thanks for noticing these new features!  Some of these are experimental and are likely to undergo a lot of change before they feel "final".  But let me offer an overview here of:

  • 0.  Modules
  • 1.  Map types
  • 2.  Auto-contracts
  • 3.  Refinement
  • 4.  Co-induction
  • 5.  Editor improvements

0.  MODULES

Dafny has supported modules for more than a year.  But this summer, Jason Koenig worked on a revised module system.  In the new system (which is currently implemented), modules can be nested.  A syntactic difference from before is that module imports are now declared inside the module's body, not at the top of its declaration.  So, where you used to write

module M imports J, K
{
    //  type declarations...
}

you now write:

module M
{
    import J;
    import K;
    // type declarations...
}

Almost.  Previously, when you imported a module, you could use its named unqualified (for example, if module J declared a class C, you could refer to it as just C in module M), and there was only limited support for qualified names (like J.C).  With the import declarations above, the types declared by the imported module must be referred to in a qualified way (that is, like J.C).  If you also want to be able to refer to the names unqualified, you can import a module as "opened", like this:

module M
{
    import opened J;
    import K;
    // type declarations...
}

Moreover, in the new module system, modules support abstraction.  This is done in connection with the refinement features in Dafny (see below).  You can say "import N as MyInterface;".  This means that you're importing some module that looks like the module MyInterface and you're going to refer to it under the name N.  You can (at the same time or) later decide on which actual module you want N to refer to (for the sake of compilation).

This gives you a taste of the new module features.  Jason has written documentation for module system.  We're going to release that documentation at the same time as we put an updated version of Dafny on rise4fun (which will happen soon, perhaps next week).

1.  MAP TYPES

Jason also implemented finite-map types in Dafny.  These are written map<T,U>, where T is the domain type (the "keys") and U is the range type (the "values").  A number of operations are supported for maps.  Like for multisets, I expect that we need more experimentation to make sure the prover support for map types works well.  So, if you use maps now, it will probably reduce your frustrations if you are aware that you may have to work a little harder to get verifications to go through.  (Also, I have been thinking that the pun of "x in m", which currently means "x is in the domain of the map m", would be less confusing if it were written something like "x in domain(m)" or "x in m.Domain".  If this feeling persists, I may change the syntax a bit.)

2.  AUTO-CONTRACTS

If you have used Dafny to write programs that create and manipulate mutable, dynamic data structures, you will have used the dynamic-frames style of specifications that Dafny supports.  You will also have noticed that using these features is somewhat verbose and idiomatic.  I have been hesitant to lock Dafny into a particular style of specifications, even though doing so is likely to reduce verbosity and clutter in many common cases.  (My hesitation stems from our Spec# experience, where we had many defaults that made simple programs easy to specify.  Too many defaults.  When the defaults were not good enough, it took a great deal of expertise to undo the defaults and write specifications that said what you really wanted to say.  And some of the specifications were available only via the defaults, which made the system harder to use.  Dafny benefits from the Spec# experience and provides a next-generation system.)

If you want to write programs with mutable, dynamic data structures, then you will probably need to learn the dynamic-frames idioms in Dafny.  Which is not too hard.  However, if you want to teach students about these, then I feel that the learning curve gets too steep--the students suddenly must know about object invariants, abstraction, framing, and the dynamic-frames specification idioms.  Auto-contracts are an attempt at making the learning curve gentler.

The idea is that you can mark a class with the {:autocontracts} attribute.  Dafny will then supply a lot of the idiomatic specifications for you.  For teaching purposes, this means you can first introduce just object invariants.  As your programs get more difficult, you'll need to teach more about dynamic frames, but (the hope is that) by that time, the students will understand object invariants.

Alas, there is no documentation for {:autocontracts}, and the features are still somewhat experimental.  For example, beyond the basics, some more experimentation would be useful to figure out what the best {:autocontract} expansions are, and error messages could be improved.  Let me say these things:

To get an idea of what {:autocontracts} can do, compare the following two programs:

  • Test/vstte2012/RingBuffer.dfy
  • Tets/vstte2012/RingBufferAuto.dfy

If you want to see exactly what {:autocontracts} does on a program, use the /dprint or /rprint switches.  /dprint prints the input program after some expansion and before resolution; /rprint prints the input program after resolution.  You can use these switches with a filename of "-", which says to print to standard output; for example, you can say /dprint:- or /rprint:-.

To turn off what is auto-generated for a particular field or method or parameter, you can mark that field or method or parameter with {:autocontract false}.

The Dafny source code is now organized in such a way that features like {:autocontracts} are easy to implement.  Hence, if you want to experiment with alternate behavior for {:autocontracts} or your own auto-markups, then that can be done fairly easily.

3.  REFINEMENT

Dafny now has some support for refinement.  This means that you can program "in stages", by first writing the most essential details of the program and later filling in more details (like introducing optimizations).  These features are still somewhat experimental and I do expect them to undergo further changes (both syntactic and semantic changes).  However, it may be that we understand what features we now want.  We'll try to get them implemented and tried out soon.  For now, if you want an idea of what the intent behind the features is, I suggest you take a look at the following two programs in the test suite:

  • Test/dafny2/StoreAndRetrieve.dfy
  • Test/dafny1/SchorrWaite-stages.dfy

The refinement features include "program skeletons", which Kuat Yessenov had worked on in Chalice.  For Dafny, this means you can in a refining module say "..." in various places (see the test files above).  This seems to be a nice feature when you're doing just one refinement, but if you do more or if the structure of a method body is more complicated, the /rprint switch that I mentioned above may be useful.  (Ultimately, the syntactic "..." constructs would seem better replaced by fancy IDE support, but "..." is at least good enough to let us experiment with the refinement features now.)

There are (probably) issues in the interplay between {:autocontracts} and refinement that haven't been worked out yet.  If you use these features together, beware, and feel free to let me know what you think the desired behavior is.

4.  CO-INDUCTION

For a number of reasons--one of them being just scientific curiosity--I've become interested in supporting not just various inductive features in a programming language (like inductive datatypes, recursive functions, inductive proofs, and Dafny's automatic tactic for introducing an inductive hypothesis--see my VMCAI 2012 paper) but also co-inductive features.  In a nutshell, co-induction allows you to deal with infinite values (like infinite lists or trees), neverending self-calls, and infinite proofs.  Different co-inductive features have been incorporated in a number of languages before (among them Lucid, Charity, Coq, and Haskell).  I'd like to explore the use of such features in a language that has an SMT-based program verifier.

I've added some experimental co-inductive features to Dafny.  These include co-inductive datatypes (introduced using the keyword "codatatype", which is otherwise very much like "datatype"), co-recursive calls (which I currently support without having to make a distinction between functions and "co-functions"), and co-predicates (which are essentially predicates on infinite data values).  As far as co-inductive proofs, I currently have special support for proving co-predicates.  All of these features are definitely experimental and are very likely to change.  (In fact, it may be that I've mostly introduced infinite values at this point, and not full co-induction.  I would also like to find a vastly better way to give co-inductive proofs.)  To get a flavor of the current state of my experimental implementation, see:

  • Test/dafny0/CoPredicates.dfy

Before co-inductive datatypes, Dafny supported an equality operation on every type.  This meant that a you could write, say, a generic linear-search method.  But in the presence of co-inductive datatypes, it is not possible to support equality at run time, since that would involve an infinite number of comparisons.  I admit, this was troubling to me for a while, until I decided I just had to bite the bullet and introduce a distinction between types that support equality and types that do not support equality.

Thus, when you now declare a type parameter, like the T in:

method LinearSearch<T>(a: array<T>, key: T) returns (r: int)

you're referring to any type whatsoever.  If you want to restrict the type parameter T so that it can only refer to types that support equality (and disequality), you follow the name "T" by "(==)".  For example:

method LinearSearch<T(==)>(a: array<T>, key: T) returns (r: int)

One of the other consequences of having a distinction between types that do or don't support equality, sets can only be created over types that support equality (how else would you test the set for membership?).

Dafny tries to help out a little.  If the type signature of a function or method makes it evident that a type parameter must denote only equality-supporting types, then Dafny will infer that automatically.  For example, if one of the parameters of the function of method has type set<T> where T is a type parameter, then Dafny will infer that T to be a T(==).

When a program uses values of a type inconsistently with the type's support for equality, I have tried to make the error messages point out how to fix the problem.  For example, some error messages say "try following the declaration of 'T' with '(==)'".

By the way, the problem with comparing infinite values for equality arises only at run time.  Thus, in ghost constructs (like specifications), Dafny allows you to use equality on any type.

Although the co-inductive features in Dafny are currently experimental, the notion of equality-supporting types is here to stay.

5.  EDITOR IMPROVEMENTS

Here's a feature that I think will get all Dafny users psyched.  The editor interfaces to Dafny, both on the web and in Visual Studio, has improved.

On the web, rise4fun.com/Dafny now supports syntax highlighting, parenthesis matching, and auto-indentation.  Thanks to Daan Leijen for working his magic!  (Chalice, Boogie, and Spec# on rise4fun will also get this support really soon.)

If you use Visual Studio for editing Dafny programs, you may have noticed that our sources contain two similar directories:  Util/VS2010/Dafny and Util/VS2010/DafnyExtension.  Our build instructions say to use the former, which was based on an old way to integrate into Visual Studio.  That mode also included use of a batch file that would fire up the .NET machine (even though one is also running inside Visual Studio) and start the Dafny verifier there.  The alternative mode--DafnyExtension--is something I started more than 18 months ago and that has been on the back burner since.  Until the last couple of weeks.

I have now put some more time into the DafnyExtension mode, which is based on the Visual Studio Extensions model.  It provides lots of nice flexibility.  The mode does not just syntax highlighting, but also parenthesis matching, outlining, and hover text (with type information) about identifiers.  Moreover, this new mode calls the Dafny verifier directly (in the same address space), which means that it is much snappier than the previous mode (where you sometimes had to wait a second or two before the verifier would even start running).  The new mode also provides visual indications of buffer changes that have taken place since (yellow) the most recent time the verifier finished and (orange) the most recent time the verifier was started--this means you can easily tell when the verifier is running.

There are some issues with the new mode.  One issue I have noticed is that, in the parser implementation of both Dafny and Boogie, there are some static field, and these don't do so well with the background threading that DafnyExtension does.  I hope to get that problem fixed soon.

The new mode still doesn't have an installer (and neither does Dafny itself), so you still have to build it from source.  But this is now easier to do than before.  (That is, kicking off the build is as easy as it was before, but now you don't have to mess with setting up that batch file and everything.)  If you want to use the new mode (which I would like to recommend), then you first need to uninstall the previous Dafny mode for Visual Studio.  Here's how you do that:

  • From the Windows Start menu, Microsoft Visual Studio 2010 SDK -> Tools -> Reset the Microsoft Visual Studio 2010 Experimental instance.

Then, build $BOOGIE/Util/VS2010/DafnyExtension/DafnyExtension.sln.

Note, the build of DafnyExtension is set up to make the extension available in the Experimental instance of VS.  So, you do need to have the Visual Studio SDK installed, see the installation instructions for the old Dafny mode for VS.  (This requirement could be changed if we have an installer.)

Finally, let me remind you all that Dafny is open source.  So, if you feel like there are features you'd want to have--for example, in the Visual Studio integration--then feel free to implement and share them.

I hope you enjoy these new features in Dafny.

Program safely!

  Rustan

Aug 23, 2012 at 3:10 PM

Thank you very much, Rustan!