Accession Number:

ADA235698

Title:

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

Descriptive Note:

Final rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Personal Author(s):

• Place, Patrick R.
• Wood, William G.
• Luckham, David C.
• Mann, Walter
• Sankar, Sriram

Report Date:

1991-02-01

Pagination or Media Count:

49.0

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.

Descriptors:

• *ADA PROGRAMMING LANGUAGE
• *SOFTWARE ENGINEERING
• TRANSFORMATIONS
• LOW LEVEL
• LANGUAGE
• CONCRETE
• SPECIFICATIONS
• CASE STUDIES

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE