Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Technical Report

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

  • February 1991
  • By 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.

  • Download

Cite This Report

SEI

Place, Patrick; & Wood, William. Formal Development of ADA Programs Using Z and Anna: A Case Study. CMU/SEI-91-TR-001 . Software Engineering Institute, Carnegie Mellon University. 1991. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313

IEEE

Place. Patrick, and Wood. William, "Formal Development of ADA Programs Using Z and Anna: A Case Study," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-91-TR-001 , 1991. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313

APA

Place, Patrick., & Wood, William. (1991). Formal Development of ADA Programs Using Z and Anna: A Case Study (CMU/SEI-91-TR-001 ). Retrieved January 16, 2019, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313

CHI

Patrick Place, & William Wood. Formal Development of ADA Programs Using Z and Anna: A Case Study (CMU/SEI-91-TR-001 ). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 1991. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313

MLA

Place, Patrick., & Wood, William. 1991. Formal Development of ADA Programs Using Z and Anna: A Case Study (Technical Report CMU/SEI-91-TR-001 ). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313

BibTex

@techreport{PlaceFormalDevelopment1991,
title={Formal Development of ADA Programs Using Z and Anna: A Case Study},
author={Patrick Place and William Wood},
year={1991},
number={CMU/SEI-91-TR-001 },
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11313} }