How to link Dafny code with a C# assembly

Question

I'm trying to build and run an example program by James Wilcox that combines Dafny code and C# code. I'm using mono on a Mac. The build command in that answer doesn't work for me:

$ dafny fileiotest.dfy fileionative.cs
Dafny 3.0.0.20820

Dafny program verifier finished with 4 verified, 0 errors
Compiled program written to fileiotest.cs
Errors compiling program into fileiotest
(8,24): error CS0234: The type or namespace name 'Net' does not exist in the namespace 'System' (are you missing an assembly reference?)

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

(28,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(43,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(58,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(73,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(87,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

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

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

How can I "add a reference to assembly"? Can it be done on the dafny command line?

Answer 1

I don't think you need the System.Net imports for the file example, so you can just delete those includes from the fileionative.cs file.

I am not sure about the TextWriter errors, but if you can figure out what assembly reference you need, you can add it to the command line by running csc manually. This is what worked on my machine:

dafny fileiotest.dfy /spillTargetCode:3 /compile:0
csc fileionative.cs fileiotest.cs /r:System.Core.dll /r:System.dll /r:System.Collections.Immutable.dll /r:System.Runtime.dll /r:System.Numerics.dll

The /spillTargetCode:3 argument tells Dafny to output the fileiotest.cs file. The /compile:0 line tells it to skip the final compilation step, so you can do it manually.

Finally, for your last two errors:

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

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

I believe this is a Dafny version mismatch thing with the conventions expected of Dafny-generated C# code. The fileionative.cs from the other stack overflow answer uses a namespace called __default, but the Dafny-generated fileiotest.cs uses a namespace called _module. So you just need to change fileionative.cs to use the correct namespace _module instead.