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

             Tim Wahls, Albert L. Baker, and Gary T. Leavens

          Department of Computer Science, 226 Atanasoff Hall
           Iowa State University, Ames, Iowa 50011-1040 USA
   wahls@cs.iastate.edu, baker@cs.iastate.edu, and leavens@cs.iastate.edu


                               Abstract
 
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.