Я подготовил очень простую библиотеку файлового ввода-вывода для Dafny на основе кода из проекта Ironfleet .
Библиотека состоит из двух файлов: файл Dafny fileio.dfy , объявляющий подписи для различных файловых операций, и файл C # fileionative.cs , который их реализует.
Например, здесь - простая программа Dafny, которая записывает строку hello world! в файл foo.txt в текущем каталоге.
Чтобы скомпилировать, поместите все три файла в один каталог, а затем выполните:
dafny fileiotest.dfy fileionative.cs
который должен напечатать что-то вроде
Dafny 2.1.1.10209
Dafny program verifier finished with 4 verified, 0 errors
Compiled program written to fileiotest.cs
Compiled assembly into fileiotest.exe
Затем вы можете запустить программу (я использую mono, так как я на Unix):
mono fileiotest.exe
, который должен вывести done в случае успеха.
Наконец, вы можете проверить содержимое файла foo.txt! Стоит сказать hello world!
Несколько последних заметок.
Во-первых, спецификации для операций в fileio.dfy довольно слабые. Я не определил никакой логической модели того, что находится на диске, поэтому вы не сможете доказать такие вещи, как «если я прочитаю только что записанный файл, я получу те же данные». (Действительно, такие вещи не соответствуют действительности, за исключением дополнительных предположений о других процессах на машине и т. Д.) Если вы заинтересованы в попытке доказать такие вещи, дайте мне знать, и я могу помочь в дальнейшем.
Во-вторых, подписи do дают вам принудительную обработку ошибок. Все операции возвращают логическое значение, указывающее, провалились они или нет, а спецификации в основном ничего не сообщают, если вы не знаете, что все операции выполнены успешно. Если это разумная дисциплина программирования для вас, было бы хорошо, если бы Dafny обеспечил ее соблюдение. (Если вы не хотите этого, его легко вынуть.)