-1

我需要将数据提供给 Dafny 函数并获取它们的输出。为此，我正在尝试创建一个调用 Dafny 函数的 C# 程序。

作为测试，我创建了一个非常简单的 Dafny 文件：

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

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

我的主要猜测是我应该将其作为多文件 .NET 程序集来处理。为此，我应该

  1. 使用类似的东西为程序的 Dafny 部分生成 C#dafny /spillTargetCode:1 dafnyModule.dfy
  2. 将其编译为类似的模块csc /target:module dafnyModule.cs
  3. 用类似的东西编译主 C# 程序csc Main.cs /addmodule:dafnyModule.netmodule。

第 1 步有效。但是，csc第 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?)
...

我的问题是：

  • 步骤 2中的调用中缺少什么csc来编译 Dafny 生成的 C# 代码？
  • 这是与 Dafny 代码交互的最佳方式吗？我可以想象还有其他选择，尽管它们看起来更费力且容易出错：
    • 在 Dafny 中有主入口点并让它调用 C# 函数来处理输入/输出？
    • 有一个 C# 程序在运行时加载由 Dafny 编译器生成的 DLL？
  • 实际上，我不是 C# 人，我更愿意从 Java 调用 Dafny！但我猜 Java 支持不如 C# 成熟，而且信息也较少。Java 类似的问题没有答案...

为了完整起见，我在 macOS 11.3.1 上使用来自 mono 6.12.0.90 的 Dafny 3.1、dotnet 5.0.104、csc。

4

1 回答 1

0

我意识到 Dafny 生成的 C# 代码以几行似乎暗示用于dotnet编译的行开头，而不是csc（我使用它是因为dafny /help提到它）。

在该线程之后，我发现了如何使用dotnet.

它起作用了，只需将生成的 C# 代码放在预期库的位置，并将主应用程序放在应该的位置。

dotnet 的整个解决方案和项目听起来有点令人生畏，并带来了 Windows 上 Visual Studio 的痛苦闪回，但幸运的是，它非常简单。

于 2021-05-29T10:19:51.483 回答