OTS/CafeOBJ2JML: An attempt to combine Design By Contract with Behavioral Specifications
This addresses the gap between formal verification and practical implementation in software engineering, though it appears incremental as it builds on existing specification paradigms.
The paper tackles the problem of ensuring implementation compliance with formal specifications by proposing a translation between algebraic specification languages and Design by Contract languages, allowing verification of system designs and implementation adherence.
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.