The Dafny compilation process translates Dafny programs into target language
source code, in particular a
.go file, compiles the result, and then potentially runs the result.
The Dafny-to-Go compiler writes out the translated files of a file A
to a folder A
-out option can be used to choose a
different output folder. The file A
.dfy is translated to A
which is placed in the output folder along with helper files.
If more than one
.dfy file is listed on the command-line, then the output
folder name is taken from the first file, but just
.go file is written ithat combines the user source files,
along with additional System and library
A multi-language program that combines Dafny and Go code “just” needs to be sure that the translated Dafny code fits in to the Go code. There are two aspects to this:
- ensuring that the names of entities in the translated Dafny code are usable from Go
- ensuring that the types are the same on both sides
The Dafny runtime library
The step of compiling Go files requires the Dafny runtime library. That library is automatically included in the output files if
dafny is doing the compilation,
but not if
dafny is only doing translation.
Manually executing Dafny-generated Go code
Suppose a Dafny program is contained in a
A.dfy, which containingthe Dafny
Main method. One can build the corresponding Go program (without running it) using this command:
dafny build --target:go A.dfy
The compiled program is then executed using the command
(cd A-go; GO111MODULE=auto GOPATH=\pwd` go run src/A.go)`
Alternatively the build and run steps can be combined:
dafny run --target:go A.dfy
Combining Go and Dafny source files
The dafny tool is not yet able to automatically combined Go and Dafny source files.