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

Wahls, Tim, Baker, Albert L. and Leavens, Gary T. (1994) The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes. Technical Report TR94-02b, Department of Computer Science, Iowa State University.

Abstract

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.


Subjects:
All uncategorized technical reports


ID code:
00000068
Deposited by:
Staff Account on 18 November 1994





Contact site administrator at: ssg@cs.iastate.edu