The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes

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 with the implicit subset of VDM, this technique is equally applicable to implicit VDM specifications. Standard ML code for the interpreter and the example used in the paper appear in the appendices.