Как dafny кодирует проверку условий, связанных с массивами?

Question

Я оцениваю использование Dafny по сравнению с прямым использованием z3 для кодирования проблемы, с которой мы сталкиваемся в моей компании.

При тестировании API z3 я заметил, что существует тип Array, которыйпохоже, очень похоже на то, как Z3 реализует общие функции. Кажется, что нет простого способа рассуждать о длине таких массивов в Z3.

Если мы посмотрим на Дафни, это может легко доказать следующее правильное

method Find(a: array<int>) returns (index: int)
   ensures index == a.Length
{
   index := a.Length;
}

Теперь,для меня вопрос:

Как массив, используемый Дафни, закодирован в Z3?

Скажем, на самом деле Дафни не использует массивы Z3, где я могунайти документацию о том, как Dafny абстрактные вещи, которые не идентифицируют ограниченное количество переменных в Z3 (например, массив)? Тот же вопрос относится к любому объекту, который выделен в куче, использует ли он абстракции сайта размещения или что-то еще?

Answer 1

На самом деле нет ни магии, ни чего-либо «неявного», гарантирующего, что все обращения к массиву находятся в пределах границ. Вы, конечно, можете писать программы Dafny, которые индексируют вне границ, вы просто не можете доказать полезность для них. Дафни заставляет вас делать это, генерируя необходимую проверку «в границах»;но вы все равно должны пройти через доказательство, вставив необходимые аннотации. Это то, что вы ищете? Это также объясняется здесь: https://rise4fun.com/Dafny/tutorialcontent/guide#h27