Implementing specification freedoms

AbstractThe 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 paper, we consider the issues involved in eliminating occurrences of high-level specification-oriented constructs during this process. Mapping issues are discussed in the context of our development methodology, in which implementations are derived via the application of correctness-preserving transformations applied 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