An Overview of Larch/C++:
Behavioral Specifications
for C++ Modules
 
Gary T. Leavens
 
TR #96-01e
February 1996, revised March, April 1996,
January, July 1997, January 1999

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.

Department of Computer Science
226 Atanasoff Hall
Iowa State University
Ames, Iowa 50011-1040, USA

AN OVERVIEW OF LARCH/C++:
BEHAVIORAL SPECIFICATIONS
FOR C++ MODULES

Gary T. Leavens¹
Department of Computer Science
Iowa State University, Ames, Iowa 50011 USA

January 13, 1999

Abstract:

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are described, with examples. Comparisons are made with other object-oriented specification languages. An innovation in Larch/C++ is the use of examples in function specifications.