[Index]

C. Direct control of FDR

It is possible to use FDR 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 FDR 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.

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

[ < ]

[ > ]

[ << ]

[ Up ]

[ >> ]

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.