article · Iowa State University Digital Repository (Iowa State University) · 1994

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

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

Cited by 7Open access

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.

Cite this paper

APA 7

Wahls, T., Baker, A. L., & Leavens, G. T. (1994). The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes. Iowa State University Digital Repository (Iowa State University).

MLA 9

Wahls, Tim, et al. “The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes.” Iowa State University Digital Repository (Iowa State University), 1994.

Chicago

Wahls, Tim, Albert L. Baker, and Gary T. Leavens. 1994. “The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes.” Iowa State University Digital Repository (Iowa State University).

Harvard

Wahls, T., Baker, A.L. and Leavens, G.T. (1994) ‘The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes’, Iowa State University Digital Repository (Iowa State University).

BibTeX

@article{wahls1994direct,
  title = {{The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes}},
  author = {Wahls, Tim and Baker, Albert L. and Leavens, Gary T.},
  journal = {Iowa State University Digital Repository (Iowa State University)},
  year = {1994}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.