Keywords: behavioral specification, model-based, behavioral interface specification language, Larch, C++, Larch/C++, Larch Shared Language, VDM, Z, correctness, verification, abstract data type, object-oriented, specification inheritance, example, checkable redundancy, behavioral subtype, informality, tunable formality.
1993 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications -- Languages; F.3.1 [Logics and Meaning of Programs] Specifying and verifying and reasoning about programs -- Assertions, invariants, pre- and post-conditions, specification techniques.
Copyright ©Kluwer Academic Publishers, 1996. Used by permission. An abbreviated and earlier version of this paper is chapter 8 in the book Specification of Behavioral Semantics in Object-Oriented Information Modeling, edited by Haim Kilov and William Harvey (Kluwer Academic Publishers, 1996), pages 121-142.
Gary T. Leavens1
Department of Computer Science
Iowa State University, Ames, Iowa 50011 USA
January 13, 1999