Formal Semantics and Soundness of an Algorithm
Tim Wahls, Gary T. Leavens · Iowa State University Digital Repository (Iowa State University) · 2000
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.