Как вызвать метод Dafny из основной программы C#?

Question

Мне нужно передать данные в функции Dafny и получить их результат. Для этого я пытаюсь создать программу на C#, которая вызывает функции Dafny.

В качестве теста я создал очень простой файл Dafny:

      module myDafnyModule {
    method boolMethod(b: bool) returns (r:bool) {
        return !b;
    }

    function method boolFunctionMethod(b:bool):bool {
        !b
    }
}

Мое главное предположение состоит в том, что я должен подойти к этому как к многофайловой сборке .NET . Для этого я должен

1. сгенерируйте C# для части программы Dafny с чем-то вроде dafny /spillTargetCode:1 dafnyModule.dfy
2. скомпилируйте это как модуль с чем-то вроде csc /target:module dafnyModule.cs
3. скомпилируйте основную программу C# с чем-то вроде csc Main.cs /addmodule:dafnyModule.netmodule.

Шаг 1 работает. Однако вызов на шаге 2 не выполняется с множеством ошибок, например

      $ csc dafnyModule.cs                       
Microsoft (R) Visual C# Compiler version 3.6.0-4.20224.5 (ec77c100)
Copyright (C) Microsoft Corporation. All rights reserved.

dafnyModule.cs(50,28): error CS0234: The type or namespace name 'Immutable' does not exist in the namespace 'System.Collections' (are you missing an assembly reference?)
dafnyModule.cs(1718,40): error CS0246: The type or namespace name 'BigInteger' could not be found (are you missing a using directive or an assembly reference?)
...

Мои вопросы:

• Чего не хватает в csc вызвать на шаге 2 для компиляции кода C#, созданного Dafny?
• Это лучший способ взаимодействия с кодом Dafny? Могу представить себе и другие варианты, хотя они кажутся более трудоемкими и подверженными ошибкам:
  • иметь основную точку входа в Dafny и вызывать функции C# для работы с вводом / выводом?
  • есть ли программа C#, загружающая во время выполнения DLL, сгенерированную компилятором Dafny?
• На самом деле, я не специалист по C# и предпочел бы звонить в Дафни с Java! Но я полагаю, что поддержка Java менее развита, чем C#, и там меньше информации. На подобный Java-вопрос ответов нет ...

Для полноты картины я использую Dafny 3.1, dotnet 5.0.104, csc из mono 6.12.0.90 на macOS 11.3.1.

Answer 1

Я понял, что код C #, сгенерированный Dafny, начинается с нескольких строк, которые, кажется, намекают на использование для компиляции вместо csc (который я использовал, потому что dafny /help упоминает это).

Следуя этой теме, я узнал, как создать приложение с библиотекой, используя dotnet.

И это сработало, просто поместив сгенерированный код C # туда, где ожидается библиотека, а в основное приложение, где он должен быть.

Все решения и проекты dotnet звучат немного устрашающе и вызывают болезненные воспоминания о Visual Studio в Windows, но, к счастью, все было просто.