Дафни разница между seq‹int› и массивом‹int›

Последовательность — это (n неизменный) математический список. Массив представляет собой структуру данных, выделенную в куче (изменяемую, потенциально псевдонимную).

Рассмотрим следующие два глупых метода

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;
}

Первый метод использует последовательности. Поскольку последовательности неизменяемы, y обновляется до новой последовательности, а индекс 1 обновляется до значения 7. Как и ожидалось, x остается неизменным на протяжении всего манипулирования y.

Второй метод использует массивы. Поскольку массивы размещаются в куче и могут создавать псевдонимы, когда мы назначаем y := x, мы попадаем в мир, где x и y — два разных имени одного и того же массива в куче. Это означает, что если мы изменим массив через y, мы увидим результаты, отраженные в чтении через x.

Чтобы ответить на ваш второй вопрос, последовательности и массивы уровня Dafny не соответствуют напрямую одноименным вещам уровня SMT. Кодировка Дафни вообще не использует последовательности или массивы SMT-уровня. Вместо этого все кодируется с помощью неинтерпретируемых функций. Я думаю, что это в первую очередь по историческим причинам, и я не знаю навскидку, исследовал ли кто-нибудь серьезно SMT-теорию последовательностей в контексте Дафни. Я могу сказать, что текущая кодировка была довольно тщательно настроена для производительности решателя.