Чтение (запись в) файлов в Дафни

Question

Я смотрел на некоторые уроки dafny и не мог найти, как читать (или записывать) простые текстовые файлы. Конечно, это должно быть возможно, верно?

Answer 1

Я подготовил очень простую библиотеку файлового ввода-вывода для 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 так как я на юниксе)

mono fileiotest.exe

который должен напечатать done на успех.

Наконец, вы можете проверить содержимое файла foo.txt! Следует сказать hello world!

---

Несколько последних заметок.

Во-первых, спецификации для операций в fileio.dfy довольно слабые Я не определил никакой логической модели того, что находится на диске, поэтому вы не сможете доказать такие вещи, как "если я прочитаю только что записанный файл, я получу те же данные". (Действительно, такие вещи не соответствуют действительности, за исключением дополнительных предположений о других процессах на машине и т. Д.) Если вы заинтересованы в попытке доказать такие вещи, дайте мне знать, и я могу помочь в дальнейшем.

Во-вторых, подписи дают вам принудительную обработку ошибок. Все операции возвращают логическое значение, говорящее о том, провалились они или нет, а спецификации в основном ничего не сообщают, если вы не знаете, что все операции выполнены успешно. Если это разумная дисциплина программирования для вас, было бы хорошо, если бы Dafny обеспечил ее соблюдение. (Если вы не хотите этого, его легко вынуть.)

Answer 2

Я пытаюсь использовать этот fileiotest.dfy в Dafny 3.1.0. Для этого я исправил отсутствие конструктора в классе HostEnvironment в файле io.dfy, переписав его как:

      class HostEnvironment
{
  constructor{:axiom} () requires false 
  ghost var ok:OkState
}

И fileio.dfy, и fileiotest.dfy прекрасно компилируются в Dafny. Однако, когда я попытался выполнить сборку с помощью fileionative.cs, я получаю следующую ошибку:

      PS C:\Users\jiplucap\Desktop\CTL_Models_and_Proofs\fileio> & "C:\Program Files\dotnet\dotnet.EXE" "c:\Users\jiplucap\.vscode\extensions\correctnesslab.dafny-vscode-1.6.0\out\resources\dafny\Dafny.dll" "c:\Users\jiplucap\Desktop\CTL_Models_and_Proofs\fileio\fileiotest.dfy" /verifyAllModules /compile:1 /spillTargetCode:1 /out:bin\fileiotest fileionative.cs

Dafny program verifier finished with 12 verified, 0 errors
Wrote textual form of target program to fileiotest.cs
Errors compiling program into fileiotest
(9,30): error CS0234: The type or namespace name 'IPEndPoint' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)

(8,28): error CS0234: The type or namespace name 'Sockets' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)

(1888,18): error CS0117: 'FileStream' does not contain a definition for 'Open'

(1900,23): error CS1061: 'FileStream' does not contain a definition for 'Write' and no accessible extension method 'Write' accepting a first argument of type 'FileStream' cam' could be found (are you missing a using directive or an assembly reference?)

Я также пытался использовать конфигурацию /spillTargetCode:3, после чего получаю другую ошибку.

Пожалуйста, есть ли способ (в Dafny 3.1.0) собрать файлы fileiotest.dfy и fileionative.cs, которые могли бы создать файл fileiote.exe?

Answer 3

Попытка скомпилировать (используя csc.exe) два файла fileionative.cs и fileiotest.cs (последний сгенерирован компилятором Dafny) с помощью /r:System.Core.dll /r:System.dll /r:System.Collections.dll /r:System.Runtime.dll /r:System.Numerics.dll вызывал множество ошибок, связанных с недоступностью, например:

      error CS0122: 'System.Collections.Immutable.ImmutableArray<T>' is inaccessible due to its protection level
error CS0053: Inconsistent accessibility: property type 'System.Collections.Immutable.ImmutableArray<T>' is less accessible than property
        'Dafny.Sequence<T>.ImmutableElements'

и другие подобные.

Пожалуйста, может ли кто-нибудь сделать простую программу Dafny, которая читает текстовый файл с использованием внешнего системного метода C# (собственный код для чтения файлов) и возвращает прочитанную строку для использования в программе Dafny?