Dafny command-line switches

Mar 17, 2014 at 2:40 AM
Where can I find a list of Dafny's command-line switches (options), and what they do?

In particular, I'm looking for one that checks you have no "miracles" left in your code, i.e. no assumes, empty method bodies etc.

Mar 18, 2014 at 2:14 AM
dafny /help
from the command line will list the supported switches along with descriptions of what they do.

The particular behavior you're looking for is automatically generated by the compiler. That is, the verifier is happy with miracles, but the compiler, which runs after the verifier, is not and will issue complaints.

A related command-line switch is /noCheating, which converts some miracles into asserts.

You're probably running from the command line, since you're asking this question. If you're running from Visual Studio, the compiler is usually turned off, but you can run it from the menu. If you're running Dafny on rise4fun, then the compiler will run (and you will get any compiler error messages), provided there is a Main method in your program.