Executing Formal Specifications with Constraint Programming







Deposit Papers 


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

Full text available as:Postscript
Adobe PDF


Executing Formal Specifications with 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 has not previously been supported in
executable specification languages. The specification abstractions
supported by our execution technique include quantified assertions
that reference 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.
Copyright (c) 1997, 1998, 2000, Tim Wahls, Gary T. Leavens, and Albert L. Baker
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:00000218
Deposited by:Staff Account on 15 May 2000

Contact site administrator at: