Executable specification languages may be the key to more widespread use of formal methods in software production. However, the expressiveness of executable specification languages is typically much less than that of non-executable specification languages such as VDM or Z. Thus, specifiers are forced to work at a lower level of abstraction to gain the advantage of executability. Additionally, specifications are typically made executable by translating them to a programming language, so errors in the specification can only be detected as errors in the resulting code. This paper presents a technique for directly executing specifications written in SPECS-C++, a model-based specification language for C++ classes. As SPECS-C++ has much in common...