Publication Date

3-2000

Technical Report Number

TR00-02

Subjects

Theory of Computation, Computing Methodologies

Abstract

This paper presents an algorithm for executing formal specifications, and a proof of the soundness of that algorithm. The algorithm executes specifications written in the model-based specification language SPECS-C++ by transforming such specifications to constraint programs. The generated programs use constraint satisfaction techniques to execute specifications written at a high level of abstraction. Denotational semantics techniques are used for both explaining the algorithm and for proving its soundness.

Comments

© 2000 by Tim Wahls and Gary T. Leavens.

Share

COinS