Software Engineering Institute Carnegie Mellon

Formal Development of Ada Programs Using Z and Anna: A Case Study

Patrick Place
William G. Wood

Technical Report
CMU/SEI-91-TR-001

This document is unavailable online. Please refer to the instructions for purchasing paper copies of SEI documents.

This report describes a method for the formal development of Ada programs from a formal specification written in Z. ANNotated Ada (Anna) is used as an intermediate language linking the more abstract Z specifications to the concrete Ada program. The method relies on the notion that successive small transformations of a specification are easier to verify than a few large transformations. Essentially the method uses three notations for the representation of the system: an implementation-independent notation for the specification of the system, an implementation-dependent notation for the representation of a lower level specification of the system, and the implementation language. Z and Anna are outlined briefly and examples of transformations are presented. A simple Z specification has been chosen and the transformations presented in the report are transformations of the Z specification into Anna. Conclusions are drawn about the development method presented.