An Overview of Larch/C++: Behavioral Specifications for C++ Modules







Deposit Papers 


Leavens, Gary T. (1997) An Overview of Larch/C++: Behavioral Specifications for C++ Modules. Technical Report TR96-01c, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF


An Overview of Larch/C++:
Behavioral Specifications for C++ Modules
Gary T. Leavens
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.
Copyright (c) Kluwer Academic Publishers, 1996.  Used by permission.
An 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.
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.

Subjects:All uncategorized technical reports
ID code:00000138
Deposited by:Staff Account on 30 January 1997

Contact site administrator at: