C Direct control of FDR

It is possible to use FDR2 without using the supplied graphical interface. The current GUI is built using Tcl/Tk and drives a Tcl interpreter with a number of added commands.

This appendix documents three possible approaches to driving FDR2 without using the GUI.

• A batch interface performing all the assertions in a script.
• A simple Tcl interface providing procedures which can return the results of assertions.
• The underlying Tcl object model used to support the GUI and the two simpler interfaces.

All the interfaces described here are provided on the same terms as the SML interface to FDR1: they are currently stable, but may change significantly between major revisions of FDR. In particular, the object model is subject to revision without notice, and is documented only to the extent needed by various customers: those who require additional functionality are invited to contact Formal Systems and discuss their requirements in detail.

• Batch interface
• Script interface
• Object model

(In all cases the FDR2 engine will generate a certain amount of noise on standard error. This can be redirected into a file if required.)

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.