Различные выходные данные компиляции Dany для предложения свидетеля при компиляции с использованием VSC и автономного компилятора

Я подозреваю, что процитированный вами абзац, вероятно, относится только к контексту проверки, а не к скомпилированному контексту. Это означает, что если вы пытаетесь проверить различные свойства, компилятор доберется до этого значения по умолчанию для инициализации при проверке операторов. Компилятор проверки проверяет значения, чтобы убедиться, что свойства допустимы.

Однако, если вы добавите утверждение в функцию.

method Main()
{ 
  var n:Pos;
  assert n == 1;
  print "n:",n;
}

Вы можете видеть, что Дафни не предполагает, что 1 является значением переменной по умолчанию.

Объяснение

Проблема, с которой вы столкнулись, заключается в том, что правила определенного назначения Dafny изменились в Dafny 4.0, см. https://github.com/dafny-lang/ide-vscode/wiki/Quick-migration-guide-from-Dafny-3. .X-to-Dafny-4.0#определенное-назначение.

Когда вы используете VS Code, вы получаете новое, более строгое правило. Вы также получаете это более строгое правило в новом интерфейсе командной строки (в этом интерфейсе командной строки используются такие глаголы, как verify и run). Например, вы увидите ту же ошибку, если попытаетесь

dafny verify test.dfy

Однако устаревший интерфейс командной строки (то есть без использования такого глагола) по-прежнему использует старое смягченное правило определенного назначения. Следовательно, команда

dafny test.dfy

не дает никакой ошибки.

Что делать

Обычно ответом на ошибку определенного присваивания является ручная инициализация переменной. Однако, если вы согласны с тем, что Дафни выбирает произвольное значение для локальной переменной n, вы можете использовать присваивание n := *;. Поскольку Pos является типом с автоматической инициализацией (то есть компилятор знает, что тип непустой, и знает какой-то способ инициализации переменной), присваивание n := *; будет удовлетворять правилу определенного присваивания.

Больше информации

Если вам нужно старое правило (которое я не рекомендую, если только у вас нет устаревшего кода Dafny, который вы пытаетесь перенести в Dafny 4.0), вы можете использовать опцию --relax-definite-assignment с новым интерфейсом командной строки. Если вы хотите строгое правило с устаревшим интерфейсом командной строки, используйте опцию /definiteAssignment:4.

Последнее замечание. Предложение, которое вы цитируете из справочного руководства, сбивает с толку. (Я сообщу об ошибке, чтобы исправить ее.) Предложение witness не объявляет значение по умолчанию. Он только объявляет примерное значение, которое используется в качестве доказательства того, что существует значение, которое компилятор может использовать для инициализации переменных. Язык не гарантирует, что вы получите именно это значение. Показательный пример: верификатор пометит второе утверждение в следующем коде как ошибку, потому что нет гарантии, что выбранное значение будет 1.

type Pos = i: int | i > 0 witness 1

method Main()
{ 
  var n: Pos := *;
  assert n > 0; // yes, the verifier proves this assertion
  assert n == 1; // error: variable n can be any value of type Pos, not necessarily 1
  print "n:", n;
}