Question

What is the difference between function, method, function method, and function by method?

Answer

The names of these alternatives will be changing between Dafny 3 and Dafny 4:

• function (function method in Dafny 3) – is a non-ghost function
• ghost function (function in Dafny 3) – is a ghost function
• function by method is a ghost function with an alternate compilable (non-ghost) method body (cf. the reference manual section on function declarations)
• method declares a non-ghost method
• ghost method declares a ghost method, though this is almost always done using a lemma instead

Note that

• Methods may have side effects but may not be used in expressions.
• Functions may be used in expressions but may not have side effects.
• Methods do not have reads clauses; functions typically do.
• Non-ghost methods and non-ghost functions may not be used in ghost code.