How-to and FAQ Guide for Dafny users

This page is the table of contents for a compendium of mini-lessons on Dafny programming idioms, how to accomplish various programming tasks in Dafny, how to fix error messages, answers to FAQs or even just occasionally asked questions, and even information that you may not have asked yet, but you might.

These pages are not intended to be a reference manual or an organized tutorial for Dafny.

If you have questions that are not addressed here, be sure to communicate them to the Dafny team.

All content on one page

FAQs

Dafny language

• “How do I format a string?”
• “Where do I put the reads clause in a subset type?”
• “Can datatypes extend traits?”
• “What is the difference between a type and a newtype?”
• “Why can compiled modules contain but not import abstract modules?”
• “Why does Dafny need an obvious assert?”
• “Why do I need a witness clause when I define a subset type or newtype?”
• “Can I access the members of an outer module from its inner module?”
• “What is - on bitvectors?”
• “Is there a simple way to prove the termination of a recursive function?”
• “Is there a way to use methods within expressions?”
• “If I have an assertion about an object (of class type) and a loop that doesn’t mention (read, modify) the object, why does dafny fail to establish the assertion after the loop?”
• “I can assert a condition right before a return, so why does the postcondition fail to verify?
• “How can I combine sequences of different types?”
• “How do I disambiguate module names?
• “A function seems to work just once. How do I get it to apply a bunch of times?”
• “Why do nested modules not see the imports of their enclosing modules?”
• “Is there a way to test that two types are the same?”
• “When a lemma has multiple ensures clauses, I’m finding that they interact, when I expected them to be independent. For example, commenting out one of them can make another one not verify. How should I think about this?”
• “What is the difference between a lemma and a ghost method?”
• “In an invariant, I want to say that once a boolean variable that starts false is set to true, it remains true forever. Can I use old for this?”
• “When proving an iff (<==>), is there a nice way to prove this by proving each side of the implication separately without making 2 different lemmas?”
• “Is there a way to do partial application for functions?”
• “Why can a ghost const not be used as a witness? Does the compiler need to use the witness as an initial value?”
• “How do I use forall statements and expressions in a lemma?”
• “Is there any difference between a method without a modifies clause and a function method with a reads this clause? I know that the latter you can use in expressions, but otherwise. Is there anything the former can do that the latter can’t, for example?”
• “Dafny doesn’t like when a type and a module have the same name. How can I fix this?”
• “Is there a way to prevent ‘Warning: note, this forall statement has no body’ from occurring? I have a forall loop with no body that results in the lemma verifying, but if I add a body (even an empty body) the lemma doesn’t verify.”
• “Is there a way to disable termination checks for recursive predicate definitions that I know to be logically consistent?”
• “Is there a way to specify that all fields of an object, except a given one, don’t change?”
• “How do labels in preconditions work?”
• “Where are attributes documented?”
• “Is there a way to ask Dafny to die on its first verification failure?”
• “I can define a trait with some type parameters say trait Test<A, B, C>. When I use this trait is there a way to get Dafny to infer these types for me?”
• “Does Dafny have monadic error handling?”
• “What is the :- operator?”
• “How does :- work? I’m getting an unexpected failure.”
• “What is the meaning of and differences among ->, -->, ~>?”
• “What is the difference between function, method, function method, and function by method?”
• “Is it possible to restrict a type parameter to be a reference type? I see you can use T(!new) but I’m looking for the opposite.”
• “A seq is an object reference, right?”
• “How do I pattern match against a head and tail of a sequence or against a set?”
• “How do I create a new empty map (or set or sequence)?”
• “I have a module that exports a bunch of things. In another module I only need to use 1 thing. Is there a way to import only the thing that I want?”
• “What is the difference between modifies this, modifies this.x, and modifies this`x?
• “How does one define a record?”
• “What does forall v :: v in vals ==> false evaluate to if vals is non-empty?”
• “Why does Dafny complain about this use of a set constructor: set i: int | Contains(i)?”
• “What’s the syntax for paths in include directives? How do they get resolved?”
• “How do {:split_here} and {:focus} work to divide up a proof?”
• “How does one declare a type to have a default initial value, say a type tagged with {:extern}?’
• “A module A has names from an import opened or another module B, but if C imports A, it does not get those names. Please explain.”
• “Are there functional alternatives to recursive calls that are more efficient or use less stack space?”
• “How do I read a file as a string?”
• “Can I ask dafny to not check termination of a function?”
• “What does {:termination false} do on trait? It looks like it is required if I want to extend traits from other modules.”
• “How do I make Dafny termination checking happy with this pattern of mutual recursion?”
• “Can it be proved that a class instance is not an instance of a trait?”
• “Is there a nice way to turn a set into a seq?”
• “How do I declare a default value for a parameter of a method or function?”
• “I just realized that a function I was compiling had a type-error inside a match case. Instead of giving a compile error I was getting a redundant clause warning for the second case. What is the reason for this?”
• “Is there a way I can pass a variable with a generic type to a method with a concrete type?”
• “How can ghost code call methods with side effects?”
• “How do I create and use an iterator?
• “Can classes appear in specs?”
• “How do I write specifications for a lambda expression in a sequence constructor?”
• “I have a lemma and later an assert stating the postcondition of the lemma, but it fails to prove. Why and how do I fix it?”
• “Why can’t I write forall t: Test :: t.i == 1 for an object t?”
• “How do I say ‘reads if x then this`y else this`z’? Dafny complains about the ‘this’.”
• “How do I model extern methods that return objects?”
• “How do I tell Dafny that a class field may be updated?”
• “Why does Dafny not know this obvious property of maps?”

Dafny tools

• “Is there a Dafny style? and a Dafny linter (style checker and bad smell warnings)?
• “Is Dafny available as a library, to be called from other software?
• “How do I run boogie manually on the Dafny output?
• “Does Dafny verify methods in parallel?”
• “Is there a doc generator for Dafny?”
• “How can I improve automation and performance for programs with non-linear arithmetic?”
• “It looks like, when compiling to C#, my print statements don’t show up if I don’t have \n at the end of the string.”
• “Is there a standard library for Dafny?”
• “Why do I need to use an old Z3?”
• “How do I ask a question or file a problem report or make a suggestion about Dafny?”
• “Any plans to release the language server as a NuGet package? Seems like it’s not part of the Dafny release.”
• “What compiler target languages are in development?”

Errors

Also see the error catalog for a complete, searchable list of error messages with explanations.

• “‘z3’ cannot be opened because the developer cannot be verified.”
• “rbrace expected”
• “closeparen expected”
• “cannot establish the existence of LHS values that satisfy the such-that predicate”
• “type parameter 0 (K) passed to type A must support no references”
• “a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map<int, A>)”
• “name of datatype (String) is used as a function”
• “possible violation of function precondition for op(v)”
• “type ? does not have a member IsFailure”
• “value does not satisfy subset constraints of ?”
• “function precondition might not hold”
• “insufficient reads clause to invoke function”
• “Cannot export mutable field ‘x’ without revealing its enclosing class ‘A’”
• “this symbol not expected in Dafny”
• Prover error: Unexpected prover response (getting info about ‘unknown’ response): (:reason-unknown “Overflow encountered when expanding old_vector”)
• “Warning: File contains no code: …”
• “Duplicate name of import: …”
• “Warning: /!\ No terms found to trigger on.”
• “Error: value does not satisfy the subset constraints of ‘(seq<uint8>, Materials.EncryptedDataKey) -> seq<uint8>’ (possible cause: it may be partial or have read effects)”