This repository contains verified bitmask implementations in Dafny.
see LICENSE file.
Reto Achermann
To verify and run the code install Dafny
$ bash tools/install-dafny.sh
The script will install Dafny in the .dafny directory of this repository.
Alternatively, you can also use the Visual Studio Code extension.
To verify the BitMask and BitField modules execute the following command
$ make verify
Generating the code to be used in the library, execute the following command:
$ make generate
This generates C++ code by default, you can change the language by setting
the TARGET environment variable.
$ TARGET=cs make generate
Verifying To verity a Dafny file, you can use the Visual Studio Code plugin or call Dafny on the file to verify using the following script:
$ bash tools/dafny-verify.sh <FILE>
Code Genereation
To generate code execute the following script, where TARGET specifies the language.
$ TARGET=xxx bash tools/dafny-compile.sh <FILE>
where TARGET is one of the languages supported by Dafny. (cpp, cs, python, ...)