Formal Development of ADA Programs Using Z and Anna: A Case Study
February 1991 • Technical Report
This 1991 report describes ANNotated ADA (Anna), a method for the formal development of ADA programs from a formal specification written in Z.
Software Engineering Institute
CMU/SEI Report Number
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.