A Model of Navigation History

TL;DR

This paper presents a formal model of web navigation history aligned with the WHATWG specification, identifies inconsistencies in browser implementations, and proposes patches to improve correctness and consistency.

Contribution

It introduces a formal model of navigation history, demonstrates its shortcomings, and proposes specific patches to align implementations with the corrected model.

Findings

Browsers are inconsistent in implementing navigation history.

The original specification does not satisfy fundamental properties of navigation.

Proposed patches improve alignment between browser behavior and the formal model.

Abstract

Navigation has been a core component of the web since its inception: users and scripts can follow hyperlinks, and can go back or forwards through the navigation history. In this paper, we present a formal model aligned with the WHATWG specification of navigation history, and investigate its properties. The fundamental property of navigation history is that traversing the history by delta then by delta' should be the same as traversing by delta+delta'. In particular, traversing by +1 (forward) then by -1 (back) is the same as traversing by 0 (doing nothing). We show that the specification-aligned model does not satisfy this property, by exhibiting a series of counter-examples, which motivate four patches to the model. We present a series of experiments, showing that browsers are inconsistent in their implementation of navigation history, but that their behaviour is closer to the patched model than to the specification-aligned model. We propose patches to the specification to align it with the patched model.