Dafny Errors and Warnings

This page contains a catalog of the dafny tool’s Error and Warning messages, all in one long page to facilitate searching.

The title of each section is an error message. Each section contains example code that produces the error, which is then followed by explanation and references.

Italicized words in the given messages indicate variable content.

## Command-line Errors and Warnings

This section is a work in progress

## Parser Errors and Warnings

### Error: Duplicate declaration modifier: abstract

abstract abstract module M {}

No Dafny modifier, such as abstract, static, ghost may be repeated Such repetition would be superfluous even if allowed.

### Error: a decl cannot be declared ‘abstract’

module M {
abstract const c := 4
}

Only modules may be declared abstract.

### Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the ‘ghost’ keyword.

ghost function f(): int
{
42
} by method {
return 42;
}

### Error: decl cannot be declared ‘ghost’ (it is ‘ghost’ by default when using –function-syntax:3)

module {:options "--function-syntax:3"} M {
ghost function f(): int { 42 }
}

For versions prior to Dafny 4, the function keyword meant a ghost function and function method meant a non-ghost function. From Dafny 4 on, ghost function means a ghost function and function means a non-ghost function. See the discussion here for a discussion of options to control this feature.

### Error: a decl cannot be declared ‘ghost’

ghost module M {}

Only some kinds of declarations can be declared ghost, most often functions, fields, and local declarations. In the example, a module may not be ghost.

### Error: a decl cannot be declared ‘static’

static module M {}

Only some kinds of declarations can be declared ‘static’, most often fields, constants, methods, and functions, and only within classes. Modules and the declarations within them are already always static.

### **Warning: Attribute attribute is deprecated and will be removed in Dafny 4.0

method {:handle} m() {}

The {:handle} and {:dllimport} attributes are obsolete and unmaintained. They will be removed.

### Error: argument to :options attribute must be a literal string

module N { const opt := "--function-syntax:4" }
import opened N
module {:options opt} M{}

The value of an options attribute cannot be a computed expression. It must be a literal string.

### Error: cannot declare identifier beginning with underscore

const _myconst := 5
function m(): (_: int) {0}

User-declared identifiers may not begin with an underscore; such identifiers are reserved for internal use. In match statements and expressions, an identifier that is a single underscore is used as a wild-card match.

### Error: sorry, bitvectors that wide (number) are not supported

const b: bv2147483648

A bitvector type name is the characters ‘bv’ followed by a non-negative integer literal. However, dafny only supports widths up to the largest signed 32-bit integer (2147483647).

### Error: sorry, arrays of that many dimensions (number) are not supported

const a: array2147483648<int>

A multi-dimensional array type name is the characters ‘array’ followed by a positive integer literal. However, dafny only supports numbers of dimensions up to the largest signed 32-bit integer (2147483647). In practice (as of v3.9.1) dimensions of more than a few can take overly long to resolve (Issue #3180).

### Error: There is no point to an export declaration at the top level

export M
method M() {}

Although all top-level declarations are contained in an implicit top-level module, there is no syntax to import that module. Such an import would likely cause a circular module dependency error. If the implicit module cannot be imported, there is no point to any export declarations inside the implicit module.

### Error: expected either a ‘{‘ or a ‘refines’ keyword here, found token

module M {}
module N refine M {}

The syntax for a module declaration is either module M { ... } or module M refines N { ... } with optional attributes after the module keyword. This error message often occurs if the refines keyword is misspelled.

### Error: no comma is allowed between provides and reveals and extends clauses in an export declaration

module M {
export A reveals b, a, reveals b
export B reveals b, a, provides b
export C provides b, a, reveals b
export D provides b, a, provides b
const a: int
const b: int
}

An export declaration consists of one or more reveals, provides, and extends clauses. Each clause contains a comma-separated list of identifiers, but the clauses themselves are not separated by any delimiter. So in the example above, the comma after a is wrong in each export declaration. This mistake is easy to make when the clauses are on the same line.

### Error: fields are not allowed to be declared at the module level; instead, wrap the field in a ‘class’ declaration

module M {
var c: int
}

var declarations are used to declare mutable fields of classes, local variables in method bodies, and identifiers in let-expressions. But mutable field declarations are not permitted at the static module level, including in the (implicit) toplevel module. Rather, you may want the declaration to be a const declaration or you may want the mutable field to be declared in the body of a class.

### Error: in refining a datatype, the ‘…’ replaces the ‘=’ token and everything up to a left brace starting the declaration of the body; only members of the body may be changed in a datatype refinement

abstract module M { datatype D = A | B }
module N refines M { datatype D = ... Y | Z }

There are limitations on refining a datatype, namely that the set of constructors cannot be changed. It is only allowed to add members to the body of the datatype.

### Error: mutable fields are not allowed in value types

datatype D = A | B  { var c: D }

The var declaration declares a mutable field, which is only permitted within classes, traits and iterators. const declarations can be members of value-types, such as datatypes.

### Error: a const field should be initialized using ‘:=’, not ‘=’

const c: int = 5

Dafny’s syntax for initialization and assignment uses :=, not =. In Dafny = is used only in type definitions.

### Error: a const declaration must have a type or a RHS value

const i

A const declaration needs its type indicated by either an explicit type or a right-hand-side expression, whose type is then the type of the declared identifier. So use syntax either like const i: int or const i:= 5 (or both together).

### Error: in refining a newtype, the ‘…’ replaces the ‘=’ token and everything up to the left brace starting the declaration of the newtype body (if any); a newtype refinement may not change the base type of the newtype

abstract module M { newtype T = int }
module N refines M { newtype T = ... int }

There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an opaque type into a newtype, however.

### Error: formal cannot be declared ‘ghost’ in this context

predicate m(i: int): (ghost r: bool) { 0 }

The output of a predicate or function cannot be ghost. It is implicitly ghost if the function is ghost itself.

### Error: formal cannot be declared ‘ghost’ in this context

ghost function m(ghost i: int): int {
42
}

If a method, function, or predicate is declared as ghost, then its formal parameters may not also be declared ghost. Any use of this construct will always be in ghost contexts.

### Error: formal cannot be declared ‘new’ in this context

method m(i: int) returns (new r: int) {}

The new modifier only applies to input parameters.

### Error: formal cannot be declared ‘nameonly’ in this context

method m(i: int) returns (nameonly r: int) {}

The nameonly modifier only applies to input parameters.

### Error: formal cannot be declared ‘older’ in this context

method m(i: int) returns (older r: int) {}

The older modifier only applies to input parameters.

### Error: a mutable field must be declared with a type

class A {
var f
const g := 5
}

Because a mutable field does not have initializer, it must have a type (as in var f: int). const declarations may have initializers; if they do they do not need an explicit type.

### Error: a mutable field may not have an initializer

class A {
var x: int := 6
var y: int, x: int := 6, z: int
}

Dafny does not allow field declarations to have initializers. They are initialized in constructors. Local variable declarations (which also begin with var) may have initializers.

### Error: invalid formal-parameter name in datatype constructor

datatype D = Nil | D(int: uint8)

Datatype constructors can have formal parameters, declared with the usual syntax: ‘name: type’. In datatype constructors the ‘name :’ is optional; one can just state the type. However, if there is a name, it may not be a typename, as in the failing example above. The formal parameter name should be a simple identifier that is not a reserved word.

### Error: use of the ‘nameonly’ modifier must be accompanied with a parameter name

datatype D = D (i: int, nameonly int) {}

The parameters of a datatype constructor do not need to have names – it is allowed to just give the type. However, if nameonly is used, meaning the constructor can be called using named parameters, then the name must be given, as in datatype D = D (i: int, nameonly j: int) {}

More detail is given here.

### Error: iterators don’t have a ‘returns’ clause; did you mean ‘yields’?

iterator Count(n: nat) returns (x: nat) {
var i := 0;
while i < n {
x := i;
yield;
i := i + 1;
}
}

An iterator is like a co-routine: its control flow produces (yields) a value, but the execution continues from that point (a yield statement) to go on to produce the next value, rather than exiting the method. To accentuate this difference, a yield statement is used to say when the next value of the iterator is ready, rather than a return statement. In addition, the declaration does not use returns to state the out-parameter, as a method would. Rather it has a yields clause. The example above is a valid example if returns is replaced by yields.

### Error: type-parameter variance is not allowed to be specified in this context

type List<T>
method m<+T>(i: int, list: List<T>) {}
method m<T,-U>(i: int, list: List<T>) {}

Type-parameter variance is specified by a +, -, * or ! before the type-parameter name. Such designations are allowed in generic type declarations but not in generic method, function, or predicate declarations.

### Error: unexpected type characteristic: ‘000’ should be one of == or 0 or 00 or !new

type T(000)

Type parameters, indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. The currently defined type parameters are designated by == (equality-supporting), 0 (auto-initializable), 00 (non-empty), and !new (non-reference).

### Error: extra comma or missing type characteristic: should be one of == or 0 or 00 or !new

type T(0,,0)

Type parameters, indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. The currently defined type parameters are designated by == (equality-supporting), 0 (auto-initializable), 00 (non-empty), and !new (non-reference).

### Error: illegal type characteristic: ‘token’ should be one of == or 0 or 00 or !new

type T(X)

Type parameters, indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. The currently defined type parameters are designated by == (equality-supporting), 0 (auto-initializable), 00 (non-empty), and !new (non-reference).

### Warning: the old keyword ‘colemma’ has been renamed to the keyword phrase ‘greatest lemma’

colemma m() ensures true {}

The adjectives least and greatest for lemmas and functions are more consistent with the nomenclature for coinduction.

### Warning: the old keyword phrase ‘inductive lemma’ has been renamed to ‘least lemma’

inductive lemma m() ensures true {}

The adjectives least and greatest for lemmas and functions are more consistent with the nomenclature for coinduction.

### Error: constructors are allowed only in classes

module M {
constructor M() {}
}

Constructors are methods that initialize class instances. That is, when a new instance of a class is being created, using the new object syntax, some constructor of the class is called, perhaps a default anonymous one. So constructor declarations only make sense within classes.

### Error: a method must be given a name (expecting identifier)

method {:extern "M"} (i: int) {}

A method declaration always requires an identifier between the method keyword and the ( that starts the formal parameter list. This is the case even when, as in the example above, a name is specified using :extern. The extern name is only used in the compiled code; it is not the name used to refer to the method in Dafny code

### Error: type of k can only be specified for least and greatest lemmas

lemma b[nat](i: int) { }

Least and greatest lemmas and predicates have a special parameter named k. Its type is specified in square brackets between the lemma/predicate name and the rest of the signature. The type may be either nat or ORDINAL. But this type is specified only for least and greatest constructs.

### Error: constructors cannot have out-parameters

class C {
constructor (i: int) returns (j: int) {}
}

Constructors are used to initalize the state of an instance of a class. Thus they typically set the values of the fields of the class instance. Constructors are used in new object expressions, which return a reference to the newly constructed object (as in new C(42)). There is no syntax to receive out-parameter values of a constructor and they may not be declared. (This is similar to constructors in other programming languages, like Java.)

### Error: A ‘reads’ clause that contains ‘*’ is not allowed to contain any other expressions

const a: object;
function f(): int
{
0
}

A reads clause lists the objects whose fields the function is allowed to read (or expressions containing such objects). reads * means the function may read anything. So it does not make sense to list * along with something more specific. If you mean that the function should be able to read anything, just list *. Otherwise, omit the * and list expressions containing all the objects that are read.

### Error: out-parameters cannot have default-value expressions

method m(i: int) returns (j: int := 0) { return 42; }

Out-parameters of a method are declared (inside the parentheses after the returns keyword) with just an identifier and a type, separated by a colon. No initializing value may be given. If a default value is needed, assign the out-parameter that value as a first statement in the body of the method.

### Error: set type expects only one type argument

const c: set<int,bool>

A set type has one type parameter, namely the type of the elements of the set. The error message states that the parser sees some number of type parameters different than one. The type parameters are listed in a comma-separated list between < and >, after the type name.

### Error: iset type expects only one type argument

const c: iset<int,bool>

A iset type has one type parameter, namely the type of the elements of the set. The error message states that the parser sees some number of type parameters different than one. The type parameters are listed in a comma-separated list between < and >, after the type name.

### Error: multiset type expects only one type argument

const c: multiset<int,bool>

A multiset type has one type parameter, namely the type of the elements of the multiset. The error message states that the parser sees some number of type parameters different than one. The type parameters are listed in a comma-separated list between < and >, after the type name.

### Error: seq type expects only one type argument

const c: seq<int,bool>
const s := seq<int,int>(3, i=>i+1)

A seq type has one type parameter, namely the type of the elements of the sequence. The error message states that the parser sees some number of type parameters different than one. The type parameters are listed in a comma-separated list between < and >, after the type name.

### Error: map type expects two type arguments

const m: map<int,bool,string>

A map type has two type parameters: the type of the keys and the type of the values. The error message states that the parser sees some number of type parameters different than two.

### Error: imap type expects two type arguments

const m: imap<int,bool,string>

A imap type has two type parameters: the type of the keys and the type of the values. The error message states that the parser sees some number of type parameters different than two.

### Error: arrow-type arguments may not be declared as ‘ghost’

const f: (ghost int, bool) -> int

Arrow types are the types of functions in Dafny. They are designated with the arrow syntax, as shown in the example, except that the types used cannot be declared as ghost.

### Error: a ‘by method’ implementation is not allowed on a twostate what

class Cell { var data: int  constructor(i: int) { data := i; } }
twostate predicate Increasing(c: Cell)
{
old(c.data) <= c.data
} by method {
return old(c.data) <= c.data;
}

Two state functions and predicates are always ghost and do not have a compiled representation. Such functions use values from two different program (heap) states, which is not something that can be implemented (at least with any degree of good performance) in conventional programming languages.

Because there is no feasible compiled verion of a two-state function, it cannot have a by method block (which is always compiled).

### Error: a ‘by method’ implementation is not allowed on an extreme predicate

least predicate g() { 42 } by method { return 42; }

Least and greatest predicates are always ghost and do not have a compiled representation, so it makes no sense to have a by method alternative implementation.

### Error: to use a ‘by method’ implementation with a what, declare id using what, not ‘what method’

function method m(): int {
42
} by method {
return 42;
}

by method constructs combine a ghost function (or predicate) with a non-ghost method. The two parts compute the same result, and are verified to do so. Uses of the function are verified using the function body, but the method body is used when the function is compiled.

Thus the function part is always implicitly ghost and may not be explicitly declared ghost.

### Error: a adjective what is supported only as ghost, not as a compiled what

twostate function method m(): int {
42
}

The twostate, least, and greatest functions and predicates are always ghost and cannot be compiled, so they cannot be declared as a function method (v3 only).

### Error: a what is always ghost and is declared with ‘what‘

module {:options "--function-syntax:experimentalPredicateAlwaysGhost"} M {
predicate method p() { true }
}

This error only occurs when the experimentalPredicateAlwaysGhost option is chosen. It indicates that predicates are always ghost and cannot be declared with the (Dafny 3) syntax predicate method.

• If you intend to predicate to be ghost, remove method.
• If you intend the predicate to be non-ghost, you either cannot use experimentalPredicateAlwaysGhost or you should use function with a bool return type instead of predicate

### Error: the phrase ‘what method’ is not allowed when using –function-syntax:4; to declare a compiled function, use just ‘function’

module {:options "--function-syntax:4"} M {
function method f(): int { 42 }
}

In Dafny 4 on, the phrases function method and predicate method are no longer accepted. Use function for compiled, non-ghost functions and ghost function for non-compiled, ghost functions, and similarly for predicates. See the documentation here.

### Error: there is no such thing as a ‘ghost what method’

module {:options "--function-syntax:experimentalDefaultGhost"} M {
ghost function method f(): int { 42 }
}

Pre-Dafny 4, a function method and a predicate method are explicitly non-ghost, compiled functions, and therefore cannot be declared ghost as well. If indeed the function or predicate is intended to be ghost, leave out method; if it is intended to be non-ghost, leave out ghost.

From Dafny 4 on, a ghost function is declared ghost function and a non-ghost function is declared function and there is no longer any declaration of the form function method, and similarly for predicates.

### Error: a what must be declared as either ‘ghost what’ or ‘what method’ when using –function-syntax:migration3to4

module {:options "--function-syntax:migration3to4"} M {
function f(): int { 42 }
}

This error occurs only when using migration3to4. With this option, ghost functions are declared using ghost function and compiled functions using function method. Change function in the declaration to one of these.

### Error: ‘decreases’ clauses are meaningless for least and greatest predicates, so they are not allowed

least predicate m(i: int)
decreases i
{
true
}

Least and greatest predicates are not checked for termination. In fact, unbounded recursion is part of being coinductive. Hence decreases clauses are inappropriate and not allowed.

### Error: name return type should be bool, got type

predicate b(): (r: boolean) { 4 }

A predicate is a function that returns bool. The return type here is something else. If you mean to have a non-bool return type, use function instead of predicate.

### Error: _name_s do not have an explicitly declared return type; it is always bool. Unless you want to name the result: ‘: (result: bool)’

predicate p(): bool { true }

A predicate is simply a function that returns a bool value. Accordingly, the type is (required to be) omitted, unless the result is being named. So predicate p(): (res: bool) { true } is permitted

### Error: A ‘*’ expression is not allowed here

function m(i: int): int
decreases *
{
42
}

A method or loop with a decreases * clause is not checked for termination. This is only permitted for non-ghost methods and loops.

### Error: A ‘*’ frame expression is not permitted here

iterator Gen(start: int) yields (x: int)
{
var i := 0;
while i < 10 invariant |xs| == i {
x := start + i;
yield;
i := i + 1;
}
}

A reads * clause means the reads clause allows the functions it specifies to read anything. Such a clause is not allowed in an iterator specification.

### Error: invalid statement beginning here (is a ‘label’ keyword missing? or a ‘const’ or ‘var’ keyword?)

method m(n: nat) {
x: while (0 < n) { break x; }
}

In this situation the parser sees the identifier (x) and the following colon. This is not a legal start to a statement. Most commonly either

• a var or const keyword is missing, and the x: is the beginning of a declaration, or
• a label keyword is missing and the identifier is the label for the statement that follows. (The second error is somewhat common because in C/C++ and Java, there is no keyword introducing a label, just the identifier and the colon.)

### Error: An initializing element display is allowed only for 1-dimensional arrays

method m() {
var a := new int[2,2] [1,2,3,4];
}

One-dimensional arrays can be initiallized like var s := new int[][1,2,3,4];, but multi-dimensional arrays cannot. The alternatives are to initialize the array in a loop after it is allocated, or to initialize with a function, as in var a:= new int[2,2]((i: int, j: int)=>i+j).

### Error: a local variable should be initialized using ‘:=’, ‘:-‘, or ‘:|’, not ‘=’

method m() {
var x = 5;
}

Local variables are initialized with := (and sometimes with :- or :|), but not with =. In Dafny = is used only in type definitions.

### Error: LHS of assign-such-that expression must be variables, not general patterns

datatype D = D(x: int, y: int)
method m() {
var D(x,y) :| x + y == 5;
}

The :| syntax is called assign-such-that: the variables on the left-hand-side are initiallized or assigned some non-deterministic values that satisfy the predicate on the right-hand-side.

However, Dafny only allows a list of simple variables on the left, not datatype deconstructor patterns, as seen here.

### Error: ‘modifies’ clauses are not allowed on refining loops

Refining statements, including loops, are deprecated.

### Error: Expected ‘to’ or ‘downto’

method m(n: nat) {
for i := n DownTo 0 {}
}

A for loop can express a computation to be performed for each value of a loop index. In Dafny, the loop index is an int-based variable that is either

• incremented up from a starting value to just before an ending value: 3 to 7 means 3, 4, 5, and 6
• or decremented from just below a starting value down to an ending value: 7 downto 3 means 6, 5, 4, and 3.

The contextual keywords to and downto indicate incrementing and decrementing, respectively. No other words are allowed here, including writing them with different case.

These two words have special meaning only in this part of a for-loop; they are not reserved words elsewhere. That is, the code

method m() {
var to: int := 6;
var downto: int := 8;
for to := to to downto {}
}

is legal, but not at all recommended.

### Error: A ‘decreases’ clause that contains ‘*’ is not allowed to contain any other expressions

method f(n: int) returns (r: int)
decreases *, n
{
r := if n == 0 then n else -1-f(n-1);
}

A decreases clause provides a metric that must decrease from one call to the next, in order to assure termination of a sequence of recursive calls. In loops it assures termination of the loop iteration.

decreases * means to skip the termination check. So it does not make sense to both list a metric and to list ‘*’. Use one or the other.

### Error: a forall statement with an ensures clause must have a body

module  M {
predicate f(i: int) { true }
method  m(a: seq<int>) {
forall i | 0 <= i < 10
ensures f(i)
}
}

A forall statement without a body is like an assume statement: the ensures clause is assumed in the following code. Assumptions like that are a risk to soundness because there is no check that the assumption is true. Thus in a context in which open assumptions are not allowed, body-less forall statements are also not allowed.

### Error: the main operator of a calculation must be transitive

lemma abs(a: int, b: int, c: int)
ensures a + b + c == c + b + a
{
calc != {
a + b + c;
a + c + b;
c + a + b;
}
}

A calc statement contains a sequence of expressions interleaved by operators. Such a sequence aids the verifier in establishing a desired conclusion. But the sequence of operators must obey certain patterns similar to chaining expressions. In this case a default operator is stated (the != between calc and {). This default operator is the implicit operator between each consecutive pair of expressions in the body of the calc statement.

But the operator has to be transitive: != is not allowed; ==, <, <=, ‘>’ and ‘>=’ are allowed.

### Error: this operator cannot continue this calculation

lemma abs(a: int, b: int, c: int)
ensures a + b + c == c + b + a
{
calc {
a + b + c;
!=
a + c + b;
!=
c + a + b;
}
}

A calc statement contains a sequence of expressions interleaved by operators. Such a sequence aids the verifier in establishing a desired conclusion. But the sequence of operators must obey certain patterns similar to chaining expressions.

In particular, this error message is complaining that it sees an unacceptable operator. In this case, the reason is that the sequence may contain only one != operator; another reason causing this message would be a combination of < and > operators.

### Error: a calculation cannot end with an operator

lemma abs(a: int, b: int, c: int)
ensures a + b + c == c + b + a
{
calc {
a + b + c;
==
}
}

A calc statement contains a sequence of expressions interleaved by operators. Such a sequence aids the verifier in establishing a desired conclusion. But the sequence must begin and end with (semicolon-terminated) expressions.

This error message is complaining that it sees an operator ending the sequence. This may be because there is no following expression or that the parser does not recognize the material after the last operator as a legal ending expression.

### Error: Ambiguous use of ==> and <==. Use parentheses to disambiguate.

const b := true ==> false <== true;

The ==> and <== operators have the same precedence but do not associate with each other. You must use parentheses to show how they are grouped. Write the above example as either (true ==> false) <== true or true ==> (false <== true).

In contrast, p ==> q ==> r is p ==> (q ==> r) and p <== q <== r is (p <== q) <== r.

### Error: Ambiguous use of && and ||. Use parentheses to disambiguate.

const b := true && false || true

The && and || operators have the same precedence but do not associate with each other. You must use parentheses to show how they are grouped. Write the above example as either (true && false) || true or true && (false || true).

### Error: chaining not allowed from the previous operator

const c := 1 in {1} == true

Chained operations are a sequence of binary operations without parentheses: a op b op c op d op e. But there are limitations on which operators can be in one chain together.

In particular, the relational operators in and !in may not be part of a chain. Use parentheses as necessary to group the operations.

### Error: a chain cannot have more than one != operator

const c := 1 != 2 != 3

Chained operations are a sequence of binary operations without parentheses: a op b op c op d op e. But there are limitations on which operators can be in one chain together.

In particular for this error message, one cannot have chains that include more than one != operator.

### Error: this operator chain cannot continue with an ascending operator

const c := 4 > 3 < 2

Chained operations are a sequence of binary operations without parentheses: a op b op c op d op e. But there are limitations on which operators can be in one chain together.

In particular for this error message, one cannot have chains that include both less-than operations (either < or <=) and greater-than operations (either > or >=).

### Error: this operator chain cannot continue with a descending operator

const c := 2 < 3 > 4

Chained operations are a sequence of binary operations without parentheses: a op b op c op d op e. But there are limitations on which operators can be in one chain together.

In particular for this error message, one cannot have chains that include both less-than operations (either < or <=) and greater-than operations (either > or >=).

### Error: can only chain disjoint (!!) with itself

const c := 2 < 3 !! 4

Chained operations are a sequence of binary operations without parentheses: a op b op c op d op e. But there are limitations on which operators can be in one chain together.

In particular for this error message, a disjoint operator (!!) can appear in a chain only if all the operators in the chain are disjoint operators.

As described here, a !! b !! c !! d means that a, b, c, and d are all mutually disjoint (which is a different rewriting of the chain than for other operations).

### Error: this operator cannot be part of a chain

const c := 2 < 3 in 4

The operators in and !in are relational operators, but they may not occur in a chain. Use parentheses if necessary. An expression like the above is not type-correct in any case.

### Error: invalid relational operator

const s : set<int>
const r := s ! s

The parser is expecting a relational expression, that is, two expressions separated by a relational operator (one of ==, !=, >, >=, <, <=, !!, in, !in). But the parser saw just a ! , which could be the beginning of !=, !!, or !in, but is not continued as such. So perhaps there is extraneous white space or something else entirely is intended.

### Error: invalid relational operator (perhaps you intended "!!" with no intervening whitespace?)

const s : set<int>
const r := s ! ! s

The parser is expecting a relational expression, that is, two expressions separated by a relational operator (one of ==, !=, >, >=, <, <=, !!, in, !in). But the parser saw two ! separated by white space. This is possibly meant to be a !! operator, but it could also just be an illegal expression.

### Error: Ambiguous use of &, |, ^. Use parentheses to disambiguate.

const i: int := 5 | 6 & 7

The bit-operators &, |, and ^ have the same precedence but do not associate with each other. So if they are used within the same expression, parentheses have to be used to show how they are grouped. The above example should be written as either (5 | 6) & 7 or 5 | (6 & 7).

### Error: too many characters in character literal

const c := '🚀';

A character literal can only contain a single value of the built-in char type. When –unicode-char is disabled, the char type represents UTF-16 code units, so this means a character literal can only contain a character that can be represented with a single such unit, i.e. characters in the Basic Multilingual Plane. The rocket ship emoji above, however, is encoded with two surrogate code points.

This can be fixed by enabling the –unicode-char mode, as that defines char as any Unicode scalar value, but be aware that it may change the meaning of your program.

More detail is given here and here.;

### Error: binding not allowed in parenthesized expression

method m() {
var c := ( 4 := 5 );
}

A binding of the form x := y is used in map-display expresions, in which case they are enclosed in square brackets, not parentheses. The above example should be var c := [ 4 := 5 ]

### Error: A forming expression must be a multiset

A set/iset/multiset display expression can have two forms. One form is a list of values enclosed by curly braces: var c := multiset{1,2,2,3}. The other appears as a conversion operation: var c := multiset(s). However, this second form can only be used to convert a set to a multiset.

In the current parser, however, this error message is unreachable. The tests that check for this error case are already known to be false by previous testing.

### Error: a map comprehension with more than one bound variable must have a term expression of the form ‘Expr := Expr’

const s := map x, y  | 0 <= x < y < 10 :: x*y

A map comprehension defines a map, which associates a value with each member of a set of keys. The full syntax for a map comprehension looks like map x | 0 <= x < 5:: x*2 => x*3 which maps the keys 0, 2, 4, 6, 8 to the values 0, 3, 6, 9, 12 respectively.

One can abbreviate the above syntax to expressions like map x | 0 <= x < 5 :: x*3, which is equivalent to map x | 0 <= x < 5 :: x => x*3. The missing expression before the => is just the declared identifier.

One can also have multiple variables involved as in map x, y | 0 < x < y < < 5 :: 10*x+y => 10*y+x, which defines the mappings (12=>21, 13=>31, 14=>41, 23=>32, 24=>42, 34=>43).

But when there are multiple variables, one cannot abbreviate the => syntax with just its right-hand expression, becuase it is not clear what the left-hand expression should be.

Rewrite the failing example above as const s := map x, y | 0 <= x < y < 10 :: f(x,y) => x*y for some f(x,y) that gives a unique value for each pair of x,y permitted by the range expression (here 0 <= x < y < 10 ).

### Error: a variable in a let expression should be initialized using ‘:=’, ‘:-‘, or ‘:|’, not ‘=’

method m() {
var x := var y = 5; y*y;
}

Like local variables, let variables are initialized with := (and sometimes with :- or :|), but not with =. In Dafny = is used only in type definitions.

### Error: LHS of let-such-that expression must be variables, not general patterns

datatype Data = D(i: int, j: int)
const c: int := var Data(d,dd) :| d == 10 && dd == 11; d

The let-such-that expression initializes a variable to some value satisfying a given condition. For example, one might write const cc := var x: int :| x <= 10; x, where cc would get some value x satisfying x < 10.

For simplicity, however, Dafny requires the variables being initialized to be simple names, not patterns.

### Error: ‘:-‘ can have at most one left-hand side

datatype Outcome<T> =
| Success(value: T)
| Failure(error: string)
{ predicate IsFailure() { this.Failure? }
function PropagateFailure<U>(): Outcome<U>
requires IsFailure()
{ Outcome<U>.Failure(this.error) // this is Outcome<U>.Failure(...)
}

function Extract(): T requires !IsFailure() { this.value }
}

function m(): Outcome<int> { Outcome<int>.Success(0) }
function test(): Outcome<int> {
var rr, rrr :- m(), 44; Outcome.Success(1)
}

Within a function, the :- operator is limited to a most one left-hand-side and exactly one-right-hand-side.

### Error: ‘:-‘ must have exactly one right-hand side

datatype Outcome<T> =
| Success(value: T)
| Failure(error: string)
{ predicate IsFailure() { this.Failure? }
function PropagateFailure<U>(): Outcome<U>
requires IsFailure()
{ Outcome<U>.Failure(this.error) // this is Outcome<U>.Failure(...)
}

function Extract(): T requires !IsFailure() { this.value }
}

function m(): Outcome<int> { Outcome<int>.Success(0) }
function test(): Outcome<int> {
var rr :- m(), 44; Outcome.Success(1)
}

This error only occurs when using the elephant operator :- in conjunction with failure-compatible types and in the context of a let-or-fail expression, as in the body of test() in the example above.

In contrast to the let expression (:=), which allows multiple parallel initializations, the let-or-fail expression (:-) is implemented to only allow at most a single left-hand-side and a single-right-hand-side.

### Error: a set comprehension with more than one bound variable must have a term expression

const s := set x, y  | 0 <= x < y < 10

A set comprehension (1) declares one or more variables, (2) possibly states some limits on those variables, and (3) states an expression over those variables that are the values in the set.

If there is no expression, then the expression is taken to be just the one declared variable. For instance one could write set b: bool, which is equivalent to set b: bool :: b and would be the set of all bool values. Another example is set x: nat | x < 5, which is equivalent to set x: nat | x < 5:: x and would be the set {0, 1, 2, 3, 4}.

But if more than one variable is declared, then there is no natural implicit expression to fill in after the :: if it is omitted, so some expression is required. The failing example above, for example, might use the expression x * y, as in set x, y | 0 <= x < y < 10 :: x * y, or any other expression over x and y.

### Error: invalid name after a ‘.’

This error message is not reachable in current Dafny. If it occurs, please report an internal bug (or obsolete documentation).

### Error: incorrectly formatted number

This error can only result from an internal bug in the Dafny parser. The parser recognizes a legitimate sequence of digits or sequence of hexdigits or a decimal number and then passes that string to a libary routine to create a BigInteger or BigDecimal. Given the parser logic, that parsing should never fail.

### Error: Malformed template pragma: #source

const s := @"
#line S
"

This pragma syntax is no longer supported. If this message is seen, please report it to the Dafny development team. The Dafny scanner once supported pragmas of the form #line <lineno> <filename>, with the filename optional. This message indicates that the pragma was not readable, most likely because the line number was not a parsable numeral.

### Error: Unrecognized pragma: #source

const s := @"
# I love hashes
"

This pragma syntax is no longer supported. If this message is seen, please report it to the Dafny development team. The Dafny scanner saw a pragma – the first character of the line is a # character. But it is not one that the scanner recognizes. The only pragma ever recognized was #line.

## Name and Type Resolution Errors and Warnings

### Warning: timeLimitMultiplier annotation overrides timeLimit annotation

method {:timeLimitMultiplier 10} {:timeLimit 5} m() {}

The {:timeLimitMultiplier n} attribute tells the prover to use a time limit that is the given number times the time limit otherwise specified by the options. The {:timeLimit n} attribute simply sets a new value for the time limit. It does not make sense to have both attributes on the same declaration. One or the other should be removed. If they are both present, just the {:timeLimitMultiplier} is used.

### Warning: Argument to ‘old’ does not dereference the mutable heap, so this use of ‘old’ has no effect

method m(i: int)
{
var j: int;
j := 1;
label L:
j := 2;
ghost var k := old@L(j);
}

The old function, used in specifications and ghost code, indicates that the argument (an expression) is to be evaluated in some previous heap state. So if the argument does not depend on the heap, the old has no effect and is likely to lead to misunderstanding. Consequently, Dafny warns against doing so. For example, it has no effect to apply old to a local variable; instead one should capture the value of the local variable in a previous state using an otherwise unused ghost variable.

### Warning: _item_s given as :induction arguments must be given in the same order as in the quantifier; ignoring attribute

predicate g(i: int, j: int)
function f(): int
ensures forall i: int, j: int {:induction j,i} | true :: g(i,j)
{ 0 }

The {:induction} attribute gives some guidance to the prover as to how to construct the induction argument that proves the lemma. The heuristics that infer an induction proof require that the arguments of the attribute be in the same order as the bound variables of the quantifier. If not, the :induction attribute is ignored.

### Warning: lemma parameters given as :induction arguments must be given in the same order as in the lemma; ignoring attribute

lemma {:induction j,i} m(i: int, j: int) ensures i + j == j + i {}

The {:induction} attribute gives some guidance to the prover as to how to construct the induction argument that proves the lemma. The heuristics that infer an induction proof require that the arguments of the attribute be in the same order as the parameters of the lemma. If not, the :induction attribute is ignored.

### Warning: invalid :induction attribute argument; expected what; ignoring attribute

lemma {:induction 42} m(i: int, j: int) ensures i + j == j + i {}

The arguments of the :induction attribute can be any of the lemma parameters (for a lemma) or bound quantifiers (for a quantifier expression), the this keyword, or true or false.

### Warning: Constructor name ‘pattern’ should be followed by parentheses

datatype D = A | B

method m(d: D) {
match d {
case A => return;
case B() => return;
}
}

The pattern following a case keyword can be a constructor possibly without arguments or it can be new variable to be bound to the match expression. A parameter-less costructor may be written without parentheses. A simple identifier that happens to be a constructor of right type will be matched in preference to a new bound identifier.

This can lead to surprises if there is a matching constructor that the writer or the reader of the software is unaware of. So it is useful to always write constructors with parentheses, to visually distinguish them from simple identifiers.

The --warn-missing-constructor-parentheses option will warn if a constructor is used without parentheses. The solution is to either add parentheses (if a constructor is intended) or rename the identifier (if a fresh bound identifier is intended).

### Warning: unusual indentation in what (which starts at location); do you perhaps need parentheses?

function f(b: bool): bool
{
b &&
b ==> b // this parses as (b &&b) ==> b, but reads as b && (b ==> b)
}

Long expressions are best split up across multiple lines; readers often use indentation as a guide to the nesting of subexpressions. For example, parallel conjuncts or disjuncts may be written with the same indentation. This warning occurs when the observed indentation is likely to cause a misunderstanding of the code, particularly of the precedence of operations. It is suggested to use parentheses or to redo the indentation to make the structure of the expression clearer.

### Warning: unusual indentation in what (which ends at location); do you perhaps need parentheses?

function f(b: bool): bool
{
b ==> b &&
b          // this parses as b ==> (b && b), but reads as (b ==> b) && b
}

Long expressions are best split up across multiple lines; readers often use indentation as a guide to the nesting of subexpressions. For example, parallel conjuncts or disjuncts may be written with the same indentation. This warning occurs when the observed indentation is likely to cause a misunderstanding of the code, particularly of the precedence of operations. It is suggested to use parentheses or to redo the indentation to make the structure of the expression clearer.

### Error: Cannot use /runAllTests on a program with a main method

This error message when using dafny test and in the situation where a Main method is already present in the program.
dafny test synthesizes a Main method that calls all the test routines, which then conflicts with the existing Main method. (The /runAllTests option has been replaced by dafny test.)

### Error: Methods with the {:test} attribute can have at most one return value

method {:test} m(i: int) returns (j: int, k: int)
{
j, k := 0,0;
}

This error only occurs when using dafny test. That command executes all methods attributed with {:test}, but such test methods are limited to methods with only one output parameter. This is purely an implementation limitation. (cf. Issue 3387)

### Warning: The kind clause at this location cannot be compiled to be tested at runtime because it references ghost state.

method {:extern} m(i: int, ghost j: int)
requires j == 1

The --test-assumptions option inserts tests of various contracts and implicit assumptions in a Dafny method, such as the requires and ensures clauses. However, because these inserted tests are compiled into the target program as runtime checks, they cannot refer to any ghost variables. (This mechanism implements Dafny’s runtime-assertion checking.)

### Warning: Internal: no wrapper for name

This message indicates a bug within the dafny tool. Please report the program that triggered the message to the Github issues site.

### Warning: No :test code calls name

This warning indicates that some method marked with {:extern} is not called by any method marked with {:test}. The intention is to check coverage of the programmed unit tests. The warning only appears when using /testContracts:TestedExterns with the legacy CLI. It is likely to be removed in a future version of dafny.

### Error: :print attribute is not allowed on functions

function {:print} f(): int { 0 }

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. Functions, whether ghost or compiled, are intended to have no side-effects at all. Thus Dafny forbids (ghost or compiled) functions from declaring that they have a print side-effect (whether or not print effects are being tracked with --track-print-effects).

### Error: :print attribute is not allowed on ghost methods

ghost method {:print} f() { }

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. A program’s ghost code is not allowed to modify the actual execution of a program. Thus ghost code should not contain print statements. So Dafny forbids ghost methods from declaring that they have a print side-effect (whether or not print effects are being tracked with --track-print-effects).

### Error: not allowed to override a non-printing method with a possibly printing method (name)

trait T {
method m()
}

class C extends T {
method {:print} m() {}
}

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. If a trait declares a method without a {:print} attribute, then any implementation of that method may not do any printing, as it must obey the trait’s specification. Thus a class implementing that method by an override cannot declare the method as possibly printing something, by giving it a {:print} attribute — even if it does not actually do any printing.

### Error: :print attribute does not take any arguments

method {:print 42} f() { }

The {:print} attribute is used to mark methods that have a side-effect of printing something. No arguments to the attribute are needed or allowed.

### Error: a function-by-method is not allowed to use print statements

function f(): int {42 }
by method {
print "I'm here\n";
return 42;
}

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. Functions, whether ghost or compiled, are intended to have no side-effects at all. A function-by-method has a method body that is intended to be a compiled way of computing what the function body expresses. But as a function may not have side-effects, the method body should not have any print statements.

This tracking of print statements (and the forbidding of them by this error message) only happens when the --track-print-effects option is enabled; the option is disabled by default.

### Error: to use a print statement, the enclosing method must be marked with {:print}

method m() { print 42; }

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. So a method that prints something (even transitively) should be marked with {:print}. This error indicates that such an attribute is missing – either add the attribute or remove the print statement.

This tracking of print statements (and thus the possibility of this error message) only happens when the --track-print-effects option is enabled; the option is disabled by default.

### Error: a function-by-method is not allowed to call a method with print effects

function m(): int { 42 }
by method { p(); return 42; }

method {:print} p() {}

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. Functions, whether ghost or compiled, are intended to have no side-effects at all. A function-by-method has a method body that is intended to be a compiled way of computing what the function body expresses. But as a function may not have side-effects, the method body should not have any print statements.

In this case, the method body might print something because a method that is called in the body is attributed with {:print} (whether or not it actually does print something).

This tracking of print statements (and thus the possibility of this error message) only happens when the --track-print-effects option is enabled; the option is disabled by default.

### Error: to call a method with print effects, the enclosing method must be marked with {:print}

method m() { p(); }

method {:print} p() {}

The {:print} attribute is used to mark methods that have a side-effect of printing something, that is, they modify the external environment. In this case, the method body might print something because a method that is called in the body is attributed with {:print} (whether or not it actually does print something). So the calling method must be marked with {:print} as well.

This tracking of print statements (and thus the possibility of this error message) only happens when the --track-print-effects option is enabled; the option is disabled by default.

This section is a work in progress

## Verification Errors

This section is a work in progress

## Compilation Errors

### Error: process Process exited with exit code code

The dafny compiler prepares a representation of the Dafny program in the desired target programming language and then invokes the target language’s compiler on those files as a subsidiary process. This error message indicates that the sub-process terminated with an error of some sort. This should not ordinarily happen. Some possible causes are

• lack of resources that caused the underlying compiler to fail
• lack of or corrupted installation of the underlying compiler
• a bug in dafny whereby the source code it prepares for the compiler is faulty

There may be additional error messages from the underlying compiler that can help debug this situation. You can also attempt to run the target programming language compiler manually in your system to make sure it is functional.

### Error: Unable to start target

The dafny compiler prepares a representation of the Dafny program in the desired target programming language and then invokes the target language’s compiler on those files as a subsidiary process. This error message indicates that this sub-process would not start; it gives some additional information about what the invoking process was told about the failure to start.

Typically this error happens when the installation of the underlying compiler is not present or is incomplete, such as the proper files not having the correct permissions.

### Error: Error: ‘feature’ is not an element of the target compiler’s UnsupportedFeatures set

This messages indicates two problems:

• the given feature is not supported in the compiler for the target language but is present in the program, so the program will need to be revised to avoid this feature;
• the feature is not listed in the in-tool list of unsupported features. The latter is a (minor) bug in the in-tool documentation. Please report this error message and the part of the program provoking it to the Dafny team’s issue tracker.

### Error: Opaque type (‘type’) with extern attribute requires a compile hint. Expected {:extern compile_type_hint}

Documentation of extern and compile hints is in progress.

### Error: Opaque type (name) cannot be compiled; perhaps make it a type synonym or use :extern.

type T

Opaque types are declared like type T. They can be useful in programs where the particular characteristics of the type do not matter, such as in manipulating generic collections. Such programs can be verified, but in order to be compiled to something executable, the type must be given an actual definition. If the definition really does not matter, just give it a definition like type T = bool or type T = int.

Note that some properties of a type an be indicated using a type charcteristic. For example, type T(00) indicates that the type T is non-empty.

### Error: since yield parameters are initialized arbitrarily, iterators are forbidden by the –enforce-determinism option

iterator Gen(start: int) yields (x: int)
yield ensures |xs| <= 10 && x == start + |xs| - 1
{
var i := 0;
while i < 10 invariant |xs| == i {
x := start + i;
yield;
i := i + 1;
}
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. In an iterator, the yield parameters are initialized with arbitary values and can be read before they are set with actual values, so there is a bit of nondeterminism. Consequently, iterators in general are not permitted along with --enforce-determinism.

### Error: iterator name has no body

iterator Gen(start: int) yields (x: int)
yield ensures |xs| <= 10 && x == start + |xs| - 1

Programs containing iterators without bodies can be verified. However, a body-less iterator is an unchecked assumption (even if it is ghost). Consequently, like body-less functions and loops, dafny will not compile a program containing an iterator without a body. Furthermore, if the iterator is non-ghost, it cannot be executed if it does not have a body.

### Error: The method ‘name’ is not permitted as a main method (reason).

method mmm(i: int) {}

To create an executable program, the compiler needs to know which is the method to call to start the program, typically known as the ‘main’ method or main entry point. dafny chooses such a method based on a few rules (cf. details in the Dafny User Guide).

But there are restrictions on which methods may be used as a main entry point. Most importantly

• the method must take no input arguments or just one argument of type seq<string>
• it must not be ghost
• the method may be a class method, but then typically it is static

Most commonly and for clarity, the intended main method is marked with the attribute {:main}.

### Error: Could not find the method named by the -Main option: name

class A { static method mm() {} }

In the legacy command-line syntax, the main method may be specified on the command-line. When doing so, the name given must be a fully-qualified name. For instance. a method m in a (top-level) module M is named M.m or in a class C in a module M is named M.C.m. This error message indicates that dafny does not recognize the name given as the name of a method.

### Error: More than one method is marked {:main}. First declaration appeared at location.

method {:main} M(s: seq<string>) {}
method {:main} P() {}

When searching all the files in the program (including included ones), dafny found more than one method marked with {:main}. The error location is that of one of the methods and the error refers to another. The tool does not know which one to use. The solution is to remove the {:main} attribute from all but one.

Note that entry points that are intended as unit tests can be marked with {:test} instead.

### Error: This method marked {:main} is not permitted as a main method (name).

method {:main} M(i: int) {}

Only some methods may be used as entry points and the one indicated may not. The principal restrictions are these (more details in the Dafny User Guide):

• the method must take no input arguments or just one argument of type seq<string>
• it must not be ghost
• the method may be a class method, but then typically it is static

### Error: More than one method is declared as ‘Main’. First declaration appeared at location.

method Main(s: seq<string>) {}
class A {
static method Main() {}
}

In the absence of any {:main} attributes, dafny chooses a method named Main as the main entry point. When searching all the files in the program (including included ones), dafny found more than one method named Main. The error location is that of one of the methods and the error text refers to another. The solution is to mark one of them as {:main}.

Note that entry points that are intended as unit tests can be marked with {:test} instead.

### Error: This method ‘Main’ is not permitted as a main method (reason).

method Main(i: int) {}

If dafny finds no methods marked {:main}, it then looks for a method named Main to use as the starting point for the program. This error occurs if the Main method that is found does not qualify as a main entry point because it violates one or more of the rules, as given by the reason in the error message.

### Error: Function name has no body

function f(): int

The given function has no body, which is OK for verification, but not OK for compilation — the compiler does not know what content to give it. Even ghost functions must have bodies because body-less ghost functions are a form of unchecked assumptions.

### Error: Function name must be compiled to use the {:test} attribute

ghost function {:test} f(): int { 42 }

Only compiled functions and methods may be tested using the dafny test command, which tests everything marked with {:test}. However this function is a ghost function, and consequently cannot be tested during execution. If you want the function to be compiled, declare the function as a function instead of ghost function in Dafny 4 or as function method instead of function in Dafny 3.

### Error: Method name is annotated with :synthesize but is not static, has a body, or does not return anything

The {:synthesize} attribute is an experimental attribute used to create a mock object for methods that do not have bodies. It is currently only available for compiling to C# and in conjunction with the Moq library. See the reference manual section on {:synthesize} for more detail.

### Error: Method name has no body

method m()

To be part of a compiled program, each method must have a body. Ghost methods are the equivalent of unchecked assumptions so they too must have bodies.

### Error: kind ‘name’ is marked as :handle, so all the traits it extends must be marked as :handle as well: trait

The :handle attribute is deprecated.

### Error: kind ‘_name’ is marked as :handle, so all its non-static members must be ghost: trait

The :handle attribute is deprecated.

### Error: an assume statement cannot be compiled (use the {:axiom} attribute to let the compiler ignore the statement)

method m(x: int) {
assume x > 0;
}

A method may be parsed and verified even if an assume statement is present. However, the assume statement is an explicit, unchecked assumption. Dafny does not allow programs with unchecked assumptions, that is, incompletely verified programs, to be compiled. The {:axiom} attribute can be used to tell Dafny that the assumption is to be considered an externally verified axiom, with the program author taking responsibility for its validity.

If the assumption marked with {:axiom} is not actually valid, then the validity of the entire program is in question.

### Error: a forall statement without a body cannot be compiled

predicate P(i: int)
method m(a: array<int>) {
forall x: int | P(x)
var y := 3;
}

A method may be parsed and verified even if a forall statement is missing a body. However, the body must be supplied before the program can be compiled, even if the method is ghost. Body-less foralls in ghost methods are similar to unchecked assumptions.

### Error: a loop without a body cannot be compiled

ghost method m(i: int) {
var x: int := i;
while x > 0
x := 3;
}

A method may be parsed and verified even if a loop is missing a body. Note that a missing body is different than an empty body, which is just { }. However, the body must be supplied before the program can be compiled, even if the method is ghost. Body-less loops in ghost methods are similar to unchecked assumptions.

### Error: nondeterministic assignment forbidden by the –enforce-determinism option

method m() {
var x: int;
x := *;
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. Hence this ‘assign any legal value’ (... := *) statement is not permitted with --enforce-determinism.

There are a few different forms of this kind of assignment:

• x := *;
• x, y, z := 3, *, 42;
• forall i | 0 <= i < a.Length { a[i] := *; }

### Error: assign-such-that statement forbidden by the –enforce-determinism option

method m() {
var x: int;
x :| x < 5;
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. Hence this ‘assign any value that satisfies the predicate’ (:|) statement is not permitted with --enforce-determinism, even if there is only one such possible value. (The tool does not try to determine whether there is just one value and whether there is a reasonable way to compute it.)

### Error: this assign-such-that statement is too advanced for the current compiler; Dafny’s heuristics cannot find any bound for variable ‘name‘

The documentation of this problem is in progress.

### Error: nondeterministic if statement forbidden by the –enforce-determinism option

method m() {
var y: int;
if * { y:= 0; } else { y:= 1; }
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. Hence this ‘non-deterministic if’ (if *) statement is not permitted with --enforce-determinism.

### Error: binding if statement forbidden by the –enforce-determinism option

method m(k: int) {
var i := k;
var y: int;
if i :| i < 5 {  } else { y := 1; }
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. The if with a binding guard (if ... :| ) checks that the given predicate is satisfiable by some value. If not, then the ‘else’ branch is executed; but if so, the ‘then’ branch is executed with an arbitrary value that satisifies the predicate. Because of this arbitrary selection, the if-with-binding-guard is not permitted with --enforce-determinism, even if there is exactly one value that satisfies the predicate. (The tool does not try to determine whether there is just one value and whether there is a reasonable way to compute it.)

### Error: case-based if statement forbidden by the –enforce-determinism option

method m(k: int) {
var i := k;
if
{
case i >= 0 => i := i - 1;
case i <= 0 => i := i + 1;
}
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. The case-based if statement allows the case guards to be evaluated in an arbitrary order and an arbitrary one of those found to be true is chosen to be executed. Hence the case-based if is not permitted with --enforce-determinism.

To enforce a deterministic order to the evaluation, use a chain of if-then-else statements.

### Error: nondeterministic loop forbidden by the –enforce-determinism option

method m(b: bool) decreases * {
while *
decreases *
{ }
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. Hence this ‘non-deterministic while’ (while *) statement is not permitted with --enforce-determinism.

### Error: case-based loop forbidden by the –enforce-determinism option

method m(k: int) {
var i := k;
while
decreases if i < 0 then -i else i
{
case i > 0 => i := i - 1;
case i < 0 => i := i + 1;
}
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result. The case-based while statement allows the case guards to be evaluated in an arbitrary order and an arbitrary one of those found to be true is chosen to be executed. Hence the case-based loop is not permitted with --enforce-determinism.

To enforce a deterministic order to the evaluation, use a chain of if-then-else statements or series of if statements in which the then-branch ends in a continue statement.

### Error: compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements

The documentation of this problem is in progress.

### Error: modify statement without a body forbidden by the –enforce-determinism option

class A { var j: int }

method m(k: int, o: A)
modifies o
{
var i := k;
modify o;
}

The --enforce-determinism option requires a target program to be deterministic and predictable: there may be no program statements that have an arbitrary, even if deterministic, result.

The modify statement allows the program to modify the state of the given objects in an arbitrary way (though each field still has a legal value of its declared type). Hence such a statement is not permitted with --enforce-determinism.

Note that a modify statement with a body is deprecated.

### Error: this let-such-that expression is too advanced for the current compiler; Dafny’s heuristics cannot find any bound for variable ‘name‘

The documentation of this problem is in progress.

### Error: Comparison of a handle can only be with another handle

The documentation of the {:handle} attribute is in progress.

### **Error: Post-conditions on function function might be unsatisfied when synthesizing code for method name”

This message relates to mocking methods in C# with the Moq framework. See the reference manual section on {:synthesize} for more detail.

This message relates to mocking methods in C# with the Moq framework. See the reference manual section on {:synthesize} for more detail.

## Errors specific to the Go compiler

### Error: Unsupported field name in extern trait

Documentation of the Go compiler errors is in progress.

### Error: Cannot convert from type to target-type

Documentation of the Go compiler errors is in progress.