Executing Formal Specifications with Concurrent Constraint Programming







Deposit Papers 


Wahls, Tim, Leavens, Gary T. and Baker, Albert L. (2000) Executing Formal Specifications with Concurrent Constraint Programming. Technical Report TR97-12c, Department of Computer Science, Iowa State University.

Full text available as:Postscript


Executing Formal Specifications with Concurrent Constraint Programming
Tim Wahls and Gary T. Leavens, and Albert L. Baker
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,
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.

Subjects:All uncategorized technical reports
ID code:00000226
Deposited by:Staff Account on 27 July 2000

Contact site administrator at: