Search code examples
c#dafnynetmodules

How to call a Dafny method from a C# main program?

I need to feed data to Dafny functions and get their output. For that, I am trying to create a C# program that calls the Dafny functions.

As a test I created a very simple Dafny file:

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

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

My main guess is that I should approach this as a multi-file .NET assembly. For this, I should

  1. generate the C# for the Dafny part of the program with something like dafny /spillTargetCode:1 dafnyModule.dfy
  2. compile that as a module with something like csc /target:module dafnyModule.cs
  3. compile the main C# program with something like csc Main.cs /addmodule:dafnyModule.netmodule.

Step 1 works. However, the csc call in step 2 fails with lots of errors like

$ 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?)
...

My questions are:

  • What is missing in the csc call in step 2 to compile the C# code generated by Dafny?
  • Is this the best way to interface with Dafny code? There are other options I could imagine, though they seem more laborious and error-prone:
    • have the main entry point in Dafny and have it call C# functions to deal with the input/output?
    • have a C# program load at runtime the DLL generated by the Dafny compiler?
  • Actually, I'm not a C# person and I'd prefer to call into Dafny from Java! But I guess Java support is less mature than C# and there's less information. A Java similar question got no answers...

For completeness, I am using Dafny 3.1, dotnet 5.0.104, csc from mono 6.12.0.90 on macOS 11.3.1.

Solution

  • I realized that the Dafny-generated C# code starts with a handful of lines that seem to hint to use dotnet to compile, instead of csc (which I was using because dafny /help mentions it).

    Following that thread I found how to build an application with a library using dotnet.

    And it worked, just by putting the generated C# code where the library is expected and the main app where it should be.

    The whole solution & project thing of dotnet sounds kinda daunting and brings painful flashbacks of Visual Studio on Windows, but it was mercifully straightforward.