Executing Formal Specifications with Constraint Programming

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

Abstract

Executing Formal Specifications with 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 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, 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,
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.


Subjects:
All uncategorized technical reports


ID code:
00000177
Deposited by:
Staff Account on 18 June 1998





Contact site administrator at: ssg@cs.iastate.edu