A method for the formal testing of program visualization tools

Many modern tools support program understanding through the visualization of program structure. Such tools are typically based on a formal theory describing the structure of programs to be visualized such as first order logic, temporal logic, entity relationship models and graph grammars. Two questions arise with such approaches: (a) does the tool correctly abide by the rules of the formalism; and (b) is the formalization itself correct? To address these questions in the context of the visual ClockWorks programming environment, we have developed a method for formally testing both the tool and the theory. This work relies heavily on the use of the PVS (J. Crow et al., 1995) theorem prover. Many of the proofs carried out in this work are easy to prove mechanically, but would be far too tedious to carry out by hand. While this technique was carried out in the context of the ClockWorks tool, the method should be applicable to any visualization system that can be formalized using logic