This repository contains
b2w, a translator from Boogie programs to WhyML programs. The translation scheme
b2w implements is described in the paper "Why Just Boogie? Translating Between Intermediate Verification Languages", available at http://arxiv.org/abs/1601.00516.
jardistribution of the translator
boogie2why3: the source code of the translator
paper_examples: the three examples discussed in the paper, with their translations as produced by
jar only requires a Java 8 JRE installed.
To translate a Boogie file
foo.bpl into a WhyML file
java -jar /path/to/b2w.jar foo.bpl foo.mlw
The translation is printed on
stdout if no output filename is provided as second argument (
Every run of
b2w may return with exit status:
0: the translation was successful and produced a correct output.
5: the translation encountered partially supported features and produced warnings. The output may be incomplete, but if it typechecks successfully it preserves correctness.
10: the translation encountered unsupported features and produced errors. The output may be incorrect (if it was produced at all).
The translator supports the following command-line options:
-module ModuleName: Set the WhyML translation's module name to ModuleName (default:
-overwrite: If the given output filename exists, overwrite it (default: append the translation)
-transform des.bpl: Dump the desugared Boogie input into file
-disableCC: Ignore limits on axiomatization of
uniqueconstants (default: the translator fails if there are more than 100
uniqueconstants of the same type)