Formal Semantics and Soundness of an Algorithm for Translating
     Model-based Specifications to Concurrent Constraint Programs
				  by
		    Tim Wahls and Gary T. Leavens

			       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 concurrent
constraint programs.  This approach can 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,
	   SPECS-C++;
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
       --- Documentation;
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,
        specification techniques;
F.3.1 [Logics and Meanings of Programs] Semantics of Programming Languages
       --- Denotational semantics.


Copyright (c) 2000 by Tim Wahls and Gary T. Leavens.