OBJ-1, A Study in Executable Algebraic Formal Specification.
Abstract
The goal of this research has been to develop a formal and executable algebraic specification language which can be used to specify a variety of application programs, such as database systems, compilers and interpreters for programming languages, and business systems. An advantage of formality in this context is that each specification has a unique unambiguous meaning, so that it is actually meaningful to ask whether or not a given program in fact satisfies a given specification. An advantage of executability is that test cases can be run directly on the specification, to examine properties of programs before they are written, and to help in debugging specifications. The latter is important because large specifications, like large programs, are usually wrong as first written. We have been investigating the utility of a number of potential advantages of the algebraic approach, including the following: Achievement of a high level of modularity in a natural way; Achievement of a high level of abstraction in a natural way; The possibility of executing test cases; User definition of data types and control structures, using any desired syntax, including pre-fix, post-fix, and 'mix-fix' operators, as well as coercions; The specification of error and exception conditions, as well as their handling, and recovery; The use of parameterized abstract modules as a method for structuring specifications; Algorithms for checking consistency and other desirable properties of specifications (e.g., the Knuth-Bendix algorithm); and Provision of a completely rigorous semantics for all these features.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1981
- Accession Number
- ADA104468
Entities
People
- Joseph A. Goguen
- José Meseguer
Organizations
- SRI International