Каковы отношения между импортом, включением и проверкой в Дафни?
Я знаю, что один исходный файл Dafny может быть включен в другой, что приводит к текстовой конкатенации файлов до проверки. Но у меня нет четкой ментальной модели взаимосвязей между включениями, импортом и тем, какие файлы проверяются когда. Возможно, эксперт может уточнить. Благодарю.
1 ответ
Это по крайней мере частично документировано в Справочном руководстве Дафни в различных разделах.
Раздел 2.0 обсуждает include:
Включенные файлы также подчиняются грамматике Дафни. Dafny анализирует и обрабатывает транзитивное закрытие исходных файлов и всех включенных файлов, но не будет вызывать верификатор для них, если они не были явно указаны в командной строке.
(акцент мой)
Раздел 3.1 обсуждает importЭто особенность модульной системы Дафни. Вы можете использовать только import внутри модуля, чтобы сделать доступными определения в другом модуле. Обратите внимание, что система модулей Dafny не зависит от того, как файлы хранятся на диске, в отличие от некоторых других языков. Поэтому, если модуль, который вы импортируете, определен в другом файле, вам, возможно, придется включить этот файл, если вы этого еще не сделали.
import не имеет прямого влияния на то, проверен ли импортированный модуль или нет. Модули в других файлах не будут проверены, если их файл не указан в командной строке. Модули в текущем файле всегда проверяются (независимо от того, импортированы они кем-либо или нет).