next up previous
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:

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.

  PJ editor
Figure 4: Window of the PJ editor displaying append




next up previous
Next: Related Work Up: No Title Previous: Verification of Formal




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