How to get a C# program from a dafny program?

Question

I cannot see how to get a C# program from a dafny program.

I've downloaded dafny in Visual Studio Code and also downloaded C#. I have a program in dafny and can right-click on the program and choose Compile and Run, but I'd like to generate a C# program as is shown in this video (8:46) : https://www.youtube.com/watch?v=99TjfvyP1z0.

function method Fib (n : int) : int
  decreases n
{
   if n < 2 then n else Fib (n - 2) + Fib (n - 1)
}

method Main ()
{
  print Fib (3);
}

score 5 · Answer 1 · answered Apr 05 '19 at 16:18

Internally, Dafny's .NET compiler generates C# code that it calls the C# compiler to turn into an executable .NET program (or a .dll). You ask Dafny to output this C# program. That's done using the command-line switch /spillTargetCode:1. In comments at the top of the generated C# program, you'll see what command-line switches to pass to the C# compiler to compile that C# program directly.

If you just want to run your Dafny program, there's no need to ever look at the C# code. Either just invoke Dafny with /compile:1 (which is the default) and then run the resulting .exe file, or invoke Dafny with /compile:3 to verify, compile, and run your program.

I've described these options as if you're running Dafny from the command line. There's also some way to add these command-line switches in the Settings for Dafny in VS Code.

If you want to interface your Dafny other C# code, you can use the {:extern} attribute on Dafny methods and other Dafny declarations. If do you that, then simply add your own .cs files on the command line when invoking Dafny. For examples, search for "extern" in the files in Dafny's test suite.

A recent addition to Dafny (so recent it isn't yet available in the binary release of Dafny, but you can get it right away if you build Dafny from source yourself) are compilers for JavaScript and Go. Select these compilers with the command-line switch /compileTarget.

Rustan

I use Dafny in VS Code. What's the way to generate the C# codes in VS Code? — LyX2394, Apr 10 '19 at 01:11
I've used these command-line switches in the terminal in VS Code, but I haven't had any success. I've instead had this error message: Windows PowerShell Copyright (C) Microsoft Corporation. All rights reserved. /compile:3 : The term '/compile:3' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name, or if a path was included, verify that the path is correct and try again. At line:1 char:1 + /compile:3 + ~~~~~~~~~~ — LyX2394, Apr 15 '19 at 18:58
That error message doesn't sound like it's coming from Dafny. Is your path to the Dafny executable set up correctly? (Under Windows, the executable is called `Dafny.exe`. On other platforms, you run it under Mono, like `mono Dafny.exe`, or use the script `dafny` that is part of the Dafny binary distribution. — Rustan Leino, Apr 17 '19 at 17:34
Currently, Dafny VSCode does not support passing command-line switches to the compile command. However, you could open a feature request (or pull request) here: https://github.com/DafnyVSCode/Dafny-VSCode/issues — Rustan Leino, Apr 17 '19 at 17:34

How to get a C# program from a dafny program?

1 Answers1