next up previous
Next: Ports Up: Formal Specification of Previous: Some Definitions

PJ Elements

This subsection defines the high-level program elements of PJ. The formal specifications are expressed with our spatial logic. They are inspired by possible spatial relationships between elements and are illustrated with example configurations. Mandatory components of configurations are displayed with a black outline and optionally with a gray background. Optional components have a gray outline and a white background.

We use a top-down approach, i.e. the specifications get more and more complex. We start with general classifications of our basic geometric objects and refine them stepwise to more specialized classifications resembling higher-level language elements. We omit several language elements but present a selection of elements sufficient to understand the example program in Figure 1. It is deliberately intended to demonstrate the reader that this is a non-trivial task ---that requires automatic verification mechanisms--- provided a language with realistic complexity is used.

Volker Haarslev
Wed Jan 31 15:50:43 MET 1996