Report Number: CSL-TR-90-438
Institution: Stanford University, Computer Systems Laboratory
Title: A Methodology for Formal Specification and Implementation of Ada Packages Using Anna
Author: Madhav, Neel
Author: Mann, Walter
Date: August 1990
Abstract: This paper presents a methodology for formal specification and prototype implementation of Ada packages using the Anna specification language. Specifications play an important role in the software development cycle. The methodology allows specifiers of Ada packages to follow a sequence of simple steps to formally specify packages. Given the formal specification of a package resulting from the methodology for package specifications, the methodology allows implementors of packages to follow a few simple steps to implement the package. The implementation is meant to be a prototype. This methodology for specification and implementation is applicable to most Ada packages. Limitations of this approach are pointed out at various points in the paper. We present software tools which help the process of specification and implementation.