6 Future Work

  We propose the following agenda to investigate and validate the idea of a grey-box specification language, suitable for engineers. First, we intend to extend an existing programming language, that is, the component implementation language Component Pascal [Obe97], with a few constructs for nondeterministic specification. We expect to need few extra data types, in particular, sequences and sets of objects, a nondeterministic choice statement, and specification statements (Sect. 4.3).

Reusing an existing language has a couple of advantages. Most importantly, we expect to flatten the learning curve and rise the acceptance by programmers using the same language as for component implementation. Further, by making the specification language a true superset of the implementation language, it becomes easy to express the required details. We acknowledge the danger of overspecification, but have not yet a solution at hand to guide the specifiers away from that abyss. Finally, using a complete existing language, accelerates the experiment, because we can concentrate on the essential extensions. Picking a language, with which we have a lot of experience and which is particularly tailored for component programming, is a matter of convenience in the first place.

With the first specification language in place, we intend to run a case study by specifying completely an existing subsystem of Oberon/F [Obe95]. The idea behind that is not to fall into the `toy example trap'.

After this case study, we will probably need to refine our language definition. This refined language should form a sound basis for further research, like tool support or transfer to other environments.