source code (
.js files), and then potentially runs the result.
to a single A
- ensuring that the names of entities in the translated Dafny code are usable from Java
- ensuring that the types are the same on both sides, which can be tricky as Javascriupt is dynamically typed
The Dafny runtime library
node) requires the Dafny runtime library.
That library is automatically included in the resulting
.js file if
dafny is doing the compilation,
but not if
dafny is only doing translation..
Manually executing Dafny-generation Java code
Suppose a Dafny program is contained in a .dfy files, A.dfy, which contains the Dafny
dafny build --target:js A.dfy
The program is then executed using the command
The combined build-and-run command is
dafny run --target:js A.dfy.