prodrelworks/dafny-image repository overview

⁠Dafny

Dafny rise4fun⁠ is an imperative compiled language that supports formal specification through preconditions, postconditions, loop invariants and loop variants. It uses boogie as the intermediate verification language.

⁠Dafny Image

Used to run dafny code .dfy file using a docker image of dafny executeable.
Comes pre-installed with z3 (windows), llvm, gcc, g++. mono-complete, boogie.exe (windows) & dafny.

⁠Running Docker Image

Assuming there is a file exercise-13.dfy in the present working directory pwd. It is mapped to a folder tempin the docker filesystem.

$ docker run --rm  -v $(pwd):/temp -it prodrelworks/dafny-image:latest
$ cd /temp/
$ /dafny-progs/dafny/Binaries/dafny /compileTarget:js /spillTargetCode:1 exercise-13.dfy
$ node exercise-13.js

On Windows

> docker run --rm  -v ${pwd}:/temp -it prodrelworks/dafny-image:latest