Representational Reasoning and Verification
G. J. Doherty, J. Creissac Campos (visit this page for up to date information) & M. D. Harrison
In Formal Aspects of Computing, 12(4):260-277. 2000.
Formal approaches to the design of interactive systems, such as the principled design approach rely on reasoning about properties of the system at a v
ery high level of abstraction. Such specifications typically provide little scope for reasoning about presentations and the representation of information in the pres
entation. Theories of distributed cognition place a strong emphasis on the role of representations in the cognitive process, but it is not clear how such theories ca
n be applied to design.
In this paper we show how a formalisation can be used to encapsulate representational aspects, affording us an opportunity to int
egrate representational reasoning into the design process. We have shown in  how properties over the abstract state place requirements on the presentation if the
properties are to be valid at the perceptual level, and we have presented a model for such properties. We base our approach on this model, and examine in more detail
the issue of verification. Given the widespread consensus that proper tool support is a prerequisite for the adoption of formal techniques, we apply a higher-order
logic theorem prover to the analysis.