Formal Development of Ada Programs Using Z and Ana: A Case Study
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 specifications has been chosen and the transformations presented in the report are transformations of the Z specifications into Anna. Conclusions are drawn about the development method presented. This report describes recent work performed by the formal specifications project of the Software Engineering Institute in conjunction with members of the Anna project at Stanford University.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1991
- Accession Number
- ADA235698
Entities
People
- David C. Luckham
- Patrick R. Place
- Sriram Sankar
- Walter Mann
- William G. Wood
Organizations
- Carnegie Mellon University