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

Thumbnail Image
Date
1994-11-18
Authors
Wahls, Tim
Baker, Albert
Leavens, Gary
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Computer Science
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.

Comments

© Tim Wahls, Albert L. Baker, and Gary T. Leavens, 1994. All rights reserved.

Description
Keywords
Citation
DOI
Source
Copyright
Collections