The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.09 - September (1990 vol.16)
pp: 1076-1088
ABSTRACT
<p>A formal specification of three base Avalon/C++ classes - recoverable, atomic, and subatomic - is given. Programmers derive from class recoverable to define persistent objects, and from either class atomic or class subatomic to define atomic objects. The specifications, written in Larch, provide the means for showing that classes derived from the base classes implement objects that are persistent or atomic and thus exemplify the applicability of an existing specification method to specifying nonfunctional properties. Writing these formal specifications for Avalon/C++'s built-in classes has helped to clarify assumptions explicit, and to characterize complex properties of objects.</p>
INDEX TERMS
Larch; Avalon/C++ objects; formal specification; recoverable; atomic; subatomic; nonfunctional properties; complex properties; formal specification.
CITATION
J.M. Wing, "Using Larch to Specify Avalon/C++ Objects", IEEE Transactions on Software Engineering, vol.16, no. 9, pp. 1076-1088, September 1990, doi:10.1109/32.58791
15 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool