The Dafny compilation process translates Dafny programs into target language source code.

For a simple Dafny-only program, the translation step converts a A.dfy file into A.cs; the build step then produces a A.dll, which can be used as a library or as an executable.

A multi-language program that combines Dafny and C# code “just” needs to be sure that the translated Dafny code fits in to the C# code. There are two aspects to this:

• ensuring that the names of entities in the translated Dafny code are usable from C#
• ensuring that the types are the same on both sides

Calling C# from Dafny

Calling a C# method from Dafny requires declaring a shim in Dafny that gives a name and types that can be referenced by Dafny code, while still having the same name as in the C# code.

For example, suppose we want to call a C# method Demo.p(). In Demo.cs we have

using System;
using System.IO;
public class Demo {
  public static void p() { Console.WriteLine("Hi!"); }
}

In Demo1.dfy we write,

module M {
  method {:extern "Demo", "p"} p() 
  method Main() {
    p();
  }
}

Note that the declaration of p() has no body; it is just a declaration because the actual implementation is in C#. Its extern attribute has two arguments: the fully-qualified class name and the method name.

Then the above can be built with dafny build --target:cs Demo1.dfy Demo.cs and then run as a dotnet program with dotnet Demo1.dll

Or, in one build-and-run step, dafny run Demo1.dfy --input Demo.cs

Calling non-static C# methods from Dafny

If the C# methods to be called are not static, then a receiver object must also be created and shared between C# and Dafny. The following example shows how to do this.

In a Demo1a.dfy file:

module {:extern "demo"} M {
  method {:extern "demo.Demo", "newDemo"} newDemo() returns (r: Demo )
  class {:extern "Demo" } Demo {
    method {:extern "demo.Demo", "p"} p()
  }
}
module MM {
  import opened M
  method Main() {
    var d: Demo := newDemo();
    d.p();
  }
}

In a Demo1x.cs file

using System;
using System.IO;

namespace demo {
  public class Demo {
    public static Demo newDemo() { return new Demo(); }
    public void p() { Console.WriteLine("Hi!"); }
  }
}

In the C# file there are two methods: a static one that returns a new instance of the Demo class, and a non-static method that does something useful. In the .dfy file we have a module M that has an extern name corresponding to the namespace of the C# class, a class declaration that associates the Dafny class Demo with the C# class demo.Demo, an instance method declaration that connects the Dafny method M.Demo.p to the C# method demo.Demo.p, and a static Dafny method M.newDemo connected to the static C# method demo.Demo.newDemo. The extern declaration for class Demo is actually not necessary if the Dafny and C# classes have the same name and the Dafny class is contained in a module whose extern name is the same as the C# namespace.

Then the Main method in the Dafny file calls the two Dafny methods, which are translated to the two C# methods. The combination is built and run using dafny run --target:cs Demo1a.dfy --input Demo1x.cs

Calling Dafny from C#

The simplest way to call a Dafny method from C# is to place the Dafny method in a class within a module. The module should be attributed as {:extern "M"}, where M is the desired name of the C# namespace in which the C# class resides. There is no need to give an extern name to the class or method.

In Demo2.dfy:

module {:extern "MM"} MM {
  class C {
    static method p() {
      print "Hello, World\n";
    }
  }
}

module MMM {
  class Demo2x {
    static method {:extern "Demo2x", "M"} M()
  }
}

method Main() { MMM.Demo2x.M(); }

In Demo2x.cs:

public class Demo2x {
  public static void M() {
    MM.C.p(); // Calls p() in Dafny
  }
}

The above program is run with dafny run --target:cs Demo2.dfy --input Demo2x.cs.

(Note that having Dafny invoke Main in the .cs code is not yet operational.)

Types

If the C# method has input arguments or an output value, then the Dafny declaration must use corresponding types in Dafny: Here, T' for a type parameter T indicates the C# type corresponding to a Dafny type T.