Specifying history and backtracking mechanisms

Alan Dix
School of Computing
Staffordshire University
Stafford, ST18 0DG, UK.
email: alan@hcibook.com
Roberta Mancini
Dipartimento di Scienze dell'Informazione
Universita' degli Studi di Roma "La Sapienza"
Via Salaria 113, 00198, Rome, Italy.

Full reference:

A. Dix and R. Mancini (1997).
Specifying history and backtracking mechanisms.
Formal Methods in Human-Computer Interaction, Eds. P. Palanque and F. Paterno. London, Springer-Verlag. pp. 1-24.

You can see the full paper (PDF) or download a compressed postscript copy from http://www.alandix.com/docs/papers/hist-Zed.ps.Z (compressed postscript). URL for related work: http://www.hcibook.com/alan/topics/undo/


Most hypertext systems and in particular most web browsers include some form of history mechanism. These allow users to see where they have been and to return to previous locations. The form of such mechanisms varies: some are stack based, others keep a full trace of all previously visited locations. Users are often confused by these mechanisms and this confusion is also reflected in some specifications! One reason for this confusion is that history mechanisms are reflexive: you are forced to think in terms of what you have been doing, rather than simply doing it. Undo mechanisms share this reflexivity as well as being similar in other ways. One consequence of reflexivity is that the notion of 'state' can be difficult to define, there being a simple state (the system without history/undo) and a full state (including the history information). This chapter will examine the history mechanisms of several browsers and hypertext systems and show how these can be formally specified over a generic base model. This will also highlight the fact that some such systems have more than one history mechanism simultaneously at work - no wonder the users get confused! The chapter draws on insights gained during recent extensive studies of undo mechanisms by the authors.

Alan Dix 23/12/96