search menu icon-carat-right cmu-wordmark

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

February 1991 Technical Report
Patrick R. Place, William G. Wood

This 1991 report describes ANNotated ADA (Anna), a method for the formal development of ADA programs from a formal specification written in Z.

Publisher:

Software Engineering Institute

CMU/SEI Report Number

CMU/SEI-91-TR-001

Abstract

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.