Wahls, Tim, Leavens, Gary T. and Baker, Albert L. (1997) Executing Formal Specifications with Constraint Satisfaction. Technical Report TR97-12, Department of Computer Science, Iowa State University.
Executing Formal Specifications with Constraint Satisfaction
Tim Wahls and Gary T. Leavens and Albert L. Baker
We have implemented an execution technique for formal specifications,
which is based on constraint satisfaction techniques. These
techniques allow one to execute model-based specifications written at
a high level of abstraction. Such specifications are comparable to
that of specifications written without executability in mind, because
quantified assertions that are bounded are executable.
The main technique for executing assertions is an adaptation of
constraint solving to the domains of interest in model-based
specification: sets, unions, sequences, tuples and objects. We
describe in detail how to do constraint satisfaction for these
domains. We also describe how these techniques are used in executing
specifications written using first-order predicate calculus assertions
over such domains.
Copyright (c) Tim Wahls, Gary T. Leavens, and Albert L. Baker, 1997.
Keywords: formal specification, model-based specification, executable
specification, prototyping, constraint solving, constraint
satisfaction, sets, unions, sequences, tuples, objects, first-order
predicate calculus, constraint logic programming, C++.
1997 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications --- Languages, reliability, tools;
D.2.m [Software Engineering]
Miscellaneous --- Rapid prototyping;
D.3.2 [Programming Languages]
Language Classifications --- Nonprocedural languages,
very high-level languages;
F.3.1 [Logics and Meaning of Programs]
Specifying and verifying and reasoning about programs ---
Assertions, pre- and post-conditions,
Contact site administrator at: firstname.lastname@example.org