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

FOZCIL (Framework for Object Z Conversion to Implementation Language) captures and implements language-independent features as the fixed part of a framework, and language-dependent properties as the extensible part of a framework. Once the framework has accepted the language-dependent features of a target OO language, it generates a FOZCIL tool instance. The tool instance is capable of accepting Object-Z specifications and of converting those specifications to skeletal code with dynamically-checkable design contracts written in that target language. This provides a significant improvement over existing tools that are custom built to provide automatic conversion from Object-Z only to a specific implementation language. FOZCIL streamlines the process of developing both the reusual language-independent portions and the language dependent portions of such tools.