Overview

HTTPS SSH

Boogie2Why3

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.

Contents

  • b2w.jar: a jar distribution 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 b2w.

Installation

Using the jar only requires a Java 8 JRE installed.

To compile from sources, you need a Java 8 JDK and Maven. The source code includes a modified version of Boogieamp used as library, so there are no external dependencies.

Usage

To translate a Boogie file foo.bpl into a WhyML file foo.mlw:

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 (foo.mlw).

Output

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).

Options

The translator supports the following command-line options:

  • -module ModuleName: Set the WhyML translation's module name to ModuleName (default: Translation)
  • -overwrite: If the given output filename exists, overwrite it (default: append the translation)
  • -transform des.bpl: Dump the desugared Boogie input into file des.bpl
  • -disableCC: Ignore limits on axiomatization of unique constants (default: the translator fails if there are more than 100 unique constants of the same type)

License

This software is distributed under GPL v.2. The version of Boogieamp provided as part of the distribution is licensed under Boogieamp's original distribution terms.

More information

For questions and comments contact Michael or Carlo A.