A Two-Tiered Approach to Specifying Programs.
Abstract
Current research in specifications is beginning to emphasize the practical use of formal specifications in program design. This thesis presents a specification approach, a specification language that supports that approach, some ways to evaluate specifications written in that language. The two-tiered approach separates the specification of underlying abstractions from the specification of state transformations. In this approach, state transformations and target programming language dependencies are isolated into an interface language component. All interface specifications are built upon shared language specifications that describe the underlying abstractions. This thesis presents an interface specification language for the CLU programming language and presumes the use of the Larch shared language. This thesis also suggests a number of kinds of analyses that one might want to perform on two-tiered specifications. These are related to the consistency, completeness, and strength of specifications, and are all presented in terms of the theories associated with specifications.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1983
- Accession Number
- ADA133949
Entities
People
- Jeanette Marie Wing
Organizations
- Massachusetts Institute of Technology