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

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

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 September 20, 2017, 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} }