Implementing Specification Freedoms.
Abstract
The process of converting formal specifications into valid implementations is central in the development of reliable software. As formal specification languages are enriched with constructs to enhance their expressive capabilities and as they increasingly afford specificational freedoms by requiring only a description of intended behavior rather than a prescription of particular algorithms, the gap between specification and implementation widens so that converting specifications into implementations becomes even more difficult. A major problem lies in the mapping of high-level specification constructs into an implementation that effects the desired behavior. In this report, we consider the issues involved in eliminating occurrences of high-level specification-oriented constructs during this process. We discuss mapping issues in the context of our development methodology, in which implementations are derived via the application of equivalence-preserving transformations to a specification language whose high-level expressive capabilities are modeled after natural language. After the general discussion, we demonstrate the techniques on a real system whose specification is written in this language. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1983
- Accession Number
- ADA127576
Entities
People
- Martin Feather
- Philip London
Organizations
- University of Southern California