Object-Z to Perfect Developer
Tim G. Kimber · 2007
Formal specification is the process of creating precise, mathematical models of a proposed system. Such models provide an unambiguous description of the functionality of a system. The specification is the basis for a mathematical proof that implementation satisfies the stated requirements under all circumstances. Object-Z is a widely used object-oriented extension of the Oxford formal specification language Z. A specification is structured in a modular, object-oriented way to facilitate conversion to object-oriented programming languages. Perfect Developer is an object-oriented model verification tool that uses a less well known, less abstract language, Perfect. However, unlike any existing Object-Z tool, Perfect Developer incorporates an automated theorem prover to verify that specifications written with it are sound. This project has gone beyond previous work, and delivered a detailed formal mapping of a large part of the Object-Z language into Perfect. Furthermore, an EBNF grammar defining a textual version of Object-Z is defined. The grammar provides the basis for a translation tool that is capable of fully translating simple, beginner level Object-Z specifications. The translations provide immediate feedback for the user, by clarifying the meaning of Object-Z expressions (e.g. What inputs and outputs does a composite operation actually have? What is its overall precondition?), and allow formal verification by the Perfect Developer tool. This project provides a genuine link between two complementary software engineering techniques, allowing each to enhance the other. i