Using a Mix of Languages in Formal Methods: The PET System

The PET project is a formal methods tool for determining necessary conditions for the execution of a path through a concurrent program. The user selects a path by selecting nodes in flow graphs displayed by the graphical user interface. The condition necessary for that path to be executable is then calculated and displayed for the user. This project mixes a graphical user interface with a back-end for the symbolic computation of the path conditions. The graphical user interface is written in TCL/TK and the back-end is written in SML. TCL/TK is a language specifically designed for the rapid construction of graphical user interfaces. SML is higher-order applicative programming language that is very well suited to symbolic computation. Interprocess communication is handled through pipelining strings. Both TCL/TK and SML are fairly good at string manipulation, so the overhead is tolerable. The ease and efficiency of writing each part in a language best suited for each task more than compensates for this additional overhead.