ISSN:
1573-7535
Keywords:
formal specification
;
model-based specification
;
precondition
;
postcondition
;
executable specification
;
concurrent constraint programming
;
C++
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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 is close to that used in nonexecutable specifications. The specification abstractions supported by our execution technique include using quantified assertions 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1026554217992
Permalink
