Prev Up Next
Go backward to Generic Specification and Verification
Friedrich von Henke, in collaboration with
F. Bartels, A. Dold, H. Pfeifer, H. Rueß

Go up to Specification and Verification
Go forward to Mizar Verification of Generic Algebraic Algorithms
Christoph Schwarzweller

Applying Larch/C++ to the STL
Gary Leavens

Larch/C++ is a model-based interface specification language tailored to the specification of C++ programs. As background, some basics of model-based interface specifications were described. By giving an abstract model of container objects, one can state conditions that require elements to remain in a container after they are inserted. Aspects of specification related to templates, the so-called "required interface" can be precisely described by Larch/C++, as shown by a case study involving the set template of the Standard Template Library (STL). This case study revealed some minor documentation problems in the STL, and pointed out some problems in Larch/C++.


Prev Up Next