After ten years of visual languages research there is still a strong need for an adequate theoretical foundation of visual languages. In his review [1] Chang identified three main areas of visual languages research on formal methods: formal models of visual languages (e.g. grammar approaches), semantics of visual programming languages (e.g. declarative and logic approaches), and visual reasoning (e.g. spatial and temporal approaches). This paper proposes a new framework for formal methods unifying the above mentioned areas. Our formal method is based on qualitative spatial reasoning and description logics as subsets of first-order predicate logic (see also [2]). We use a single method to formally specify syntax and semantics of visual languages and to reason about language elements. This method is especially suited for completely visual or diagrammatical languages. Even visual query languages are suitable candidates for our approach.
Formal semantics for completely visual languages are less well understood than for other languages (e.g. iconic languages). Therefore, we prove the feasibility of our approach using Pictorial Janus (PJ) [3] as example application. It is important to note that PJ is a real, completely visual language that has been fully implemented. It can be classified as a parallel logic programming language. We think it is furthermore significant that we prove the feasibility and scalability of our approach by choosing a language with sufficient complexity instead of choosing a `toy' language.
Another motivation is that PJ's syntax and static semantics are entirely based on spatial relationships between language elements. PJ's dynamic (operational) semantics can be defined by graphical transformation rules. We are aware of only two other approaches working on formal semantics of completely visual languages. Citrin et al. [4] describe a formal semantics of control for their language VIPR. Cohn and Gooday [5] are also working on formal semantics for Pictorial Janus using their RCC theory.
The remainder of this paper is structured as follows. The next two sections elaborate on our methodology and give an informal introduction to the computational model of Pictorial Janus. They are followed by the main part of this paper dealing with formal semantics of static PJ programs. Afterwards, we summarize the translation process to description logic, our methodology for verification, and the implemented program systems used to perform the actual testing. This paper concludes with a short review of related work and an outlook on future research.