4.3 Abstract Statements

  Specifications can also be expressed in imperative languages, enriched by specification statements and data types like sets and sequences. Specification statements can express things like `set x, y, z such that P holds' [BvW97,Mor90]. Other nondeterministic constructs help to avoid overspecification. The imperative style allows to break down an operation into a sequence of statements.

External calls can be included indicating to the client programmer which calls are made in which sequence and in which states. Hence, it fulfills our requirements for grey-box specifications. However, it is far from trivial to write a specification that includes all external calls and does not overspecify the component.

The notation of abstract statements may range from very mathematical to a syntax similar to implementation languages. In accordance with Sect. 3 we argue for the latter. Using abstract statements, we get a seamless refinement approach without a paradigm change from initial specification to implementation. An implementation only differs from a specification by the absence of nondeterministic constructs and special data types. This seamless approach also allows for intermediate steps, which as in a calculation can reduce errors.

Specifications by abstract statements come close to contracts as proposed by Helm et al. [HG90]. Contracts of Helm et al. specify `behavioral dependencies' between objects in terms of method calls and other constructs. Contracts are expressed in a special purpose language and then have to be linked to the underlying programming language. By contrast, we like to see abstract statements as a moderate extension of the underlying programming language.