FOZCIL: a framework for converting formal specifications in Object-Z to design contracts in OO programming languages

Formal languages use mathematical notations to capture the software specifications precisely. Design by Contract is a technique used during software implementation to ensure that the software conforms to the specifications. However, there is a semantic gap in the development process between the specifications written in a formal language and the design contracts written in an implementation language. Automated conversion of formal specifications to the design contracts in object-oriented implementation languages can help bridge this gap. Prior work has been done by Sowmiya Ramkarthik and Sherri Sanders to develop such tools for the automated conversions from the Object-Z formal language to the Java and Object PERL implementation languages. However, each tool was custom built to work with only one or two such OO languages. Moreover, there has been significant redundant efforts in the development of each of these tools. FOZCIL (Framework for Object Z Conversion to Implementation Language) is a framework that captures and implements these redundant language-independent features as frozen spots (i.e., the fixed part of the framework) and the language-dependent properties as hot spots (i.e., the extensible part of the framework). When the framework accepts the language-dependent features for a target object-oriented language, it generates a FOZCIL tool instance which, in turn, is capable of accepting Object-Z specifications and converting the specifications to skeletal code with dynamically-checkable design contracts written in that target language.