ANNA package specification: case studies

We present techniques of software specification of Ada* software based on the Anna specification language and examples of Ada packages formally specified in Anna. A package specification for an abstract set type is used to illustrate the techniques and pitfalls involved in the process of software specification and development. This specification not only exemplifies good Anna style and specification approach, but has a secondary goal of teaching the reader how to use Anna and the associated set of Anna tools developed at Stanford University over the past six years. The technical report thus aims to give readers a new way of looking at the software design and development process, synthesizing fifteen years of research in the process. *Ada is a registered trademark of the U.S. Government (Ada Joint Program Office)