Specification Translator: Tool to Translate Specifications for Deductive Verifiers
About the Specification Translator
The Specification Translator is a tool that has been implemented as part of our research titled "Join Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". This tool will translate specifications in verified Java programs from one specification language into another. It supports the tools Krakatoa, OpenJML and VerCors.
The tool takes an annotated Java program and a target tool as input. It will then generate an annotated Java program where the annotations have been translated.
What's included in this artifact?
This artifact contains the following things:
- specification-translator.zip: A directory containing the Specification Translator tool as well as the examples used for the evaluation.
- SpecTranslatorArtifact.ova: A Virtual Machine with the Specification Translator tool, as well as the OpenJML and VerCors verifiers. It also contains the examples used for the evaluation and a script to reproduce the evaluation.
You can use the Virtual Machine to reproduce the evaluation including verification after translation.
If you just want to use the Specification Translator or have a look at the input/output files of the evaluation, then the zip file is sufficient.
The Specification Translator tool is shared under the CC-BY 4.0 license.
The verifiers in the VM, as well as the examples and case studies used for the evaluation, are not licensed under the CC-BY 4.0 but under their original licenses which have been included.
- 2023-06-19 first online, published, posted
- Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
To access the source code, use the following command:
git clone https://data.4tu.nl/v3/datasets/9650e706-6335-4fdd-b669-1a72ac1fe23d.git