EditorArrow: an arrow-based model for editor-based programming. State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present EditorArrow: a single, unified semantic model that defines shared state and event handling. We study the properties of EditorArrow, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle. The availability of this tool has proved to be indispensable in this endeavor.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Achten, Peter; van Eekelen, Marko; de Mol, Maarten; Plasmeijer, Rinus: EditorArrow: an arrow-based model for editor-based programming (2013)
- de Mol, Maarten; van Eekelen, Marko: Beautiful code, beautiful proof? (2013)