Translating Invariant Proofs between Spec# and JML

Abstract

This work aims at relating the methodologies Spec] and JML rely on by defining a semantics-preserving translation scheme between Spec] and JML. This translation shall map a Spec] program, verifiable in the Spec] methodology, to a semantic equivalent JML program, verifiable in the JML methodology, and vice versa.