Wahls, Tim and Leavens, Gary T. (2000) Formal Semantics and Soundness of an Algorithm. Technical Report TR00-02, Department of Computer Science, Iowa State University.
Formal Semantics and Soundness of an Algorithm
for Translating Model-based Specifications to Constraint Programs
Tim Wahls and Gary T. Leavens
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.
Keywords: Executable specifications, behavioral interface
specification language, formal specification, prototyping, translation
of specifications to constraints, constraint programming, soundness,
denotational semantics, model-based specification, formal methods,
precondition, postcondition, SPECS-C++.
1999 CR Categories:
D.2.1 [Software Engineering] Requirements/Specifications
--- Rapid prototyping, languages, theory, tools;
D.2.4 [Software Engineering] Software/Program Verification
--- Formal methods, programming by contract, reliability, tools,
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
D.3.2 [Programming Languages] Language Classifications
--- Constraint and logic languages,
nonprocedural languages, very high-level languages;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, pre- and post-conditions,
F.3.1 [Logics and Meanings of Programs] Semantics of Programming Languages
--- Denotational semantics.
Copyright (c) 2000 by Tim Wahls and Gary T. Leavens.
Contact site administrator at: firstname.lastname@example.org