ISSN:
1573-7535
Schlagwort(e):
formal specification
;
model-based specification
;
precondition
;
postcondition
;
executable specification
;
concurrent constraint programming
;
C++
Quelle:
Springer Online Journal Archives 1860-2000
Thema:
Informatik
Notizen:
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.
Materialart:
Digitale Medien
URL:
http://dx.doi.org/10.1023/A:1026554217992
Permalink
