Specifying history and backtracking mechanisms
School of Computing
Stafford, ST18 0DG, UK.
Dipartimento di Scienze dell'Informazione
Universita' degli Studi di Roma "La Sapienza"
Via Salaria 113, 00198, Rome, Italy.
A. Dix and R. Mancini (1997).
Specifying history and backtracking mechanisms.
In 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