4.1 Sequences🔗

Sequences are a built-in Dafny type that represent ordered collections of elements. They can model data structures such as lists, queues, and stacks. Sequences are immutable value types: once created, their contents cannot be modified. In this respect, they resemble strings in languages like Java or Python, but unlike strings, Dafny sequences can contain elements of any type, not just characters.

seq<int>

A particularly powerful feature of sequences is that they can be freely created and manipulated in specifications and functions.

For example, sortedness can be expressed recursively: if the first element is less than or equal to the rest, and the remainder of the sequence is sorted, then the entire sequence is sorted.

Dafny

predicate sorted2(s: seq<int>){
  0 < |s| ==> (forall i :: 0 < i < |s| ==> s[0] <= s[i]) &&
               sorted2(s[1..])
}

The notation s[1..] slices the sequence, creating a new sequence from the first element to the end. Sequences are immutable, so this does not modify s; it produces a new sequence with the same order of elements, minus the first.

The slice notation is written as:

s[i..j]
where 0 <= i <= j <= |s|

Dafny enforces these index bounds. The slice will contain exactly j - i elements, starting with s[i] and continuing sequentially. The element at index j is excluded, following the same half-open interval convention as regular indexing.

  [] // the empty sequence, which can be a sequence of any type
  [true] // a singleton sequence of type seq<bool>

however, the Z3 theorem prover will not recognize this on its own unless explicitly guided by an assertion (see Lemmas/Induction for details on why this is necessary).

This is a property of each individual element of the sequence. If we wanted to relate multiple elements to each other, we would need to quantify over the indices, as in the first example.

Because sequences support in and !in, this operation gives us an easy way to express the “element not in array” property, turning:

forall k :: 0 <= k < a.Length ==> elem != a[k]

into:

elem !in a[..]

Further, bounds are easily included:

forall k :: 0 <= k < i ==> elem != a[k]

is the same as

elem !in a[..i]

4.2 Sequence APIs🔗

• Creating Sequences:

  Empty sequence

  var s := [];

  With elements

  var s := [1, 2, 3];

  Comprehension sequence (ghost-only)

  ghost var sq := seq(i | 0 <= i < 5, i * i);  // [0,1,4,9,16]

• Length

  var n := |s|;

• Indexing (requires proof 0 <= i < |s|)

  var x := s[i];

• Concatenation

  var s3 := s1 + s2;

• Slicing

  • Slice with start and end indices (0 <= i <= j <= |s|)

    var sub := s[i..j];

  • Prefix (from start up to index i)

    var pre := s[..i];

  • Suffix (from index i to end)

    var suf := s[i..];

• Updating Elements

  Since sequences are immutable, updating creates a new sequence:

  var s2 := s[i := v];

• Membership

  Check if element exists in sequence

  assert 2 in [1,2,3];

• Quantifiers over Sequences

  You can quantify over sequence indices or elements:

  Over indices

  assert forall i :: 0 <= i < |s| ==> s[i] >= 0;

  Over elements

  assert forall x :: x in s ==> x >= 0;

• Properties

  Equality

  assert [1,2] == [1,2];

  Prefix test

  assert s1 <= s2;   // s1 is a prefix of s2

• Examples

  Dafny

  method testSeq{
    var s := [1, 2, 3, 4];
  
    assert |s| == 4;
    assert s[0] == 1;
    assert s[3] == 4;
  
    var sub := s[1..3];   // [2,3]
    assert sub == [2,3];
  
    var pre := s[..2];    // [1,2]
    var suf := s[2..];    // [3,4]
  
    var s2 := s[2 := 99]; // [1,2,99,4]
  
    assert forall i :: 0 <= i < |s| ==> s[i] > 0;
  }

4.3 Set🔗

set<int>

The set formed by the display is the expected set, containing just the elements specified. For the case of the empty set, the type of the variable s1 above is not fully known from its initialization. However, later s1 is compared to s2, so it must have the same type as s2, namely set‘. However, in the example below, there is no such use of ‘s1‘, so the type of ‘s1‘ must be specifically stated in its declaration.

Sets are used in several annotations, including reads and modifies clauses. In this case, they can be sets of a specific object type (like Nodes in a linked list), or they can be sets of the generic reference type object. Despite its name, this can point to any object or array. This is useful to bundle up all of the locations that a function or method might read or write when they can be different types.

When used in a decreases clause, sets are ordered by proper subset. To use sets in decreases clauses, the successive values must be “related” in some sense, which usually implies that they are recursively calculated, or similar.

You can test if a set is empty by comparing it to the empty set (s == {} is true if and only if s has no elements.)

A useful way to create sets is using a set comprehension. This defines a new set by including f(x) in the set for all x of type T that satisfy p(x):

set x: T | p(x) :: f(x)

This defines a set in a manner reminiscent of a universal quantifier (forall). As with quantifiers, the type can usually be inferred. In contrast to quantifiers, the bar syntax (|) is required to separate the predicate (p) from the bound variable (x). The type of the elements of the resulting set is the type of the return value of f(x). The values in the constructed set are the return values of f(x): x itself acts only as a bridge between the predicate p and the function f. It usually has the same type as the resulting set, but it does not need to. As an example:

method m(){
  assert (set x | x in {0,1,2} :: x + 0) == {0,1,2};
}

method m()
{
  assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2};
}

method m(){
  // assert {0*1, 1*1, 2*1} == {0,1,2};  
  // include this assertion as a lemma to prove the next line
  assert (set x | x in {0,1,2} :: x * 1) == {0,1,2};
}

To help Dafny prove this assertion, you can precede it with the assertion assert {0*1, 1*1, 2*1} == {0,1,2};. This lets Dafny figure out both assertions.

method m(){
  assert {0*1, 1*1, 2*1} == {0,1,2};  
  // include this assertion as a lemma to prove the next line
  assert (set x | x in {0,1,2} :: x * 1) == {0,1,2};
}

Without care, a set comprehension could prescribe an infinite number of elements, but a set is only allowed to have a finite number of elements. For example, if you tried writing set x | x % 2 == 0 as the set of all even integers, then you would get an error. (If you really want an infinite set, use the iset type instead. For example, iset x | x % 2 == 0 is legal in ghost contexts.) To ensure that set comprehensions give rise to finite sets, Dafny employs some heuristics. When creating sets of integers, this can be done by bounding the integers in at least one conjunct of the predicate (something like 0 <= x < n). Requiring a bound variable to be in an existing set also works, as in x in {0,1,2} from above.

4.4 Set APIs🔗

• Creating Sets Empty set

  var s := set[];

  Set with elements

  var s := set[1, 2, 3];

  Comprehension set (ghost-only)

  ghost var evens := set x | 0 <= x < 10 && x % 2 == 0;

• Membership

  Check if element is in set

  
  if x in s {
    ...
  }

  Negated membership

  
  if x !in s {
    ...
  }

• Set Operations

  Union

  var u := s1 + s2;

  Intersection

  var i := s1 * s2;

  Difference

  var d := s1 - s2;

• Subset Relations Subset

  assert s1 <= s2;   // s1 is a subset of s2

  Proper subset

  assert s1 < s2;    // s1 is a proper subset of s2

  Superset

  assert s1 >= s2;

• Size and Cardinality

  Cardinality

  var n := |s|;

• Quantifiers over Sets

  You can quantify over elements in sets:

  
  assert forall x :: x in s ==> x >= 0;
  assert exists x :: x in s && x % 2 == 0;

• Examples

  Dafny

  method testSet() {
    var s1 := set[1, 2, 3];
    var s2 := set[3, 4, 5];
  
    assert 1 in s1;
    assert 4 !in s1;
  
    var u := s1 + s2;
    assert u == set[1, 2, 3, 4, 5];
  
    var i := s1 * s2;
    assert i == set[3];
  
    var d := s1 - s2;
    assert d == set[1, 2];
  
    assert |s1| == 3;
    assert s1 < u;}

4.5 Map🔗

In Dafny, a map is an immutable key–value collection. Maps are mathematical objects and cannot be mutated directly. Instead, operations return new maps.

• Creating Maps

  Empty map

  var m := map[];

  With key–value pairs

  var m := map[1 := "one", 2 := "two"];

• Membership and Lookup Check if key exists

  
  if k in m {
    ...
  }

  Lookup value (requires proof that k is in domain)

  var v := m[k];

• Domain and Keys

  Domain (set of keys)

  var dom := m.Keys;  // returns a set of keys

  Values are not directly retrievable as a set, but you can work with them by iterating over keys.

• Adding / Updating Bindings

  Since maps are immutable, updating creates a new map:

  var m2 := m[k := v];

• Removing Bindings

  Remove one key

  var m2 := m - k;

  Remove multiple keys

  var m3 := m - {k1, k2};

• Union override (+):

  Keys in the right map override keys in the left:

  var m3 := m1 + m2;

• Difference (-):

  Remove a set of keys:

  var m2 := m1 - {k1, k2};

• Properties and Quantifiers

  You can reason about maps using Dafny’s quantifiers:

  assert forall k :: k in m ==> m[k] >= 0;

• Complete Example

  Dafny

  method Demo() {
    var m := map[1 := "a", 2 := "b"];
    assert 1 in m;
    assert m[1] == "a";
  
    var m2 := m[3 := "c"];
    assert 3 in m2;
  
    var dom := m2.Keys;
    assert dom == {1,2,3};
  
    var m3 := m2 - 2;
    assert 2 !in m3;
  
    var m4 := m3 + map[2 := "bb"];
    assert m4[2] == "bb";}

4.6 Map APIs🔗

4.7 Arrays🔗

In Dafny, an array is a mutable, fixed-length, heap-allocated sequence of elements. Arrays differ from sequences (seq<T>), which are immutable mathematical objects.

Here’s a rundown of Dafny arrays:

• Declaring Arrays

  
   // declaration
  var a: array<int>;        
  
  // allocate length-5 array of ints, default-initialized to 0
  a := new int[5];           

  new int[5] creates an array of length 5.

  All elements are automatically initialized with the default value of the type (0 for int, false for bool, null for references, etc.).

• Accessing and Assigning

  
  a[0] := 42;                // assign
  var x := a[0];             // read

  Indexing uses [].

  Dafny checks bounds statically when possible, otherwise requires proofs (0 <= i < a.Length).

• Length

  var n := a.Length;         // length property

• Multi-Dimensional Arrays

  var b := new int[3, 4];    // 2D array with dimensions 3x4
  b[2, 3] := 99;

  Multi-dimensional arrays are rectangular, not jagged.

  You can check length along each dimension with .Length(i):

  var rows := b.Length(0);
  var cols := b.Length(1);

• Array Literals (since Dafny 4.0)

  var c := new int[][2, 3];   // 2D array
  c[0,0] := 1;

  Unlike seq, arrays don’t have a simple literal syntax like [1,2,3]. You must allocate with new.

• Converting Between seq and array

  Since arrays are mutable and seq are immutable: Array to Seq:

  ghost var s := a[..];   // turn array into a sequence snapshot

  a[..] creates a sequence of the array’s contents. Seq to Array:

  Dafny

  method SeqToArray(s: seq<int>) returns (a: array<int>)
    ensures a[..] == s
  {
    a := new int[|s|];
    var i := 0;
    while i < |s|
      invariant 0 <= i <= |s|
      invariant forall j :: 0 <= j < i ==> a[j] == s[j]
    {
      a[i] := s[i];
      i := i + 1;
    }
  }

• Arrays in Specifications You can use framing to indicate what arrays are modified:

  Dafny

  method Fill(a: array<int>, v: int)
    requires a != null
    modifies a
    ensures forall i :: 0 <= i < a.Length ==> a[i] == v
  {
    var i := 0;
    while i < a.Length
      invariant 0 <= i <= a.Length
      invariant forall j :: 0 <= j < i ==> a[j] == v
    {
      a[i] := v;
      i := i + 1;
    }
  }

4.8 Summary🔗