Executing Formal Specifications with Concurrent Constraint Programming by Tim Wahls and Gary T. Leavens, and Albert L. Baker Abstract We have implemented a technique for execution of formal, model-based specifications. The specifications we can execute are written at a level of abstraction that is close to that used in nonexecutable specifications. The specification abstractions supported by our execution technique include using quantified assertions to to directly construct post-state values, and indirect definitions of post-state values (definitions that do not use equality). Our approach is based on translating specifications to the concurrent constraint programming language AKL. While there are, of course, expressible assertions that are not executable, our technique is amenable to any formal specification language based on a finite number of intrinsic types and pre- and postcondition assertions. To appear in Automated Software Engineering, 7(4), 2000. Copyright (c) 2000, Kluwer Academic Publishers. Keywords: Executable specifications, constraint programming, SPECS-C++ AKL, behavioral interface specification, C++, model-based specification, precondition, postcondition, formal specification, prototyping, constraint solving, constraint satisfaction, sets, unions, sequences, tuples, objects, first-order predicate calculus. 1997 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications --- Languages, reliability, tools, SPECS-C++; D.2.7 [Software Engineering] Distribution and Maintenance --- Documentation; D.2.m [Software Engineering] Miscellaneous --- Rapid prototyping; D.3.2 [Programming Languages] Language Classifications --- Nonprocedural languages, Very high-level languages; D.3.4 [Programming Languages] Processors --- Interpreters; Very high-level languages; F.3.1 [Logics and Meaning of Programs] Specifying and verifying and reasoning about programs --- Assertions, pre- and post-conditions, specification techniques.