An Overview of Larch/C++: Behavioral Specifications for C++ Modules
Date
1999
Authors
Leavens, Gary
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
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. Copyright (c) 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.
Series Number
Journal Issue
Is Version Of
Versions
Series
Academic or Administrative Unit
Type
article
Comments
Rights Statement
Copyright
Funding
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