Publication Date

5-2000

Technical Report Number

TR97-12b

Subjects

Computing Methodologies, Software, Theory of Computation

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.

Comments

Copyright © 1997, 1998, 2000, Tim Wahls, Gary T. Leavens, and Albert L. Baker.

Share

COinS