Issue No. 09 - September (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.58791
<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>
Larch; Avalon/C++ objects; formal specification; recoverable; atomic; subatomic; nonfunctional properties; complex properties; formal specification.
J. Wing, "Using Larch to Specify Avalon/C++ Objects," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 1076-1088, 1990.