Anna Package Specification Analyzer User Guide.
Abstract
The Anna Package Specification Analyzer is a tool used in developing Ada package specifications annotated with Anna language constructs. The tool constructs a symbolic representation of a package specification, and models different states of that package. Using deductive reasoning on the model, it answers questions about those states, and, if the specification is complete enough, simulates by symbolic execution how an implementation of the package which satisfies the specification would behave, even if no such implementation exists. In consequence, the user has greater confidence in the resulting specification; inconsistencies detected later by run-time checking tools are more likely due to errors in the implementation, rather than in the formal specification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1993
- Accession Number
- ADA311118
Entities
People
- Walter Mann
Organizations
- Stanford University