The techniques described in this paper (e.g. in Subsections 3.5 and 4.6) have been implemented in F⭑ (master branch). F⭑ is open source software, it is available on Github, and it is known to work well on Windows, Mac, and Linux. Instructions for building from source are available at INSTALL.md.
As a backup plan we have also prepared a Linux VM with everything that is needed to build F⭑ from source and with a working binary, everything as of October 2016 at the time of the artifact evaluation. It can be downloaded as an OVA archive, or just the disk image in VMDK format (xzipped). The user name is 'edsger' and the password is 'monad'. To use this VM you currently need to open a terminal and type:
$ cd ~/FStar/examples/dm4free $ make
After this you can try out the various examples below
by running fstar.exe NameOfExample.fst.
The VM has the emacs and vim editors installed with
F⭑-specific modes installed.
In case you wish to update F⭑ to the very latest GitHub version
you can optionally do this:
$ cd ~/FStar $ git pull $ make -C src ocaml-fstar-ocamlSome notes on the implementation of Dijkstra monads for free in F⭑ are available at various places.
The examples from Section 2 are also available in the F⭑ repo and work as expected. Here is in which file each of the example lives: