Enriching Interactive Components with Again Commands

The paper studies the systematic design and implementation of interactive components whose input interface is enriched by undo commands. An undo command inverts the interaction history returning to a previously visited state. We formalize different policies for undo commands cancelling the most recent input, the most recent occurrence of a specified input, and the final history segment after a user defined checkpoint. For each undo policy, we specify the component's modified input/output behaviour in terms of the original behaviour as a function from input streams to output streams. Then we systematically transform the modified input/output behaviour into an implementation by a state transition machine. The resulting formal method extends the state transition table of an interactive component in a systematic way when its input interface is enriched by undo commands under different policies.