The code generation is currently broken for Java as there is an error when compiling the Java generated file.
This is due to the use of a lambda in the Dafny code that improbably not fully translated in Java.
report this issue to Dafny.
Another issue is with tail continuations and seem to appear with many targets.
It is a bit more complicated to report and stems from using a recursive computation in a datatype.
There is an example of a Python translation with the problem that I should submit to Dafny.
franck44
commented
8 months ago
The code generation is currently broken for Java as there is an error when compiling the Java generated file. This is due to the use of a lambda in the Dafny code that improbably not fully translated in Java.
Another issue is with tail continuations and seem to appear with many targets. It is a bit more complicated to report and stems from using a recursive computation in a datatype. There is an example of a Python translation with the problem that I should submit to Dafny.