Citation entries (in BibTeX format) may be found here.
In many domain specific languages diagrammatic notation is used because it conforms to notations used by domain specialists before the deployment of programmable components. The aim is to lessen the possibility of error by changing as little as possible. However the switch to programmable components often means a radical change in the details of the implementation. Such changes can mean that the domain experts' interpretation of the notation diverges significantly from the actual implementation.
We explore this problem, taking programmable controllers as a specific example. The IEC 1131-3 international standard has a diagrammatic notation and a textual language for the description of ``function blocks'' which are the basic components of controller programs. We take an idealised version of the textual language and its diagrammatic counterpart and show that the diagrams capture equivalence of textual programs under a collection of equational laws.
This result establishes that diagrams relieve the programmer of the need to consider non-significant variants of programs and the match between program texts, their corresponding diagrams and their intended interpretation.
We propose that the domain of a Domain-Specific Language (DSL) can be characterised by:
We develop these ideas in the context of industrial computing systems by presenting a semantics and proof system for a language based on IEC 1131-3, the international standard programming language for programmable controllers.
Of particular significance in this example is the use of a diagrammatic representation and the development of a proof system for a class of invariance properties that requires only local knowledge of the structure of diagrams.
Graph-based notations form a significant subclass of visual languages. Studies of the use of such notations in practice have shown that users often employ pragmatic aspects, such as layout, to capture important domain information. Moreover this pragmatic information can support and guide reasoning over such representations. However, typical formalisations of graph-based notations often pay scant regard to such pragmatic considerations. This paper highlights an algebraic account of graph-based notations which is sensitive to relevant layout information. We illustrate, with examples taken from software engineering practice, how this algebra both captures pragmatic aspects of graphs and supports direct reasoning over their structure.
Diagrammatic specification, modelling and programming languages are increasingly prevalent in software engineering and, it is often claimed, provide natural representations which permit of intuitive reasoning. A desirable goal of software engineering is the rigorous justification of such reasoning, yet many formal accounts of diagrammatic languages confuse or destroy any natural reading of the diagrams. Hence they cannot be said to be intuitive. The answer, we feel, is to examine seriously the meaning and accuracy of the terms ``natural'' and ``intuitive'' in this context. This paper highlights, and illustrates by means of examples taken from industrial practice, an ongoing research theme of the authors. We take a deeper and more cognitively informed consideration of diagrams which leads us to a more natural formal underpinning that permits
D.Phil. thesis. Click here for the abstract.
Higraphs, which are structures extending graphs by permitting a hierarchy of nodes, underlie a number of diagrammatic formalisms popular in computing. We provide an algebraic account of higraphs (and of a mild extension), with our main focus being on the mathematical structures underlying common operations, such as those required for understanding the semantics of higraphs and Statecharts, and for implementing sound software tools which support them.
We develop an algebraic foundation for some of the graph-based structures underlying a variety of popular diagrammatic notations for the specification, modelling and programming of computing systems. Using hypergraphs and higraphs as leading examples, a locally ordered category Graph(C) of graphs in a locally ordered category $C$ is defined and endowed with symmetric monoidal closed structure. Two other operations on higraphs and variants, selected for relevance to computing applications, are generalised in this setting.
Harel introduces the notion of zooming out as a useful operation in working with higraphs. Zooming out allows us to consider less detailed versions of a higraph by dropping some detail from the description in a structured manner. Although this is a very useful operation it seems it can be misleading in some circumstances by allowing the user of the zoomed out higraph to make false inferences given the usual transition system semantics for higraphs. We consider one approach to rectifying this situation by following through Harel's suggestion that, in some circumstances, it may be useful to consider higraphs with edges that have no specific origin or destination. We call these higraphs loose higraphs and show that an appropriate definition of zooming on loose higraphs avoids some of the difficulties arising from the use of zooming. We also consider a logic for connectivity in loose higraphs.