Larch/C++ [30] is a model-based specification language that allows the specification of both the exact interface and the behavior of a C++ [12,46] program module.
