Types in Dafny

0. Basic types

Dafny offers three basic types, bool for booleans, int for integers, and real for reals.

0.0. Booleans

There are two boolean values and each has a corresponding literal in the language: false and true.

In addition to equality (==) and disequality (!=), which are defined on all types, type bool supports the following operations:

Negation is unary; the others are binary. The table shows the operators in groups of increasing binding power, with equality binding stronger than conjunction and disjunction, and weaker than negation. Within each group, different operators do not associate, so parentheses need to be used. For example,

A && B || C    // error

would be ambiguous and instead has to be written as either

(A && B) || C

or

A && (B || C)

depending on the intended meaning.

The expressions A <==> B and A == B give the same value, but note that <==> is associative whereas == is chaining. So,

A <==> B <==> C

is the same as

A <==> (B <==> C)

and

(A <==> B) <==> C

whereas

A == B == C

is simply a shorthand for

A == B && B == C

Conjunction is associative and so is disjunction. These operators are are short circuiting (from left to right), meaning that their second argument is evaluated only if the evaluation of the first operand does not determine the value of the expression. Logically speaking, the expression A && B is defined when A is defined and either A evaluates to false or B is defined. When A && B is defined, its meaning is the same as the ordinary, symmetric mathematical conjunction ∧. The same holds for || and ∨.

Implication is right associative and is short-circuiting from left to right. Reverse implication B <== A is exactly the same as A ==> B, but gives the ability to write the operands in the opposite order. Consequently, reverse implication is left associative and is short-circuiting from right to left. To illustrate the associativity rules, each of the following four lines expresses the same property, for any A, B, and C of type bool:

A ==> B ==> C
A ==> (B ==> C)  // parentheses redundant, since ==> is right associative
C <== B <== A
(C <== B) <== A  // parentheses redundant, since <== is left associative

To illustrate the short-circuiting rules, note that the expression a.Length is defined for an array a only if a is not null (see Section 5), which means the following two expressions are well-formed:

a != null ==> 0 <= a.Length
0 <= a.Length <== a != null

The contrapositive of these two expressions would be:

a.Length < 0 ==> a == null  // not well-formed
a == null <== a.Length < 0  // not well-formed

but these expressions are not well-formed, since well-formedness requires the left (and right, respectively) operand, a.Length < 0, to be well-formed by itself.

Implication A ==> B is equivalent to the disjunction !A || B, but is sometimes (especially in specifications) clearer to read. Since, || is short-circuiting from left to right, note that

a == null || 0 <= a.Length

is well-formed, whereas

0 <= a.Length || a == null  // not well-formed

is not.

In addition, booleans support logical quantifiers (forall and exists), described in a different part of the Dafny language reference.

0.1. Numeric types

Dafny supports numeric types of two kinds, integer-based, which includes the basic type int of all integers, and real-based, which includes the basic type real of all real numbers. User-defined numeric types based on int and real, called newtypes, are described in Section 7. Also, the subset type nat, representing the non-negative subrange of int, is described in Section 8.

The language includes a literal for each non-negative integer, like 0, 13, and 1985. Integers can also be written in hexadecimal using the prefix “0x”, as in 0x0, 0xD, and 0x7c1 (always with a lower case x, but the hexadecimal digits themselves are case insensitive). Leading zeros are allowed. To form negative integers, use the unary minus operator.

There are also literals for some of the non-negative reals. These are written as a decimal point with a nonempty sequence of decimal digits on both sides. For example, 1.0, 1609.344, and 0.5772156649.

For integers (in both decimal and hexidecimal form) and reals, any two digits in a literal may be separated by an underscore in order to improve human readability of the literals. For example:

1_000_000        // easier to read than 1000000
0_12_345_6789    // strange but legal formatting of 123456789
0x8000_0000      // same as 0x80000000 -- hex digits are often placed in groups of 4
0.000_000_000_1  // same as 0.0000000001 -- 1 Ångström

In addition to equality and disequality, numeric types support the following relational operations:

Like equality and disequality, these operators are chaining, as long as they are chained in the “same direction”. That is,

A <= B < C == D <= E

is simply a shorthand for

A <= B && B < C && C == D && D <= E

whereas

A < B > C

is not allowed.

There are also operators on each numeric type:

The binary operators are left associative, and they associate with each other in the two groups. The groups are listed in order of increasing binding power, with equality binding more strongly than the multiplicative operators and weaker than the unary operator. Modulus is supported only for integer-based numeric types. Integer division and modulus are the Euclidean division and modulus. This means that modulus always returns a non-negative, regardless of the signs of the two operands. More precisely, for any integer a and non-zero integer b,

a == a / b * b + a % b
0 <= a % b < B

where B denotes the absolute value of b.

Real-based numeric types have a member Trunc that returns the floor of the real value, that is, the largest integer not exceeding the real value. For example, the following properties hold, for any r and r' of type real:

3.14.Trunc == 3
(-2.5).Trunc == -3
-2.5.Trunc == -2
real(r.Trunc) <= r
r <= r' ==> r.Trunc <= r'.Trunc

Note in the third line that member access (like .Trunc) binds stronger than unary minus. The fourth line uses the conversion function real from int to real, as described in Section 7.0.

0.2. Characters

Dafny supports a type char of characters. Character literals are enclosed in single quotes, as in 'D'. To write a single quote as a character literal, it is necessary to use an escape sequence. Escape sequences can also be used to write other characters. The supported escape sequences are as follows:

The escape sequence for a double quote is redundant, because '"' and '\"' denote the same character—both forms are provided in order to support the same escape sequences as for string literals (Section 2.2.0). In the form \uxxxx, the u is always lower case, but the four hexadecimal digits are case insensitive.

Character values are ordered and can be compared using the standard relational operators:

Sequences of characters represent strings, as described in Section 2.2.0.

1. Type parameters

Many of the types (as well as functions and methods) in Dafny can be parameterized by types. These type parameters are typically declared inside angle brackets and can stand for any type. It is sometimes necessary to restrict these type parameters so that they can only be instantiated by certain families of types. As such, Dafny distinguishes types that support the equality operation not only in ghost contexts but also in compiled contexts. To indicate that a type parameter is restricted to such equality supporting types, the name of the type parameter takes the suffix “(==)”.⁰ For example,

method Compare〈T(==)〉(a: T, b: T) returns (eq: bool)
{
  if a == b { eq := true; } else { eq := false; }
}

is a method whose type parameter is restricted to equality-supporting types. Again, note that all types support equality in ghost contexts; the difference is only for non-ghost (that is, compiled) code. Co-inductive datatypes, function types, as well as inductive datatypes with ghost parameters are examples of types that are not equality supporting.

Dafny has some inference support that makes certain signatures less cluttered (described in a different part of the Dafny language reference). In some cases, this support will infer that a type parameter must be restricted to equality-supporting types, in which case Dafny adds the “(==)” automatically.

2. Collection types

Dafny offers several built-in collection types.

2.0. Sets

For any type T, each value of type set〈T〉 is a finite set of T values. Set membership is determined by equality in the type T, so set〈T〉 can be used in a non-ghost context only if T is equality supporting.

A set can be formed using a set display expression, which is a possibly empty, unordered, duplicate-insensitive list of expressions enclosed in curly braces. To illustrate,

{}        {2, 7, 5, 3}        {4+2, 1+5, a*b}

are three examples of set displays. There is also a set comprehension expression (with a binder, like in logical quantifications), described in a different part of the Dafny language reference.

In addition to equality and disequality, set types support the following relational operations:

Like the arithmetic relational operators, these operators are chaining.

Sets support the following binary operators, listed in order of increasing binding power:

The associativity rules of +, -, and * are like those of the arithmetic operators with the same names. The expression A !! B, whose binding power is the same as equality (but which neither associates nor chains with equality), says that sets A and B have no elements in common, that is, it is equivalent to

A * B == {}

However, the disjointness operator is chaining, so A !! B !! C !! D means:

A * B == {} && (A + B) * C == {} && (A + B + C) * D == {}

In addition, for any set s of type set〈T〉 and any expression e of type T, sets support the following operations:

The expression e !in s is a syntactic shorthand for !(e in s).

2.1. Multisets

A multiset is similar to a set, but keeps track of the multiplicity of each element, not just its presence or absence. For any type T, each value of type multiset〈T〉 is a map from T values to natural numbers denoting each element's multiplicity. Multisets in Dafny are finite, that is, they contain a finite number of each of a finite set of elements. Stated differently, a multiset maps only a finite number of elements to non-zero (finite) multiplicities.

Like sets, multiset membership is determined by equality in the type T, so multiset〈T〉 can be used in a non-ghost context only if T is equality supporting.

A multiset can be formed using a multiset display expression, which is a possibly empty, unordered list of expressions enclosed in curly braces after the keyword multiset. To illustrate,

multiset{}    multiset{0, 1, 1, 2, 3, 5}    multiset{4+2, 1+5, a*b}

are three examples of multiset displays. There is no multiset comprehension expression.

In addition to equality and disequality, multiset types support the following relational operations:

Like the arithmetic relational operators, these operators are chaining.

Multisets support the following binary operators, listed in order of increasing binding power:

The associativity rules of +, -, and * are like those of the arithmetic operators with the same names. The expression A !! B says that multisets A and B have no elements in common, that is, it is equivalent to

A * B == multiset{}

Like the analogous set operator, !! is chaining.

In addition, for any multiset s of type multiset〈T〉, expression e of type T, and non-negative integer-based numeric n, multisets support the following operations:

The expression e in s returns true if and only if s[e] != 0. The expression e !in s is a syntactic shorthand for !(e in s). The expression s[e := n] denotes a multiset like s, but where the multiplicity of element e is n. Note that the multiset update s[e := 0] results in a multiset like s but without any occurrences of e (whether or not s has occurrences of e in the first place). As another example, note that s - multiset{e} is equivalent to:

if e in s then s[e := s[e] - 1] else s

2.2. Sequences

For any type T, a value of type seq〈T〉 denotes a sequence of T elements, that is, a mapping from a finite set of consecutive natural numbers (called indicies) to T values. (Thinking of it as a map, a sequence is therefore something of a dual of a multiset.)

A sequence can be formed using a sequence display expression, which is a possibly empty, ordered list of expressions enclosed in square brackets. To illustrate,

[]        [3, 1, 4, 1, 5, 9, 3]        [4+2, 1+5, a*b]

are three examples of sequence displays. There is no sequence comprehension expression.

In addition to equality and disequality, sequence types support the following relational operations:

Like the arithmetic relational operators, these operators are chaining. Note the absence of > and >=.

Sequences support the following binary operator:

Operator + is associative, like the arithmetic operator with the same name.

In addition, for any sequence s of type seq〈T〉, expression e of type T, integer-based numeric i satisfying 0 <= i < |s|, and integer-based numerics lo and hi satisfying 0 <= lo <= hi <= |s|, sequences support the following operations:

Expression s[i := e] returns a sequence like s, except that the element at index i is e. The expression e in s says there exists an index i such that s[i] == e. It is allowed in non-ghost contexts only if the element type T is equality supporting. The expression e !in s is a syntactic shorthand for !(e in s).

Expression s[lo..hi] yields a sequence formed by taking the first hi elements and then dropping the first lo elements. The resulting sequence thus has length hi - lo. Note that s[0..|s|] equals s. If the upper bound is omitted, it defaults to |s|, so s[lo..] yields the sequence formed by dropping the first lo elements of s. If the lower bound is omitted, it defaults to 0, so s[..hi] yields the sequence formed by taking the first hi elements of s.

In the sequence slice operation, slices is a nonempty list of length designators separated and optionally terminated by a colon, and there is at least one colon. Each length designator is a non-negative integer-based numeric, whose sum is no greater than |s|. If there are k colons, the operation produces k consecutive subsequences from s, each of the length indicated by the corresponding length designator, and returns these as a sequence of sequences.¹ If slices is terminated by a colon, then the length of the last slice extends until the end of s, that is, its length is |s| minus the sum of the given length designators. For example, the following equalities hold, for any sequence s of length at least 10:

var t := [3.14, 2.7, 1.41, 1985.44, 100.0, 37.2][1:0:3];
assert |t| == 3 && t[0] == [3.14] && t[1] == [];
assert t[2] == [2.7, 1.41, 1985.44];
var u := [true, false, false, true][1:1:];
assert |u| == 3 && u[0][0] && !u[1][0] && u[2] == [false, true];
assert s[10:][0] == s[..10];
assert s[10:][1] == s[10..];

The operation multiset(s) yields the multiset of elements of sequence s. It is allowed in non-ghost contexts only if the element type T is equality supporting.

2.2.0. Strings

A special case of a sequence type is seq〈char〉, for which Dafny provides a synonym: string. Strings are like other sequences, but provide additional syntax for sequence display expressions, namely string literals. There are two forms of the syntax for string literals: the standard form and the verbatim form.

String literals of the standard form are enclosed in double quotes, as in "Dafny". To include a double quote in such a string literal, it is necessary to use an escape sequence. Escape sequences can also be used to include other characters. The supported escape sequences are the same as those for character literals, see Section 0.2. For example, the Dafny expression "say \"yes\"" represents the string say "yes". The escape sequence for a single quote is redundant, because "'" and "\'" denote the same string—both forms are provided in order to support the same escape sequences as for character literals.

String literals of the verbatim form are bracketed by @" and ", as in @"Dafny". To include a double quote in such a string literal, it is necessary to use the escape sequence "", that is, to write the character twice. In the verbatim form, there are no other escape sequences. Even characters like newline can be written inside the string literal (hence spanning more than one line in the program text).

For example, the following three expressions denote the same string:

"C:\\tmp.txt"
@"C:\tmp.txt"
['C', ':', '\\', 't', 'm', 'p', '.', 't', 'x', 't']

Since strings are sequences, the relational operators < and <= are defined on them. Note, however, that these operators still denote proper prefix and prefix, respectively, not some kind of alphabetic comparison as might be desireable, for example, when sorting strings.

2.3. Finite and Infinite Maps

For any types T and U, a value of type map〈T,U〉 denotes a (finite) map from T to U. In other words, it is a look-up table indexed by T. The domain of the map is a finite set of T values that have associated U values. Since the keys in the domain are compared using equality in the type T, type map〈T,U〉 can be used in a non-ghost context only if T is equality supporting.

Similarly, for any types T and U, a value of type imap〈T,U〉 denotes a (possibly) infinite map. In most regards, imap〈T,U〉 is like map〈T,U〉, but a map of type imap〈T,U〉 is allowed to have an infinite domain.

A map can be formed using a map display expression, which is a possibly empty, ordered list of maplets, each maplet having the form t := u where t is an expression of type T and u is an expression of type U, enclosed in square brackets after the keyword map. To illustrate,

map[]    map[20 := true, 3 := false, 20 := false]    map[a+b := c+d]

are three examples of map displays. By using the keyword imap instead of map, the map produced will be of type imap〈T,U〉 instead of map〈T,U〉. Note that an infinite map (imap) is allowed to have a finite domain, whereas a finite map (map) is not allowed to have an infinite domain. If the same key occurs more than once, only the last occurrence appears in the resulting map.² There is also a map comprehension expression, explained in a different part of the Dafny language reference.

For any map fm of type map〈T,U〉, any map m of type map〈T,U〉 or imap〈T,U〉, any expression t of type T, any expression u of type U, and any d in the domain of m (that is, satisfying d in m), maps support the following operations:

|fm| denotes the number of mappings in fm, that is, the cardinality of the domain of fm. Note that the cardinality operator is not supported for infinite maps. Expression m[d] returns the U value that m associates with d. Expression m[t := u] is a map like m, except that the element at key t is u. The expression t in m says t is in the domain of m and t !in m is a syntactic shorthand for !(t in m).³

Here is a small example, where a map cache of type map〈int,real〉 is used to cache computed values of Joule-Thomson coefficients for some fixed gas at a given temperature:

if K in cache {  // check if temperature is in domain of cache
  coeff := cache[K];  // read result in cache
} else {
  coeff := ComputeJouleThomsonCoefficient(K);  // do expensive computation
  cache := cache[K := coeff];  // update the cache
}

3. Types that stand for other types

It is sometimes useful to know a type by several names or to treat a type abstractly.

3.0. Type synonyms

A type synonym declaration:

type Y〈T〉 = G

declares Y〈T〉 to be a synonym for the type G. Here, T is a nonempty list of type parameters (each of which is optionally designated with the suffix “(==)”), which can be used as free type variables in G. If the synonym has no type parameters, the “〈T〉” is dropped. In all cases, a type synonym is just a synonym. That is, there is never a difference, other than possibly in error messages produced, between Y〈T〉 and G.

For example, the names of the following type synonyms may improve the readability of a program:

type Replacements〈T〉 = map〈T,T〉
type Vertex = int

As already described in Section 2.2.0, string is a built-in type synonym for seq〈char〉, as if it would have been declared as follows:

type string = seq〈char〉

3.1. Opaque types

A special case of a type synonym is one that is underspecified. Such a type is declared simply by:

type Y〈T〉

It is a known as an opaque type. Its definition can be revealed in a refining module. To indicate that Y designates an equality-supporting type, “(==)” can be written immediately following the name “Y”.

For example, the declarations

type T
function F(t: T): T

can be used to model an uninterpreted function F on some arbitrary type T. As another example,

type Monad〈T〉

can be used abstractly to represent an arbitrary parameterized monad.

4. Datatypes

Dafny offers two kinds of algebraic datatypes, those defined inductively and those defined co-inductively. The salient property of every datatype is that each value of the type uniquely identifies one of the datatype's constructors and each constructor is injective in its parameters.

4.0. Inductive datatypes

The values of inductive datatypes can be seen as finite trees where the leaves are values of basic types, numeric types, reference types, co-inductive datatypes, or function types. Indeed, values of inductive datatypes can be compared using Dafny's well-founded < ordering.

An inductive datatype is declared as follows:

datatype D〈T〉 = Ctors

where Ctors is a nonempty |-separated list of (datatype) constructors for the datatype. Each constructor has the form:

C(params)

where params is a comma-delimited list of types, optionally preceded by a name for the parameter and a colon, and optionally preceded by the keyword ghost. If a constructor has no parameters, the parentheses after the constructor name can be omitted. If no constructor takes a parameter, the type is usually called an enumeration; for example:

datatype Friends = Agnes | Agatha | Jermaine | Jack

For every constructor C, Dafny defines a discriminator C?, which is a member that returns true if and only if the datatype value has been constructed using C. For every named parameter p of a constructor C, Dafny defines a destructor p, which is a member that returns the p parameter from the C call used to construct the datatype value; its use requires that C? holds. For example, for the standard List type

datatype List〈T〉 = Nil | Cons(head: T, tail: List〈T〉)

the following holds:

Cons(5, Nil).Cons? && Cons(5, Nil).head == 5

Note that the expression

Cons(5, Nil).tail.head

is not well-formed, since Cons(5, Nil).tail does not satisfy Cons?.

The names of the destructors must be unique across all the constructors of the datatype. A constructor can have the same name as the enclosing datatype; this is especially useful for single-constructor datatypes, which are often called record types. For example, a record type for black-and-white pixels might be represented as follows:

datatype Pixel = Pixel(x: int, y: int, on: bool)

To call a constructor, it is usually necessary only to mention the name of the constructor, but if this is ambiguous, it is always possible to qualify the name of constructor by the name of the datatype. For example, Cons(5, Nil) above can be written

List.Cons(5, List.Nil)

As an alternative to calling a datatype constructor explicitly, a datatype value can be constructed as a change in one parameter from a given datatype value using the datatype update expression. For any d whose type is a datatype that includes a constructor C that has a parameter (destructor) named f of type T, and any expression t of type T,

d[f := t]

constructs a value like d but whose f parameter is t. The operation requires that d satisfies C?. For example, the following equality holds:

Cons(4, Nil)[tail := Cons(3, Nil)] == Cons(4, Cons(3, Nil))

4.1. Tuple types

Dafny builds in record types that correspond to tuples and gives these a convenient special syntax, namely parentheses. For example, what might have been declared as:

datatype Pair〈T,U〉 = Pair(0: T, 1: U)

Dafny provides as the type (T, U) and the constructor (t, u), as if the datatype's name were “” and its type arguments are given in round parentheses, and as if the constructor name were “”. Note that the destructor names are 0 and 1, which are legal identifier names for members. For example, showing the use of a tuple destructor, here is a property that holds of 2-tuples (that is, pairs):

(5, true).1 == true

Dafny declares n-tuples where n is 0 or 2 or up. There are no 1-tuples, since parentheses around a single type or a single value have no semantic meaning. The 0-tuple type, (), is often known as the unit type and its single value, also written (), is known as unit.

4.2. Co-inductive datatypes

Whereas Dafny insists that there is a way to construct every inductive datatype value from the ground up, Dafny also supports co-inductive datatypes, whose constructors are evaluated lazily and hence allows infinite structures. A co-inductive datatype is declared using the keyword codatatype; other than that, it is declared and used like an inductive datatype.

For example,

codatatype IList〈T〉 = Nil | Cons(head: T, tail: IList〈T〉)
codatatype Stream〈T〉 = More(head: T, tail: Stream〈T〉)
codatatype Tree〈T〉 = Node(left: Tree〈T〉, value: T, right: Tree〈T〉)

declare possibly infinite lists (that is, lists that can be either finite or infinite), infinite streams (that is, lists that are always infinite), and infinite binary trees (that is, trees where every branch goes on forever), respectively.

5. Reference types

Dafny offers a host of reference types. These represent references to objects allocated dynamically in the program heap. To access the members of an object, a reference to (that is, a pointer to or object identity of) the object is dereferenced.

The special value null is part of every reference type.⁴

5.0. Classes

A class C is a reference type declared as follows:

class C〈T〉 extends J
{
  members
}

where the list of type parameters T is optional and so is “extends J”, which says that the class extends a trait J. The members of a class are fields, functions, and methods. These are accessed or invoked by dereferencing a reference to a C instance. A function or method is invoked on an instance of C, unless the function or method is declared static. Mechanically, this just means the method takes an implicit receiver parameter, namely, the instance used to access the member. In the specification and body of an instance function or method, the receiver parameter can be referred to explicitly by the keyword this. However, in such places, members of this can also be mentioned without any qualification. To illustrate, the qualified this.f and the unqualified f refer to the same field of the same object in the following example:

class C {
  var f: int;
  method Example() returns (b: bool)
  {
    b := f == this.f;
  }
}

so the method body always assigns true to the out-parameter b. There is no semantic difference between qualified and unqualified accesses to the same receiver and member.

A C instance is created using new, for example:

c := new C;

Note that new simply allocates a C object and returns a reference to it; the initial values of its fields are arbitrary values of their respective types. Therefore, it is common to invoke a method, known as an initialization method, immediately after creation, for example:

c := new C;
c.InitFromList(xs, 3);

When an initialization method has no out-parameters and modifies no more than this, then the two statements above can be combined into one:

c := new C.InitFromList(xs, 3);

Note that a class can contain several initialization methods, that these methods can be invoked at any time, not just as part of a new, and that new does not require that an initialization method be invoked at creation.

To write structured object-oriented programs, one often relies on that objects are constructed only in certain ways. For this purpose, Dafny provides constructor (method)s, which are a restricted form of initialization methods. A constructor is declared with the keyword constructor instead of method. When a class contains a constructor, every call to new for that class must be accompanied with a call to one of the constructors. Moreover, a constructor cannot be called at other times, only during object creation. Other than these restrictions, there is no semantic difference between using ordinary initialization methods and using constructors.

The Dafny design allows the constructors to be named, which promotes using names like InitFromList above. Still, many classes have just one constructor or have a typical constructor. Therefore, Dafny allows one anonymous constructor, that is, a constructor whose name is essentially “”. For example:

class Item {
  constructor (x: int, y: int)
  // ...
}

When invoking this constructor, the “.” is dropped, as in:

m := new Item(45, 29);

Note that an anonymous constructor is just one way to name a constructor; there can be other constructors as well.

5.1. Arrays

Dafny supports mutable fixed-length array types of any positive dimension. Array types are reference types.

5.1.0. One-dimensional arrays

A one-dimensional array of n T elements is created as follows:

a := new T[n];

The initial values of the array elements are arbitrary values of type T. The length of an array is retrieved using the immutable Length member. For example, the array allocated above satisfies:

a.Length == n

For any integer-based numeric i in the range 0 <= i < a.Length, the array selection expression a[i] retrieves element i (that is, the element preceded by i elements in the array). The element stored at i can be changed to a value t using the array update statement:

a[i] := t;

Caveat: The type of the array created by new T[n] is array〈T〉. A mistake that is simple to make and that can lead to befuddlement is to write array〈T〉 instead of T after new. For example, consider the following:

var a := new array〈T〉;
var b := new array〈T〉[n];
var c := new array〈T〉(n);  // resolution error
var d := new array(n);  // resolution error

The first statement allocates an array of type array〈T〉, but of unknown length. The second allocates an array of type array〈array〈T〉〉 of length n, that is, an array that holds n values of type array〈T〉. The third statement allocates an array of type array〈T〉 and then attempts to invoke an anonymous constructor on this array, passing argument n. Since array has no constructors, let alone an anonymous constructor, this statement gives rise to an error. If the type-parameter list is omitted for a type that expects type parameters, Dafny will attempt to fill these in, so as long as the array type parameter can be inferred, it is okay to leave off the “〈T〉” in the fourth statement above. However, as with the third statement, array has no anonymous constructor, so an error message is generated.

One-dimensional arrays support operations that convert a stretch of consecutive elements into a sequence. For any array a of type array〈T〉, integer-based numerics lo and hi satisfying 0 <= lo <= hi <= a.Length, the following operations each yields a seq〈T〉:

The expression a[lo..hi] takes the first hi elements of the array, then drops the first lo elements thereof and returns what remains as a sequence. The resulting sequence thus has length hi - lo. The other operations are special instances of the first. If lo is omitted, it defaults to 0 and if hi is omitted, it defaults to a.Length. In the last operation, both lo and hi have been omitted, thus a[..] returns the sequence consisting of all the array elements of a.

The subarray operations are especially useful in specifications. For example, the loop invariant of a binary search algorithm that uses variables lo and hi to delimit the subarray where the search key may be still found can be expressed as follows:

key !in a[..lo] && key !in a[hi..]

Another use is to say that a certain range of array elements have not been changed since the beginning of a method:

a[lo..hi] == old(a[lo..hi])

or since the beginning of a loop:

ghost var prevElements := a[..];
while // ...
  invariant a[lo..hi] == prevElements[lo..hi];
{
  // ...
}

Note that the type of prevElements in this example is seq〈T〉, if a has type array〈T〉.

A final example of the subarray operation lies in expressing that an array's elements are a permutation of the array's elements at the beginning of a method, as would be done in most sorting algorithms. Here, the subarray operation is combined with the sequence-to-multiset conversion:

multiset(a[..]) == multiset(old(a[..]))

5.1.1. Multi-dimensional arrays

An array of 2 or more dimensions is mostly like a one-dimensional array, except that new takes more length arguments (one for each dimension), and the array selection expression and the array update statement take more indices. For example:

matrix := new T[m, n];
matrix[i, j], matrix[x, y] := matrix[x, y], matrix[i, j];

create a 2-dimensional array whose dimensions have lengths m and n, respectively, and then swaps the elements at i,j and x,y. The type of matrix is array2〈T〉, and similarly for higher-dimensional arrays (array3〈T〉, array4〈T〉, etc.). Note, however, that there is no type array0〈T〉, and what could have been array1〈T〉 is actually named just array〈T〉.

The new operation above requires m and n to be non-negative integer-based numerics. These lengths can be retrieved using the immutable fields Length0 and Length1. For example, the following holds of the array created above:

matrix.Length0 == m && matrix.Length1 == n

Higher-dimensional arrays are similar (Length0, Length1, Length2, …). The array selection expression and array update statement require that the indices are in bounds. For example, the swap statement above is well-formed only if:

0 <= i < matrix.Length0 && 0 <= j < matrix.Length1 &&
0 <= x < matrix.Length0 && 0 <= y < matrix.Length1

In contrast to one-dimensional arrays, there is no operation to convert stretches of elements from a multi-dimensional array to a sequence.

5.2. Traits

A trait is an “abstract superclass”, or call it an “interface” or “mixin”. Traits are new to Dafny and are likely to evolve for a while.

The declaration of a trait is much like that of a class:

trait J
{
  members
}

where members can include fields, functions, and methods, but no constructor methods. The functions and methods are allowed to be declared static.

A reference type C that extends a trait J is assignable to J, but not the other way around. The members of J are available as members of C. A member in J is not allowed to be redeclared in C, except if the member is a non-static function or method without a body in J. By doing so, type C can supply a stronger specification and a body for the member.

new is not allowed to be used with traits. Therefore, there is no object whose allocated type is a trait. But there can of course be objects of a class C that implements a trait J, and a reference to such a C object can be used as a value of type J.

As an example, the following trait represents movable geometric shapes:

trait Shape
{
  function method Width(): real
    reads this
  method Move(dx: real, dy: real)
    modifies this
  method MoveH(dx: real)
    modifies this
  {
    Move(dx, 0.0);
  }
}

Members Width and Move are abstract (that is, body less) and can be implemented differently by different classes that extend the trait. The implementation of method MoveH is given in the trait and thus gets used by all classes that extend Shape. Here are two classes that each extends Shape:

class UnitSquare extends Shape
{
  var x: real, y: real;
  function method Width(): real {  // note the empty reads clause
    1.0
  }
  method Move(dx: real, dy: real)
    modifies this
  {
    x, y := x + dx, y + dy;
  }
}
class LowerRightTriangle extends Shape
{
  var xNW: real, yNW: real, xSE: real, ySE: real;
  function method Width(): real
    reads this
  {
    xSE - xNW
  }
  method Move(dx: real, dy: real)
    modifies this
  {
    xNW, yNW, xSE, ySE := xNW + dx, yNW + dy, xSE + dx, ySE + dy;
  }
}

Note that the classes can declare additional members, that they supply implementations for the abstract members of the trait, that they repeat the member signatures, and that they are responsible for providing their own member specifications that both strengthen the corresponding specification in the trait and are satisfied by the provided body. Finally, here is some code that creates two class instances and uses them together as shapes:

var myShapes: seq〈Shape〉;
var A := new UnitSquare;
myShapes := [A];
var tri := new LowerRightTriangle;
myShapes := myShapes + [tri];  // myShapes contains two Shape values, of different classes
myShapes[1].MoveH(myShapes[0].Width());  // move shape 1 to the right by the width of shape 0

5.3. Type object

There is a built-in reference type object that is like a supertype of all reference types.⁵ The purpose of type object is to enable a uniform treatment of dynamic frames. In particular, it is useful to keep a ghost field (typically named Repr for “representation”) of type set〈object〉.

5.4. Iterator types

An iterator provides a programming abstraction for writing code that iteratively returns elements. These CLU-style iterators are co-routines in the sense that they keep track of their own program counter and control can be transferred into and out of the iterator body.

An iterator is declared as follows:

iterator Iter〈T〉(in-params) yields (yield-params)
  specification
{
  body
}

where T is a list of type parameters (as usual, if there are no type parameters, “〈T〉” is omitted). This declaration gives rise to a reference type with the same name, Iter〈T〉. In the signature, in-parameters and yield-parameters are the iterator's analog of a method's in-parameters and out-parameters. The difference is that the out-parameters of a method are returned to a caller just once, whereas the yield-parameters of an iterator are returned each time the iterator body performs a yield. The details of the specification are described in a different part of the Dafny language reference. The body consists of statements, like in a method body, but with the availability also of yield statements.

From the perspective of an iterator client, the iterator declaration can be understood as generating a class Iter〈T〉 with various members, a simplified version of which is described next.

The Iter〈T〉 class contains an anonymous constructor whose parameters are the iterator's in-parameters:

predicate Valid()
constructor (in-params)
  modifies this
  ensures Valid()

An iterator is created using new and this anonymous constructor. For example, an iterator willing to return ten consecutive integers from start can be declared as follows:

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

An instance of this iterator is created using:

iter := new Gen(30);

The predicate Valid() says when the iterator is in a state where one can attempt to compute more elements. It is a postcondition of the constructor and occurs in the specification of the MoveNext member:

method MoveNext() returns (more: bool)
  requires Valid()
  modifies this
  ensures more ==> Valid()

Note that the iterator remains valid as long as MoveNext returns true. Once MoveNext returns false, the MoveNext method can no longer be called. Note, the client is under no obligation to keep calling MoveNext until it returns false, and the body of the iterator is allowed to keep returning elements forever.

The in-parameters of the iterator are stored in immutable fields of the iterator class. To illustrate in terms of the example above, the iterator class Gen contains the following field:

var start: int;

The yield-parameters also result in members of the iterator class:

var x: int;

These fields are set by the MoveNext method. If MoveNext returns true, the latest yield values are available in these fields and the client can read them from there.

To aid in writing specifications, the iterator class also contains ghost members that keep the history of values returned by MoveNext. The names of these ghost fields follow the names of the yield-parameters with an “s” appended to the name (to suggest plural). Name checking rules make sure these names do not give rise to ambiguities. The iterator class for Gen above thus contains:

ghost var xs: seq〈int〉;

These history fields are changed automatically by MoveNext, but are not assignable by user code.

Finally, the iterator class contains some special fields for use in specifications. In particular, the iterator specification gets recorded in the following immutable fields:

ghost var _reads: set〈object〉;
ghost var _modifies: set〈object〉;
ghost var _decreases0: T0;
ghost var _decreases1: T1;
// ...

where there is a _decreasesi: Ti field for each component of the iterator's decreases clause.⁶ In addition, there is a field:

ghost var _new: set〈object〉;

to which any objects allocated on behalf of the iterator body get added. The iterator body is allowed to remove elements from the _new set, but cannot by assignment to _new add any elements.

Note, in the precondition of the iterator, which is to hold upon construction of the iterator, the in-parameters are indeed in-parameters, not fields of this.

5.5. Async-task types

Another experimental feature in Dafny that is likely to undergo some evolution is asynchronous methods. When an asynchronous method is called, it does not return values for the out-parameters, but instead returns an instance of an async-task type. An asynchronous method declared in a class C with the following signature:

async method AM〈T〉(in-params) returns (out-params)

also gives rise to an async-task type AM〈T〉 (outside the enclosing class, the name of the type needs the qualification C.AM〈T〉). The async-task type is a reference type and can be understood as a class with various members, a simplified version of which is described next.

Each in-parameter x of type X of the asynchronous method gives rise to a immutable ghost field of the async-task type:

ghost var x: X;

Each out-parameter y of type Y gives rise to a field

var y: Y;

These fields are changed automatically by the time the asynchronous method is successfully awaited, but are not assignable by user code.

The async-task type also gets a number of special fields that are used to keep track of dependencies, outstanding tasks, newly allocated objects, etc. These fields will be described in more detail as the design of asynchronous methods evolves.

6. Function types

Functions are first-class values in Dafny. Function types have the form (T) -> U where T is a comma-delimited list of types and U is a type. T is called the function's domain type(s) and U is its range type. For example, the type of a function

function F(x: int, b: bool): real

is (int, bool) -> real. Parameters are not allowed to be ghost.

To simplify the appearance of the basic case where a function's domain consist of a list of exactly one type, the parentheses around the domain type can be dropped in this case, as in T -> U. This innocent simplification requires additional explanation in the case where that one type is a tuple type, since tuple types are also written with enclosing parentheses. If the function takes a single argument that is a tuple, an additional set of parentheses is needed. For example, the function

function G(pair: (int, bool)): real

has type ((int, bool)) -> real. Note the necessary double parentheses. Similarly, a function that takes no arguments is different from one that takes a 0-tuple as an argument. For instance, the functions

function NoArgs(): real
function Z(unit: ()): real

have types () -> real and (()) -> real, respectively.

The function arrow, ->, is right associative, so A -> B -> C means A -> (B -> C). The other association requires explicit parentheses: (A -> B) -> C.

Note that the receiver parameter of a named function is not part of the type. Rather, it is used when looking up the function and can then be thought of as being captured into the function definition. For example, suppose function F above is declared in a class C and that c references an object of type C; then, the following is type correct:

var f: (int, bool) -> real := c.F;

whereas it would have been incorrect to have written something like:

var f': (C, int, bool) -> real := F;  // not correct

Outside its type signature, each function value has three properties, described next.

Every function implicitly takes the heap as an argument. No function ever depends on the entire heap, however. A property of the function is its declared upper bound on the set of heap locations it depends on for a given input. This lets the verifier figure out that certain heap modifications have no effect on the value returned by a certain function. For a function f: T -> U and a value t of type T, the dependency set is denoted f.reads(t) and has type set〈object〉.

The second property of functions stems from that every function is potentially partial. In other words, a property of a function is its precondition. For a function f: T -> U, the precondition of f for a parameter value t of type T is denoted f.requires(t) and has type bool.

The third property of a function is more obvious—the function's body. For a function f: T -> U, the value that the function yields for an input t of type T is denoted f(t) and has type U.

Note that f.reads and f.requires are themselves functions. Suppose f has type T -> U and t has type T. Then, f.reads is a function of type T -> set〈object〉 whose reads and requires properties are:

f.reads.reads(t) == f.reads(t)
f.reads.requires(t) == true

f.requires is a function of type T -> bool whose reads and requires properties are:

f.requires.reads(t) == f.reads(t)
f.requires.requires(t) == true

6.0. Lambda expressions

In addition to named functions, Dafny supports expressions that define functions. These are called lambda (expression)s (some languages know them as anonymous functions). A lambda expression has the form:

(params) specification => body

where params is a comma-delimited list of parameter declarations, each of which has the form x or x: T. The type T of a parameter can be omitted when it can be inferred. If the identifier x is not needed, it can be replaced by “_”. If params consists of a single parameter x (or _) without an explicit type, then the parentheses can be dropped; for example, the function that returns the successor of a given integer can be written as the following lambda expression:

x => x + 1

The specification is a list of clauses requires E or reads W, where E is a boolean expression and W is a frame expression.

body is an expression that defines the function's return value. The body must be well-formed for all possible values of the parameters that satisfy the precondition (just like the bodies of named functions and methods). In some cases, this means it is necessary to write explicit requires and reads clauses. For example, the lambda expression

x requires x != 0 => 100 / x

would not be well-formed if the requires clause were omitted, because of the possibility of division-by-zero.

In settings where functions cannot be partial and there are no restrictions on reading the heap, the eta expansion of a function F: T -> U (that is, the wrapping of F inside a lambda expression in such a way that the lambda expression is equivalent to F) would be written x => F(x). In Dafny, eta expansion must also account for the precondition and reads set of the function, so the eta expansion of F looks like: