Next: Related Work Up: No Title Previous: Verification of Formal

Implementation

The specification of PJ's syntax and semantics of static programs are completed and have been translated to DL notation. The specifications were developed and verified with the help of a fully implemented system (using Common Lisp) that integrates a DL component (Loom [11]) with a special object-oriented editor for PJ programs and an interpreter for textually encoded PJ programs. Our prototype consists of seven major modules:

• Geometry: computes dimension of intersections between rectangular regions, (directed) lines, and points (as start and end points of lines).

• Topology: implements the topological relations of our spatial logic using the geometry module. It also offers a function that computes these relationships between arbitrary sets of objects, using a corresponding decision tree.

• Loom System: implementation of a DL system (i.e. it is a specialized theorem prover) offering powerful reasoning mechanisms. It is used to verify the PJ specifications and to validate them with example programs of PJ. Analyzed example programs are represented as a semantic network based on concept and relation definitions that are defined in the formal specification.

• Editor: offers an object-oriented interface to facilitate easy and quick construction of PJ programs (see Figure 4). The graphical elements currently supported are rectangles, lines, arrows, and text. It also serves as interface to the geometry and topology module and the Loom system.

• DL database: consists of concept and relation definitions (in Loom syntax) which make up the formal specification of PJ.

• Loom interface: integrates the editor and the functional interface of Loom.

• Janus interpreter: executes textually encoded PJ programs. The textual coding of PJ programs uses horn clause syntax. The variable names are randomly generated. The `^' character denotes a tell right for the corresponding variable. For instance, the following code for append was generated and executed by our prototype:

  append([],R21,^R25) :- R25:=R21.
  append([R15|R16],R5,^R20) :- R20:=[R15|R7], append(R16,R5,^R7).

Our test suite consists of a reasonable number of programs implementing simple (e.g. list operations such as append, reverse, etc.) as well as more complex tasks (e.g. queue management, simple bank accounts, etc). Example programs successfully parsed are automatically translated, textually encoded, and executed by our interpreter. The iterative process of developing formal semantics specifications and verifying them with example programs turned out to be very fruitful.

  
Figure 4: Window of the PJ editor displaying append

Next: Related Work Up: No Title Previous: Verification of Formal