Practical Issues in Having a Usable Library of Software Specifications.
Abstract
Though formal specifications of software modules offer much toward the design problems of large software systems, creating formal specifications is very difficult, requiring much upfront effort. This paper examines a common idea for dealing with the high cost of software, but in the context of specification. That idea is a pool or 'library' of specifications, so that it is easy to build on the work of others. Unlike other efforts that have concentrated on technical problems in having such a library, this paper identifies and studies several common sense requirements on such a library being effectively used. Such issues are closer related to human factors than to technical problems; yet these are clearly as critical in use as technical issues. Our conclusions have arisen from two studies. In one, we wrote several module specifications in the form that might appear in a library. The module varied in complexity from a stack to the kernel of a text editor; the text editor specifications ranged in length from 9 to 28 pages including copious comments as in-line documentation. The second study compared portions of the English and formal specifications of KSOS (Ford Aerospace, 1978), the Kernelized Secure Operating System. The paper may be viewed as rather tutorial about writing correct, understandable formal specifications for others to use in their system design.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1981
- Accession Number
- ADA108656
Entities
People
- Ralph M. Weischedel
Organizations
- University of Delaware