Dafny difference between seq<int> and array<int>

Question

• I can't seem to tell the difference between dafny's seq<int> and array<int>.
• Do they correspond to their SMT entities? (not sure because arrays in dafny have .Length)

Answer 1

A sequence is a (n immutable) mathematical list. An array is a heap allocated (mutable, potentially aliased) data structure.

Consider the following two silly methods

method Seq()
{
  var x := [1, 2, 3];
  assert x[1] == 2;
  var y := x;
  assert y[1] == 2;
  y := y[1 := 7];
  assert y[1] == 7;
  assert x[1] == 2;
}

method Array()
{
  var x := new int[3](i => i + 1);
  assert x[1] == 2;
  var y := x;
  assert y[1] == 2;
  y[1] := 7;
  assert y[1] == 7;
  assert x[1] == 7;
}

The first method uses sequences. Since sequences are immutable, y gets updated to a new sequence, with index 1 updated to have value 7. As expected, x remains unchanged throughout the manipulation of y.

The second method uses arrays. Since arrays are heap allocated and can alias, when we assign y := x, we enter a world where x and y are two different names for the same array in the heap. That means that if we modify the array via y, we will see the results reflected in reads through x.

To answer your second question, Dafny-level sequences and arrays do not directly correspond to the SMT-level things of the same name. Dafny's encoding does not use SMT-level sequences or arrays at all. Instead, everything is encoded via uninterpreted functions. I think this is primarily for historical reasons, and I don't know off the top of my head whether anyone has seriously investigated the SMT theory of sequences in the context of Dafny. I can say that the current encoding has been pretty carefully tuned for solver performance.