Technical Report Number
Theory of Computation, Computing Methodologies
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.