Question

How do I write specifications for a lambda expression in a sequence constructor?

Answer

Consider the code

class C {
  var p: (int, int);
}

function Firsts0(cs: seq<C>): seq<int> {
  seq(|cs|, i => cs[i].p.0) // Two errors: `[i]` and `.p`
}

Dafny complains about the array index and an insufficient reads clause in the lambda function. Both of these need specifications, but where are they to be written.

The specifications in a lamda function expression are written after the formal aarguments but before the =>.

The array index problem is solved by a requires clause that limits the range of the index::

class C {
  var p: (int, int);
}

function Firsts0(cs: seq<C>): seq<int> {
  seq(|cs|, i requires 0 <= i < |cs| => cs[i].p.0) // Two errors: `[i]` and `.p`
}

and the reads complaint by a reads clause that states which objects will be read. In this case, it is the objects cs[i] that have their p field read. If the element type of cs were a value type instead of a reference type, this reads clause would be unnecessary.

class C {
  var p: (int, int);
}

function Firsts2(cs: seq<C>): seq<int>
  reads set i | 0 <= i < |cs| :: cs[i]
{
  seq(|cs|, i
    requires 0 <= i < |cs|
    reads set i | 0 <= i < |cs| :: cs[i] => cs[i].p.0)
}