Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Observational implementation of algebraic specifications
Hennicker R. Acta Informatica28 (3):187-230,1991.Type:Article
Date Reviewed: Jul 1 1992

Hennicker takes an observational approach to the construction of implementations of algebraic specifications. An implementation is correct if it satisfies the input/output behavior required by the specification, irrespective of its internal functions. The author presents a proof technique, called context induction, for the verification of implementations. He extends the approach to parameterized observational specifications to support modular construction of implementations.

It has been found that two observational implementations compose vertically (or stepwise). If at least one of the parameterized specifications P1 or P2 is monotonic, then they also compose horizontally (or modularly). For Pi to be monotonic, it must be parameter complete and parameter tolerant, and all observational non-parameter sorts of Pi must be observably monomorphic. Furthermore, for Pi to be parameter complete and parameter tolerant, a necessary and sufficient condition is that it must be parameter protecting (contain no junk and no confusion).

The paper contains useful comparisons with other approaches; excellent, clear examples illustrate the features covered. The paper is fairly long, but the proofs of  theorems  have been placed in the appendix. It would make more sense to the reader if the graphical illustrations for “vertical” and “horizontal” implementations were consistent with the literal meanings of the two words, as in the figures originally proposed by Burstall and Goguen.

Reviewer:  T.H. Tse Review #: CR115359
Bookmark and Share
Specifying And Verifying And Reasoning About Programs (F.3.1 )
Algebraic Approaches To Semantics (F.3.2 ... )
Would you recommend this review?
Other reviews under "Specifying And Verifying And Reasoning About Programs": Date
Programming: the derivation of algorithms
Kaldewaij A., Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780132041089)
Aug 1 1991
An introduction to programming with specifications
Kubiak R., Rudziński R., Sokolowski S., Academic Press Prof., Inc., San Diego, CA, 1991. Type: Book (9780124276208)
Jun 1 1992
A Hoare-like verification system for a language with an exception handling mechanism
Szczepanska D. Theoretical Computer Science 80(2): 319-335, 1991. Type: Article
Nov 1 1991

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2023 ThinkLoud®
Terms of Use
| Privacy Policy