OTS/CafeOBJ2JML: An attempt to combine Design By Contract with Behavioral Specifications

TL;DR

This paper explores integrating algebraic specifications with Design by Contract to ensure implementation compliance with formal specifications, combining rigorous design verification with practical implementation guarantees.

Contribution

It proposes a translation method between algebraic specifications and JML to verify that implementations adhere to formal specifications.

Findings

Demonstrates a translation approach between algebraic specs and JML.

Shows that this method helps ensure implementation correctness.

Provides a framework for combining formal verification with practical design by contract.

Abstract

Design by Constract (DBC) has influenced the development of formal specification languages that allow the mix of specification and implementation code, like Eiffel, the Java Modeling Language (JML) and Spec#. Meanwhile algebraic specification languages have been developing independently and offer full support for specification and verification of design for large and complex systems in a mathematical rigorous way. However there is no guarantee that the final implementation will comply to the specification. In this paper we proposed the use of the latter for the specification and verification of the systems design and then by presenting a translation between the two, the use of the former to ensure that the implementation respects the specification and thus enjoy the verified properties.