DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Formal Development of Ada Programs Using Z and Ana: A Case Study
CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST
Pagination or Media Count:
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.
APPROVED FOR PUBLIC RELEASE