Sylvain Conchon
email: conchon@lri.fr

Jean-Christophe Filliâtre
email: filliatr@lri.fr

Semi-Persistent Data Structures

A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure. Additionally, we give some examples of semi-persistent data structures (arrays, lists and hash tables).

Introduction

A data structure is said to be persistent when any update operation returns a new structure without altering the old version. In purely applicative programming, data structures are automatically persistent [START_REF] Okasaki | Purely Functional Data Structures[END_REF]. Yet this notion is more general and the exact meaning of persistent is observationally immutable. Driscoll et al. even proposed systematic techniques to make imperative data structures persistent [START_REF] Driscoll | Making Data Structures Persistent[END_REF]. In particular, they distinguish partial persistence, where all versions can be accessed but only the newest can be updated, from full persistence where any version can be accessed or updated. In this paper, we study another notion of persistence, which we call semi-persistence.

One of the main interests of a persistent data structure shows up when it is used within a backtracking algorithm. Indeed, when we are back from a branch, there is no need to undo the modifications performed on the data structure: we simply use the old version, which persisted, and start a new branch. One can immediately notice that full persistence is not needed in this case, since we are reusing ancestors of the current version, but never siblings (in the sense of another version obtained from a common ancestor). We shall call semi-persistent a data structure where only ancestors of the newest version can be updated. Note that this notion is different from partial persistence, since we need to update ancestors, and not only to access them.

A semi-persistent data structure can be more efficient than its fully persistent counterpart, both in time and space. Let us illustrate this fact on an example. We consider persistent arrays as introduced in [START_REF] Henry | Shallow binding makes functional arrays fast[END_REF]. The basic idea is to use an imperative array for the newest version of the persistent array and indirections for old versions. For instance, starting with an array a 0 initialized with 0, and performing the successive updates a 1 = set(a 0 , 1, 7), a 2 = set(a 1 , 2, 8) and a 3 = set(a 2 , 5, 3), we end up with the following situation:

When accessing or updating an old version, e.g. a 1 , Baker's solution is to first perform a rerooting operation, which makes a 1 point to the imperative array by reversing the linked list of indirections:

But if we know that we are not going to access a 2 and a 3 anymore, we can save this list reversal. All we need to do is to perform the assignments contained in this list:

Thus it is really easy to turn these persistent arrays into a semi-persistent data structure, which is more efficient since we save some pointer assignments. An Objective Caml code for such semi-persistent arrays is given in Section 2.1. On this particular example, we see that the data structure behaves like an "undo stack" (the pairs index/value stored in indirections are precisely the undo operations). The same idea could be applied to any imperative data structure where update operations can be undone. Contrary to the use of an explicit undo stack, which interferes with the backtracking algorithm, this solution is hiding the undo stack in the data structure. Thus the algorithm may be written as if it was operating on a fully persistent data structure, provided that we only backtrack to ancestor versions.

Checking the correctness of a program involving a semi-persistent data structure amounts to showing that • first, the data structure is correctly used ;

• second, the data structure is correctly implemented. This article only addresses the former point. Regarding the latter, we simply give implementations of semi-persistent data structures. Proving the correctness of these implementations is out of the scope of this paper (see Section 5).

Our approach consists in annotating programs with user pre-and postconditions, which mainly amounts to expressing the validity of the successive versions of a semipersistent data structure. By validity, we mean being an ancestor of the newest version. Then we compute a set of proof obligations which express the correctness of programs using a weakest precondition-like calculus [START_REF] Edsger | A discipline of programming[END_REF]. These obligations lie in a decidable logical fragment, for which we provide a sound and complete decision procedure. Thus we end up with an almost automatic way of checking the legal use of semi-persistent data structures.

To make it more precise, let us consider two programs manipulating a semi-persistent data structure. Each program is a function taking a version x 0 of the data structure as argument, generating new versions using an update operation upd and finally accessing the resulting version using an access operation acc :

fun f x 0 = {valid(x 0 )} let x 1 = upd x 0 in let x 2 = upd x 0 in acc x 2 fun g x 0 = {valid(x 0 )} let x 1 = upd x 0 in let x 2 = upd x 0 in acc x 1
Each function has a precondition requiring the validity of x 0 (through a valid predicate).

Then both functions successively build two new versions x 1 and x 2 as successors of x 0 . This can be illustrated by the following version trees, where arrows represent version successors and a dashed arrow stands for a version that has become invalid:

Finally, function f accesses x 2 , which is legal; and function g accesses x 1 , which is illegal since x 1 is not an ancestor of the newest version x 2 . If the x i were semi-persistent arrays, as described above, the contents of x 1 would indeed be modified by the creation of x 2 . Thus x 1 should not be accessed anymore. As illustrated by this example, evaluation order matters as the creation of a new version has side-effects on other versions. Thus semi-persistence is clearly related to impure data structures. For this reason, our weakest precondition calculus relies on a small effect inference which detects the mutation of the data structure.

Related work. To our knowledge, this notion of semi-persistence is new. However, there are several domains which are somehow connected to our work, either because they are related to some kind of stack analysis, or because they are providing decision procedure for reachability issues. First, works on escape analysis [START_REF] Hannan | A type-based analysis for stack allocation in functional languages[END_REF][START_REF] Blanchet | Escape analysis: Correctness proof, implementation and experimental results[END_REF] address the problem of stack-allocating values; we may think that semi-persistent versions that become invalid are precisely those which could be stack-allocated, but it is not the case as illustrated by example g above. Second, works on stack analysis to ensure memory safety [START_REF] Morrisett | Stack-based typed assembly language[END_REF][START_REF] Spalding | Certifying compilation for a language with stack allocation[END_REF][START_REF] Tofte | Implementation of the typed call-by-value lambda-calculus using a stack of regions[END_REF] provide methods to check the consistent use of push and pop operations. However, these approaches are not precise enough to distinguish between two sibling versions (of a given semi-persistent data structure) which are both upper in the stack. Regarding the decidability of our proof obligations, our approach is similar to other works regarding reachability in linked data structures [START_REF] Nelson | Verifying reachability invariants of linked structures[END_REF][START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF][START_REF] Ranise | A theory of singly-linked lists and its extensible decision procedure[END_REF]. However, our logic is much simpler and we provide a specific decision procedure. Finally, we can mention Knuth's dancing links [START_REF] Knuth | Dancing links[END_REF] as an example of a data structure specifically designed for backtracking algorithms; but it is still a traditional imperative solution where an explicit undo operation is performed in the main algorithm.

This paper is organized as follows. First, Section 2 gives examples of semi-persistent data structures and shows the benefits of semi-persistence with some benchmarks. Then our formalization of semi-persistence is presented in two steps: Section 3 introduces a small programming language to manipulate semi-persistent data structures, and Section 4 defines the proof system which checks the valid use of semi-persistent data structures. Section 5 concludes with possible extensions.

Examples of Semi-Persistent Data Structures

We present the implementation of semi-persistent arrays, lists and hash tables and benchmarks to show the benefits of semi-persistence. All these examples are written in Objective Caml [START_REF] Leroy | The Objective Caml System[END_REF].

Arrays

First we implement semi-persistent arrays, as described in the introduction of this paper. The interface is similar to persistent arrays:

type α t val create : int → α → α t val get : α t → int → α val set : α t → int → α → α t
Type α t is the polymorphic type of semi-persistent arrays containing values of type α. create n v creates a new array of size n with all cells initialized with v. get and set are the usual access and update functions.

A semi-persistent array is a reference containing a value of type α data, which is either an imperative array from Ocaml's standard library or an indirection: The only difference with the fully persistent implementation is in function reroot, where the sequence a.(i) ← v; t := n would be replaced by the more complex code:

type α t =
let v' = a.(i) in a.(i) ← v; t := n; t' := Diff (i, v', t)
Thus we save, in the semi-persistent implementation, an array access, a constructor allocation and an assignment. It is worth noticing that get performs a reroot operation only to improve further calls to get and set. This is definitely the good choice in a pure backtracking algorithm (i.e. where we only access the current version or backtrack to some previous version). But we could imagine a more complex algorithm where we need to access to previous versions without backtracking. For this purpose, we could also provide a non-destructive access operation, nd get, which simply follows the Diff stack:

let rec nd_get t i = match !t with | Newest a → a.(i) | Diff (j, v, t') → if i = j then v else nd_get t' i
Our formalization of semi-persistence will handle both kinds of access operations.

Lists

As a second example, we consider an immutable data structure which we make semipersistent. The simplest and most popular example is the list data structure. To make it semi-persistent, the idea is to reuse cons cells between successive conses to the same list. For instance, given a list l, the cons operation 1::l allocates a new memory block to store 1 and a pointer to l. Then a successive operation 2::l could reuse the same memory block if the list is used in a semi-persistent way. Thus we simply need to replace 1 by 2. To do this, we must maintain for each list the previous cons, if any.

To implement semi-persistent lists, we use the following type of double-linked lists:

type α t = { mutable head : α; tail : α t; mutable pc : α t }
Fields head and tail are the usual fields for linked lists, except that head is a mutable field to allow further modification of its contents. The additional field pc keeps track of a previous cons, if any.

Similarly to the constant null in C or Java programs, we would like to represent the empty list as a statically allocated constant value of type α t. Since there is no way to build such a polymorphic value (we can not instantiate the head field), we turn the empty list into a function taking a dummy value as argument:

let nil v = let rec null = { head = v; tail = null; pc = null } in null
This function allocates a single cons cell null where tail and pc fields are physically equal to null. Thus testing for the empty list is as simple as let is_nil l = l.tail == l Additionally, the empty list is used as the value for pc when there is no previous cons.

The cons function checks the existence of a previously allocated block (testing pc for being the empty list) and reuses it if any:

let cons x l = if is_nil l.pc then begin let n = { l with head=x; tail=l } in if not (is_nil l) then l.pc ← n; n end else begin let c = l.pc in c.head ← x; c end
The test not (is nil l) prevents from reusing the successor of the empty list, since it is shared by all lists.

Implementing the tail operation is immediate:

let tail l = l.tail
Though tail does not modify l, it makes it invalid since a subsequent cons on the result of tail l would modify the head of l in place. Contrary to operation get on arrays, it is not possible to implement a non-destructive version of tail. Yet it is possible to provide other, non-destructive, access operations, such as a membership test function:

let rec mem x l = not (is_nil l) && (l.head = x || mem x l.tail)
It is worth noticing that these semi-persistent lists are trading off allocation for deallocation. Indeed, the average use of these lists requires less allocation than ordinary immutable lists (the cons cells are slightly bigger but are reusable). But, on the contrary, such lists prevent deallocation since a pointer p to a 1-element list cons x nil makes all subsequent conses alive as long as p is alive.

Such semi-persistent lists could even be used to improve the implementation of semipersistent arrays from the previous section, since Diff cells could similarly be reused.

Hash Tables

Combining (semi-)persistent arrays with (semi-)persistent lists, one easily gets (semi-)persistent hash tables. Such a combination is nicely implemented as a module parameterized with data structures for arrays and lists respectively. Introducing the following signatures for these parameters: By instantiating arrays and lists implementations by semi-persistent arrays and lists from Sections 2.1 and 2.2 respectively, we automatically get semi-persistent hash tables. Note that mem is a non-destructive operation only if PA.get is.

module type Array = sig type α t val create : int → α → α t val get : α t → int → α val set : α t → int → α → α t end module type List = sig type α t val nil : α → α t val cons : α → α t → α t val mem : α → α t →

Benchmarks

We present some benchmarks to show the benefits of semi-persistence. Each of the previous three data structures is tested the same way and compared to its fully persistent counterpart. The test consists in simulating a backtracking algorithm with branching degree 4 and depth 6, operating on a single data structure. N successive update operations are performed on the data structure between two branchings points (that is set on arrays, cons on lists and add on hash tables). In each case, the benchmarking function is as follows: As we can see, the speedup ratio is always greater than 1 and almost reaches 7 (for semi-persistent lists). Regarding memory consumption, we compared the total number of allocated bytes, as reported by Ocaml's garbage collector. For the tests corresponding to the last column (N = 10000) semi-persistent data structures always used much less memory than persistent ones: 3 times less for arrays, 575 times less for lists and 1.5 times less for hash tables. The dramatic ratio for lists is easily explained by the fact that our benchmark program reflects the best case regarding memory allocation (allocation in one branch is reused in other branches, which all have the same length).

let bench t = let rec descend h k t = if k < N

Programming with Semi-Persistent Data Structures

This section introduces a small programming language to manipulate semi-persistent data structures. In order to keep it simple, we assume that we are operating on the successive versions of a single, statically allocated, data structure. Multiple data structures and dynamic allocation are discussed in Section 5.

Syntax

The syntax of our language is as follows:

Primitive Operations

As seen in Section 2, we use three kinds of operations on semi-persistent data structures:

• update operations backtracking to a given version and creating a new successor, which becomes the newest version;

• destructive access operations backtracking to a given version, which becomes the newest version, and then accessing it;

• non-destructive access operations accessing an ancestor of the newest version, without modifying the data structure.

Since update and destructive access operations both need to backtrack, it is convenient to design a language based on the following three primitives:

• backtrack: backtracks to a given version, making it the newest version;

• branch: builds a new successor of a given version, assuming it is the newest version;

• acc: accesses a given version, assuming it is a valid version.

Then update and destructive access operations can be rephrased in terms of the above primitives: upd e = branch (backtrack e) dacc e = acc (backtrack e)

Operational Semantics

We equip our language with a small step operational semantics, which is given in Figure 1. One step of reduction is written e 1 , S 1 → e 2 , S 2 where e 1 and e 2 are program expressions and S 1 and S 2 are states. A value v is either a constant c or a pointer p. Pointers represent versions of the semi-persistent data structure. A state S is a stack p 1 , . . . , p m of pointers, p m being the top of the stack. The semantics is straightforward, except for primitive operations. Primitive backtrack expects an argument p n designating a valid version of the data structure, that is an element of the stack. Then all pointers on top of p n are popped from the stack and p n is the result of the operation. Primitive branch expects an argument p n being the top of the stack and pushes a new value p, which is also the result of the operation. Finally, primitive acc expects an argument p n designating a valid version, leaves the stack unchanged and returns some value for version p n , represented by A(p n ). (We leave A uninterpreted since we are not interested in the values contained in the data structure.)

Note that reduction of backtrack p n or acc p n is blocked whenever p n is not an element of S, which is precisely what we intend to prevent.

There is an obvious property of reduction which will be useful in Section 4.4:

Lemma 1 The first element of a state is preserved by reduction, that is if e, pS → e ′ , S ′ then S ′ = pS ′′ .

E ::= [] | f E | let x = E in e | if E
x = v in e, S → e{x ← v}, S f v, S → e{x ← v}, S if fun f (x : ι) = {φ} e {ψ} ∈ ∆ backtrack p n , p 1 • • • p n p n+1 • • • p m → p n , p 1 • • • p n branch p n , p 1 • • • p n → p, p 1 • • • p n p p fresh acc p n , p 1 • • • p n p n+1 • • • p m → A(p n ), p 1 • • • p n p n+1 • • • p m E[e 1 ], S 1 → E[e 2 ], S 2 if e 1 , S 1 → e 2 ,

Type System with Effect

We introduce a type system to characterize well-formed programs. Our language is simply typed and thus type-checking is immediate. Meanwhile, we infer the effect ǫ of each expression, as an element of the boolean lattice ({⊥, ⊤}, ∧, ∨). This boolean indicates whether the expression modifies the semi-persistent data structure (⊥ meaning no modification and ⊤ a modification). Effects will be used in the next section to simplify constraint generation. Each function is given a type τ , as follows:

τ ::= (x : ι) → ǫ {φ} ι {ψ}
The argument is given a type and a name (x) since it is bound in both precondition φ and postcondition ψ. Type τ also indicates the latent effect ǫ of the function, which is the effect resulting from the function application.

A typing environment Γ is a set of type assignments for variables (x : ι), constants (c : ι) and functions (f : τ ). It is assumed to contain at least type declarations for the primitives, as follows:

backtrack : (x : semi) → ⊤ {φ backtrack } semi {ψ backtrack } branch : (x : semi) → ⊤ {φ branch } semi {ψ branch } acc : (x : semi) → ⊥ {φ acc } δ {ψ acc }
where pre-and postcondition are given later. As expected, both backtrack and branch modify the semi-persistent data structure and thus have effect ⊤, while the non-destructive access acc has effect ⊥. Given a typing environment Γ, the judgment Γ ⊢ e : ι, ǫ means "e is a well-formed expression of type ι and effect ǫ" and the judgment Γ ⊢ d : τ means "d is a well-formed function definition of type τ ". Typing rules are given in Figure 2. They assume judgments Γ ⊢ φ pre and Γ ⊢ ψ post ι for the well-formedness of pre-and postconditions respectively, to be defined later in Section 4.1. Note that there is no typing rule for pointers, to prevent their explicit use in programs. d i can be given a type τ i such that d 1 : τ 1 , . . . , d n : τ n ⊢ d i : τ i for each i. The types τ i can easily be obtained by a fixpoint computation, starting will all latent effects set to ⊥, since effect inference is clearly a monotone function.

Var

x : ι ∈ Γ Γ ⊢ x : ι, ⊥ Const c : ι ∈ Γ Γ ⊢ c : ι, ⊥ App f : (x : ι 1 ) → ǫ 2 {φ} ι 2 {ψ} ∈ Γ Γ ⊢ e : ι 1 , ǫ 1 Γ ⊢ f e : ι 2 , ǫ 1 ∨ ǫ 2 Ite Γ ⊢ e 1 : bool, ǫ 1 Γ ⊢ e 2 : ι, ǫ 2 Γ ⊢ e 3 : ι, ǫ 3 Γ ⊢ if e 1 then e 2 else e 3 : ι, ǫ 1 ∨ ǫ 2 ∨ ǫ 3 Let Γ ⊢ e 1 : ι 1 , ǫ 1 Γ, x : ι 1 ⊢ e 2 : ι 2 , ǫ 2 Γ ⊢ let x = e 1 in e 2 : ι 2 , ǫ 1 ∨ ǫ 2 Fun x : ι 1 ⊢ φ pre x : ι 1 ⊢ ψ post ι 2 Γ, x : ι 1 ⊢ e : ι 2 , ǫ Γ ⊢ fun f (x : ι 1 ) = {φ} e {ψ} : (x : ι 1 ) → ǫ {φ} ι 2 {ψ}

Examples

Let us consider the two functions f and g from the introduction. Let S be a state composed of a single pointer p. The reduction of f p in S runs as follows:

f p, p → let x 1 = upd p in let x 2 = upd p in acc x 2 , p → let x 1 = p 1 in let x 2 = upd p in acc x 2 , pp 1 → let x 2 = upd p in acc x 2 , pp 1 → let x 2 = p 2 in acc x 2 , pp 2 → acc p 2 , pp 2 → A(p 2 ), pp 2 p 3
and ends on the value A(p 2 ). On the contrary, the reduction of g p in S runs as follows:

g p, p → let x 1 = upd p in let x 2 = upd p in acc x 1 , p → let x 1 = p 1 in let x 2 = upd p in acc x 1 , pp 1 → let x 2 = upd p in acc p 1 , pp 1 → let x 2 = p 2 in acc p 1 , pp 2 → acc p 1 , pp 2
and blocks on acc p 1 .

Proof System

This section introduces a theory for semi-persistence and a proof system for this theory. First we define the syntax and semantics of logical annotations. Then we compute a set of constraints for each program expression, which is proved to express the correctness of the program with respect to semi-persistence. Finally we give a decision procedure to solve the constraints.

Theory of Semi-Persistence

The syntax of annotations is as follows:

term t ::= x | p | prev(t) atom a ::= t = t | path(t, t) postcondition ψ ::= a | ψ ∧ ψ precondition φ ::= a | φ ∧ φ | ψ ⇒ φ | ∀x. φ
Terms are built from variables, pointers and a single function symbol prev. Atoms are built from equality and a single predicate symbol path. A postcondition ψ is restricted to a conjunction of atoms. A precondition is a formula φ built from atoms, conjunctions, implications and universal quantifications. A negative formula (i.e. appearing on the left side of an implication) is restricted to a conjunction of atoms. We introduce two different syntactic categories ψ and φ for formulae but one can notice that φ actually contains ψ. This syntactic restriction on formulae is justified later in Section 4.5 when introducing the decision procedure. In the remainder of the paper, a "formula" refers to the syntactic category φ. Substitution a of term t for a variable x in a formula φ is written φ{x ← t}. We denote by S(A) the set of all subterms of a set of atoms A.

The typing of terms and formulae is straightforward, assuming that prev has signature semi → semi. Function postconditions may refer to the function result, represented by the variable ret. Formulae can only refer to variables of type semi (including variable ret). We write Γ ⊢ φ to denote a well-formed formula φ in a typing environment Γ.

We now give the semantics of program annotations. The main idea is to express that a given version is valid if and only if it is an ancestor of the newest version. To illustrate this idea, the following figure shows the successive version trees for the sequence of declarations x 1 = upd x 0 , x 2 = upd x 1 , x 3 = upd x 1 and x 4 = upd x 0 :

The newest version is pictured as a black node, other valid versions as white nodes and invalid ones as gray nodes.

The meaning of prev and path is to define the notion of ancestor: prev(x) is the immediate ancestor of x and path(x, y) holds whenever x is an ancestor of y. The corresponding theory can be axiomatized as follows: The constraint synthesis for a function call, C(f e 1 , φ), is the only nontrivial case. It requires precondition φ f to be valid and postcondition ψ f to imply the expected property φ. Universal quantification is used to introduce f 's results and side-effects. We use the effect in f 's type to distinguish two cases: either effect is ⊥ which means that cur is not modified and thus we only quantify over f 's result (hence we get for free the invariance of cur ); or effect is ⊤ and we quantify over an additional variable cur ′ which stands for the new value of cur . To simplify this definition, we introduce a formula transformer frame f (φ) which builds the appropriate postcondition for argument e 1 .

frame f (φ) = φ f {x ← ret} ∧ ∀ret ′ . ψ f {ret ← ret ′ , x ← ret} ⇒ φ{ret ← ret ′ } if f : (x : ι) → ⊥ {φ f } ι ′ {ψ f } frame f (φ) = φ f {x ← ret} ∧ ∀ret ′ cur ′ . ψ f {ret ← ret ′ , x ← ret, cur ← cur ′ } ⇒ φ{ret ← ret ′ , cur ← cur ′ } if f : (x : ι) → ⊤ {φ f } ι ′ {ψ f } C(v, φ) = φ{ret ← v} C(if
The formula established by an expression may be weakened, as stated by the following lemma:

Examples

This section details the constraints obtained on several program examples.

Simple Examples

Let us consider again the two functions f and g from the introduction, valid(x 0 ) being now expressed as path(x 0 , cur ):

fun f (x 0 : semi) = {path(x 0 , cur)} let x 1 = upd x 0 in let x 2 = upd x 0 in acc x 2 fun g (x 0 : semi) = {path(x 0 , cur)} let x 1 = upd x 0 in let x 2 = upd x 0 in acc x 1
We compute the associated constraints for an empty postcondition true. The constraint

C(f ) is ∀x 0 . ∀cur. path(x 0 , cur) ⇒ path(x 0 , cur) ∧ ∀x 1 . ∀cur 1 . (prev(x 1 ) = x 0 ∧ cur 1 = x 1 ) ⇒ path(x 0 , cur 1 ) ∧ ∀x 2 . ∀cur 2 . (prev(x 2 ) = x 0 ∧ cur 2 = x 2 ) ⇒ path(x 2 , cur 2 ) ∧ ∀ret. true ⇒ true
It can be split into three proof obligations, which are the following universally quantified sequents: path(x 0 , cur) ⊢ path(x 0 , cur)

path(x 0 , cur), prev(x 1 ) = x 0 , cur 1 = x 1 ⊢ path(x 0 , cur 1 )
path(x 0 , cur), prev(x 1 ) = x 0 ,

cur 1 = x 1 , prev(x 2 ) = x 0 , cur 2 = x 2 ⊢ path(x 2 , cur 2 )
The three of them hold in theory T and thus f is correct. Similarly, the constraint C(g) can be computed and split into three proof obligations. The first two are exactly the same as for f but the third one is slightly different:

path(x 0 , cur), prev(x 1 ) = x 0 , cur 1 = x 1 , prev(x 2 ) = x 0 , cur 2 = x 2 ⊢ path(x 1 , cur 2 )
In that case it does not hold in theory T .

Backtracking Example

As a more complex example, let us consider a backtracking algorithm. The pattern of a program performing backtracking on a persistent data structure is a recursive function bt looking like fun bt (x : semi) = . . . bt(upd x) . . . bt(upd x) . . . Function bt takes a data structure x as argument and makes recursive calls on several successors of x. This is precisely a case where the data structure may be semi-persistent, as motivated in the introduction. To capture this pattern in our framework, we simply need to consider two successive calls bt(upd x), which can be written as follows:

fun bt (x : semi) = let = bt(upd x) in bt(upd x)
Function bt obviously requires a precondition stating that x is a valid version of the semi-persistent data structure. This is not enough information to discharge the proof obligations: the second recursive call bt(upd x) requires x to be valid, which possibly could no longer be the case after the first recursive call. Therefore a postcondition for bt is needed to ensure the validity of x:

fun bt (x : semi) = { path(x, cur ) } let = bt(upd x) in bt(upd x) { path(x, cur ) } The constraint C(bt) is ∀x. ∀cur. path(x, cur) ⇒ path(x, cur) ∧ ∀x 1 . ∀cur 1 . (prev(x 1 ) = x ∧ cur 1 = x 1 ) ⇒ path(x 1 , cur 1 ) ∧ ∀x 2 . ∀cur 2 . path(x 1 , cur 2 ) ⇒ path(x, cur 2 ) ∧ ∀x 3 . ∀cur 3 . (prev(x 3 ) = x ∧ cur 3 = x 3 ) ⇒ path(x 3 , cur 3 ) ∧ ∀x 4 . ∀cur 4 . path(x 3 , cur 4 ) ⇒ path(x, cur 4 )
which is valid in theory T .

Soundness

In the remainder of this section, we consider a program ∆ = d 1 , . . . , d n whose constraints are valid, that is

|= C(d 1 ) ∧ • • • ∧ C(d n ).
We are going to show that the evaluation of this program will not block.

For this purpose we first introduce the notion of validity with respect to a state of the operational semantics:

Definition 2 A formula φ is valid in a state S = p 1 , . . . , p n , written S |= φ, if it is valid in any model M for T such that prev(p i+1 ) = p i for all 1 ≤ i < n cur = p n
Then we show that this validity is preserved by the operational semantics. To do this, it is convenient to see the evaluation contexts as formula transformers, as follows:

E E[φ] [] φ let x = E 1 in e 2 E 1 [C(e 2 , φ){x ← ret}] if E 1 then e 2 else e 3 E 1 [C(e 2 , φ) ∧ C(e 3 , φ)] f E 1 E 1 [frame f (φ)]
There is a property of commutation between contexts for programs and contexts for formulae:

Lemma 4 S |= C(E[e], φ) if and only if S |= C(e, E[φ]).

Proof. Immediate by induction on E.

We now want to prove preservation of validity, that is if S |= C(e, φ) and e, S → e ′ , S ′ then S ′ |= C(e ′ , φ). Obviously, this does not hold for any state S, program e and formula φ. Indeed, if S ≡ p 1 p 2 , e ≡ upd p 1 and φ ≡ prev(p 2 ) = p 1 , then C(e, φ) is

path(p 1 , cur) ∧ ∀ret ′ cur ′ . (prev(ret ′ ) = p 1 ∧ cur ′ = ret ′ ) ⇒ prev(p 2 ) = p 1
which holds in S. But S ′ ≡ p 1 p for a fresh p, e ′ ≡ p, and C(e ′ , φ) is prev(p 2 ) = p 1 which does not hold in S ′ (since p 2 does not appear in S ′ anymore). Fortunately, we are not interested in the preservation of C(e, φ) for any formula φ, but only for formulae which arise from function postconditions. As pointed out in Section 4.1, a function postcondition may only refer to x, cur and ret only. Therefore we are only considering formulae C(e, φ) where x is the only free variable (cur and ret do not appear in formulae C(e, φ) anymore). This excludes the formula prev(p 2 ) = p 1 in the example above.

In the remainder of this section, we only consider program expressions and formulae which only refer to a single pointer p (representing the function argument). For technical reasons, it is also convenient to restrict ourselves to states whose p is the first element. This is not a restriction, as stated by the following lemma:

Lemma 5 Let e be an expression and φ a formula which both refer to a single pointer p. Then, for any state S 1 pS 2 , S 1 pS 2 |= C(e, φ) if and only if pS 2 |= C(e, φ).

We are now able to prove preservation of validity: • If e = f v and f is not a primitive then e ′ = e f {x ← v} and S ′ = S. We have • Proof. The proof is done by induction on the length of the evaluation → * and by case analysis on the last reduction:

C(e, φ) = C(v, frame f (φ)) = frame f (φ){ret ← v}. If f : (x : ι) → ⊥ {φ f } ι ′ {ψ f } then this simplifies to φ f {x ← v} ∧ ∀ret ′ . ψ f {x ← v, . . . } ⇒ φ{x ← v, . . . }. Since f is correct, we have |= C(f ) = ∀x. φ f ⇒ C(e f , ψ f ). Thus S |= φ f {x ← v} ⇒ C(e f {x ←
If e = backtrack p n then S = p 1 • • • p n p n+1 • • • p m , e ′ = p n and S ′ = p 1 • • • p n . We have S |= C(backtrack p n , φ), that is S |= • • • ∧ ∀ret ′ cur ′ . (ret ′ = p n ∧ cur ′ = p n ) ⇒ φ{ret ← ret ′ ,
• If e is irreducible then it is either a value v and the result holds, or it is an expression E[f v] with f a primitive. By hypothesis, we have S |= C(E[f v], φ) and thus

S |= C(f v, E[φ]) by Lemma 4. Since C(f v, E[φ]) = φ f {x ← v} ∧ . . .
, where φ f is f 's precondition and x its formal argument. In each case, the validity of this precondition contradicts the irreducibility of e.

• If e, S → e 1 , S 1 → * e ′ , S ′ → then by Lemma 6 S 1 |= C(e 1 , φ) and the result holds by induction hypothesis on e 1 .

Decision Procedure

We now show that constraints are decidable and we give a decision procedure. First, we notice that any formula φ is equivalent to a conjunction of formulae of the form ∀x

1 . . . . ∀x n . a 1 ∧ • • • ∧ a m ⇒ a
where the a i 's are atoms. This results from the syntactic restrictions on pre-and postconditions, together with the weakest preconditions rules which are only using postconditions in negative positions. Therefore we simply need to decide whether a given atom is the consequence of other atoms. We first recall the notion of congruence closure of a set H of hypotheses {a 1 , . . . , a m }.

Definition 3

The congruence closure H ⋆ of H is the smallest set of atoms such that

• if a ∈ H then a ∈ H ⋆ ; • if t ∈ S(H ⋆ ) then t = t ∈ H ⋆ ; • if t 1 = t 2 ∈ H ⋆ then t 2 = t 1 ∈ H ⋆ ; • if t 1 = t 2 ∈ H ⋆ and t 2 = t 3 ∈ H ⋆ then t 1 = t 3 ∈ H ⋆ ; • if t 1 = t 2 ∈ H ⋆ and prev(t 1 ), prev(t 2 ) ∈ S(H ⋆ ) then prev(t 1 ) = prev(t 2 ) ∈ H ⋆ ; • if t 1 = t 2 ∈ H ⋆ , t 3 = t 4 ∈ H ⋆ and path(t 1 , t 3 ) ∈ H ⋆ then path(t 2 , t 4 ) ∈ H ⋆ .
Obviously S(H ⋆ ) = S(H) since no new term is created. Thus H ⋆ is finite and can be computed as a fixpoint.

Algorithm 1 For any atom a such that S({a}) ⊆ S(H), the following algorithm, decide(H, a), decides whether H |= a.

1. First we compute the congruence closure H ⋆ .

2. If a is of the form t 1 = t 2 , we return true if t 1 = t 2 ∈ H ⋆ and false otherwise.

3. If a is of the form path(t 1 , t 2 ), we build a directed graph G whose nodes are the subterms of H ⋆ , as follows:

(a) for each pair of nodes t and prev(t) we add an edge from prev(t) to t;

(b) for each path(t 1 , t 2 ) ∈ H ⋆ we add an edge from t 1 to t 2 ;

(c) for each t 1 = t 2 ∈ H ⋆ we add two edges between t 1 and t 2 .

4. Finally we check whether there is a path from t 1 to t 2 in G.

Obviously this algorithm terminates since H ⋆ is finite and thus so is G. We now show soundness and completeness for this algorithm. Note: the restriction S({a}) ⊆ S(H) can be easily met by adding to H the equalities t = t for any subterm t of a; it was only introduced to simplify the proof above.

Implementation

We have implemented the whole framework of semi-persistence. The implementation relies on an existing proof obligations generator, Why [START_REF] Filliâtre | The Why verification tool[END_REF]. This tool takes annotated firstorder imperative programs as input and uses a traditional weakest precondition calculus to generate proof obligations. The language we use in this paper is actually a subset of Why's input language. We simply use the imperative aspect to make cur a mutable variable. Then the resulting proof obligations are exactly the same as those obtained by the constraint synthesis defined in Section 4.2.

The Why tool outputs proof obligations in the native syntax of various existing provers. In particular, these formulas can be sent to Ergo [START_REF] Conchon | Ergo: A Decision Procedure for Program Verification[END_REF], an automatic prover for first-order logic which combines congruence closure with various built-in decision procedures. We first simply axiomatized theory T using (A 1 )-(A 3 ), which proved to be powerful enough to verify all examples from this paper and several other benchmark programs. Yet it is possibly incomplete (automatic theorem provers use heuristics to handle quantifiers in first-order logic). To achieve completeness, and to assess the results of Section 4.5, we also implemented theory T as a new built-in decision procedure in Ergo. Again we verified all the benchmark programs.

Conclusion

We have introduced the notion of semi-persistent data structures, where update operations are restricted to ancestors of the most recent version. Semi-persistent data structures may be more efficient than their fully persistent counterparts, and are of particular interest in implementing backtracking algorithms. We have proposed an almost automatic way of checking the legal use of semi-persistent data structures. It is based on light user annotations in programs, from which proof obligations are extracted and automatically discharged by a decision procedure.

There is a lot of remaining work to be done. First, the language introduced in Section 3, in which we check for legal use of semi-persistence, could be greatly enriched. Beside the missing features such as polymorphism or recursive datatypes, it would be of particular interest to consider the following extensions:

• simultaneous use of several semi-persistent data structures: One would probably need to express disjointness of version subtrees, and thus to enrich the logical fragment used in annotations with disjunctions and negations. We may lose decidability of the logic, though.

• dynamic creation of semi-persistent data structures: This would imply to express in the logic the freshness of the allocated pointers and to maintain the newest versions for each data structures.

Note that these two features are already present in the data structures examples from Section 2.

Another interesting direction would be to provide systematic techniques to make data structures semi-persistent as previously done for persistence [START_REF] Driscoll | Making Data Structures Persistent[END_REF]. Clearly what we did for lists could be extended to tree-based data structures.

It would be even more interesting to formally verify semi-persistent data structure implementations, that is to show that the contents of any ancestor of the version being updated is preserved. Since such implementations are necessarily using imperative features (otherwise they would be fully persistent), proving their correctness requires verification techniques for imperative programs. This could be done for instance using verification tools such as SPEC# [START_REF] Barnett | The Spec# programming system: An overview[END_REF] or Caduceus [START_REF] Filliâtre | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (Tool presentation)[END_REF]. However, we would prefer verifying Ocaml code, as given in Section 2 for instance, but unfortunately there is currently no tool to handle such code.

e

  ::= x | c | p | f e | let x = e in e | if e then e else e d ::= fun f (x : ι) = {φ} e {ψ} ι ::= semi | δ | boolA program expression is either a variable (x), a constant (c), a pointer (p), a function call, a local variable introduced by a let binding, or a conditional. The set of function names f includes some primitive operations (introduced in the next section). A function definition d introduces a function f with exactly one argument x of type ι, a precondition φ, a body and a postcondition ψ. A type ι is either the type semi of the semi-persistent data structure, the type δ of the values it contains, or the type bool of booleans. The syntax of pre-and postconditions will be given later in Section 4. A program ∆ is a finite set of mutually recursive functions.

  then e else e v ::= c | p S ::= p • • • p if true then e 1 else e 2 , S → e 1 , S if false then e 1 else e 2 , S → e 2 , S let

Figure 1 :

 1 Figure 1: Operational Semantics

Figure 2 :

 2 Figure 2: Typing Rules

Figure 3 :

 3 Figure 3: Constraint synthesis

Lemma 3

 3 If |= ∀ret. ∀cur . φ 1 ⇒ φ 2 and |= C(e, φ 1 ) then |= C(e, φ 2 ).

Lemma 6 •

 6 Let S be a state, φ be a formula and e a program expression. If S |= C(e, φ) and e, S → e ′ , S ′ then S ′ |= C(e ′ , φ). Proof. The proof is done by induction on e: • If e = if true then e 1 else e 2 then e ′ = e 1 and S ′ = S. We have C(e, φ) = C(true, C(e 1 , φ) ∧ C(e 2 , φ)) = C(e 1 , φ) ∧ C(e 2 , φ) since C(e 1 , φ) ∧ C(e 2 , φ) cannot refer to a boolean result. Thus S ′ |= C(e ′ , φ). Similarly for if false. If e = let x = v in e 1 then e ′ = e 1 {x ← v} and S ′ = S. We have C(e, φ) = C(v, C(e 1 , φ){x ← ret}) = C(e 1 , φ){x ← v} = C(e 1 {x ← v}, φ), hence the result holds.

  v}, ψ f {x ← v}) and the result follows by Lemma 3. Similarly for f : (x :ι) → ⊤ {φ f } ι ′ {ψ f }. • If e = acc p n then S = S ′ = p 1 • • • p n p n+1 • • • p m and e ′ = A(p n ). We have S |= C(acc p n , φ), that is S |= • • • ∧ ∀ret ′ . true ⇒ φ{ret ← ret ′ }. By instantiating ret ′ by A(p n ) we have S |= φ{ret ← A(p n )} that is S |= C(A(p n ), φ).Since S ′ = S the result holds.• If e = branch p n then S = p 1 • • • p n , S ′ = Sp and e ′ = p with p a fresh pointer.S |= C(branch p n , φ), that is S |= • • • ∧ ∀ret ′ cur ′ . (ret ′ = cur ′ ∧ prev(cur ′ ) = p n ) ⇒ φ{ret ← ret ′ ,cur ← cur ′ }. By instantiating both ret ′ and cur ′ by p, we have S |= (p = p ∧ prev(p) = p n ) ⇒ φ{ret ← p, cur ← p}. Since this formula does not contain cur anymore, it is also valid in S ′ = Sp. Since prev(p) = p n in S ′ then the left hand-side is valid and we have S ′ |= φ{ret ← p, cur ← p}. Since cur is p in S ′ we also have S ′ |= φ{ret ← p} which is C(p, φ).

Finally, we prove the following progress property: Theorem 1

 1 Let S be a state, φ be a formula and e a program expression. If S |= C(e, φ) and e, S → * e ′ , S ′ →, then e ′ is a value.

  It results in a total of 46 N elementary operations and 3(4 6 -1) backtracks. The following table gives timings for various values of N. The code was compiled with the Ocaml native-code compiler (ocamlopt -unsafe) on a dual core Pentium 2.13GHz processor running under Linux. The timings are given in seconds and correspond to CPU time obtained using the UNIX times system call.

		N 200 1000 5000 10000
	persistent arrays	0.21 1.50 13.90	30.5
	semi-persistent arrays	0.18 1.10 7.59	17.3
	persistent lists	0.18 2.38 50.20 195.0
	semi-persistent lists	0.11 0.76 8.02	31.1
	persistent hash tables	0.24 2.15 19.30	43.1
	semi-persistent hash tables 0.22 1.51 11.20	28.2
	then
	let t = ... operation on t ... in
	descend h (k+1) t
	else if h < 6 then begin (* branch *)
	descend (h+1) 0 t;
	descend (h+1) 0 t;
	descend (h+1) 0 t;
	descend (h+1) 0 t
	end
	in
	descend 0 0 t

  cur ← cur ′ }. By instantiating both ret ′ and cur ′ by p n , we have S |= φ{ret ← p n , cur ← p n }. Since this formula only refers to the first element of S, which is also by Lemma 1 the first element of S ′ , we haveS ′ |= φ{ret ← p n , cur ← p n } and thus S ′ |= φ{ret ← p n } (since cur is p n in S ′ ), that is S ′ |= C(p, φ). • If e = E[e 1 ] and E[e 1 ], S → E[e ′ 1 ], S ′ with e 1 , S → s ′ 1 , S ′ ,then S |= C(e 1 , E[φ]) by Lemma 4. By induction hypothesis on e 1 we have S ′ |= C(e ′ 1 , E[φ]). Then again by Lemma 4 we have S ′ |= C(E[e ′ 1], φ).

  Theorem 2 decide(H, a) returns true if and only if H |= a.Proof. (Soundness) Let M be a model of H and let us show that M is a model of a. Obviously, M is also a model of H ⋆ . If a is path(t 1 , t 2 ) then the proof is by induction on the length of the path. If the path has length 0, then t 1 ≡ t 2 and the result holds since M is a model of axiom (A 1 ). Otherwise, we proceed by case analysis on the last step of the path since M is a model of the transitivity axiom (A ⋆ . If the last step is an edge corresponding to t 3 = t 4 ∈ H ⋆ , then M is a model of path(t 3 , t 4 ) by axiom (A 1 ) and axioms of equality.(Completeness) Let us assume that H |= a. If a is t 1 = t 2 then t 1 = t 2 ∈ H ⋆ by definition of the congruence closure, and thus the algorithm returns true. If a is path(t 1 , t 2 ) we proceed by induction on the proof of H |= a and by case analysis on the last rule:• (A 1 ): There is an empty path from t 1 to t 2 .• (A 2 ): We have H |= path(t 1 , prev(t 2 )). By Lemma 2, we have prev(t 2 ) ∈ S(H) and thus we can apply the induction hypothesis. So there is a path from t 1 to prev(t 2 ) and thus a path from t 1 to t 2 .• (A 3 ): We have H |= path(t 1 , t) and H |= path(t, t 2 ). By Lemma 2, we have t ∈ S(H) and thus we can apply the induction hypothesis. • Congruence: We have H |= u 1 = t 1 , H |= u 2 = t 2 and H |= path(u 1 , u 2 ). Thus we have H |= path(u 1 , t 1 ) and H |= path(u 2 , t 2 ) (as above) and H |= path(u 1 , u 2 ) by induction hypothesis; the result follows.

[START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF]

). If the last step is an edge from prev(t) to t then the result holds since M is a model of both (A 1 ) and (A 2 ). If the last step is an edge corresponding to path(t 3 , t 4 ) ∈ H ⋆ then the results holds since M is a model of H

Definition 1 The theory T is defined as the combination of the theory of equality and the following axioms:

(A 1 ) ∀x. path(x, x) (A 2 ) ∀xy. path(x, prev(y)) ⇒ path(x, y) (A 3 ) ∀xyz. path(x, y) ∧ path(y, z) ⇒ path(x, z)

We write |= φ if φ is valid in any model of T .

The three axioms (A 1 )-(A 3 ) exactly define path as the reflexive transitive closure of prev -1 , since we consider validity in all models of T and therefore in those where path is the smallest relation satisfying axioms (A 1 )-(A 3 ). Note that prev is a total function and that there is no notion of "root" in our logic. Thus a version always has an immediate ancestor, which may or may not be valid.

To account for the modification of the newest version as program execution progresses, we introduce a "mutable" variable cur to represent the newest version. This variable does not appear in programs: its scope is limited to annotations. The only way to modify its contents is to call the primitive operations backtrack and branch. We are now able to give the full type expressions for the three primitive operations:

As expected, effect ⊤ for the first two reflects the modification of cur . The validity of function argument x is expressed as path(x, cur ) in operations backtrack and acc.

Note that acc has no postcondition (written true and which could stand for the tautology cur = cur ) since we are not interested in the values contained in the data structure.

We are now able to define the judgements used in Section 3.4 for pre-and postconditions. We write Γ ⊢ φ pre as syntactic sugar for Γ, cur : semi ⊢ φ. Similarly, Γ ⊢ ψ post ι is syntactic sugar for Γ, cur : semi, ret : ι ⊢ ψ when return type ι is semi and for Γ, cur : semi ⊢ ψ otherwise. Note that since Γ only contains the function argument x in typing rule Fun, the function precondition may only refer to x and cur , and its postcondition to x, cur and ret.

In Section 4.5, we will need the following subterms property:

Lemma 2 If H is a set of atoms, t 1 a subterm of H and H |= path(t 1 , t 2 ) then t 2 is a subterm of H.

Constraints

We now define the set of constraints associated to a given program. This is mostly a weakest precondition calculus, which is greatly simplified here since we have only one mutable variable (namely cur ). For a program expression e and a formula φ we write


Kevin Falzone

Sophie Lemonnier

Thibaut Grébert

J M Christian Bastien

Bastien 2023 Christian

Using Scarf Plots to Visualize Moment-to-Moment Visual Search Behavior on Websites Des scarf plots pour visualiser la dynamique des comportements visuels de recherche d'information sur sites Web

Keywords: Human-centered computing → Visualization, Web-based interaction, Hypertext / hypermedia visualization, eye tracking, scarf plot, transition, information search, web, moment-to-moment behavior visualisation, oculométrie, graphique en écharpe, recherche d'information, web, dynamique des comportements

Despite a large number of metrics and eye-tracking data visualization techniques allowing us to study information search on the Internet, the moment-to-moment dynamics of this process has not been taken into account. Therefore, the aim of this paper is to show the interest of visualization methods such as scarf plots. An adaptation of these visualizations has been developed and applied to a dataset of 46 participants who have performed an information search task on a website. Compared to the techniques usually used, our approach allows us, on the one hand, to illustrate the information search behaviors of each individual in one figure (the total duration of the search, the path of the web pages, the number of web pages, the duration of web page exploration, the areas of interest explored, etc.), and on the other hand, to juxtapose several individuals, thus allowing us to easily compare and categorize them.

CCS Concepts: •

INTRODUCTION

In recent years, eye-tracking has been widely used in the field of information search on the Internet [START_REF] Linden | Eye Movement in User Experience and Human-Computer Interaction Research[END_REF][START_REF]Eye Tracking in User Experience Design[END_REF][START_REF] Lund | Eye Tracking in Library and Information Science: A Literature Review[END_REF][START_REF] Nielsen | Eyetracking Web Usability[END_REF][START_REF] Strzelecki | Eye-Tracking Studies of Web Search Engines: A Systematic Literature Review[END_REF]. It allows us to track and record continuously, and in real time, the position of the individuals' gaze on a web page. Two common events are identified from the recorded data: fixations and saccades [START_REF] Holmqvist | Eye Tracking: A Comprehensive Guide to Methods, Paradigms, and Measures[END_REF].

The fixation is a static state of the eye that makes it possible to collect visual information. The saccade is a rapid movement of the eye between two fixations. It is used to move from one source of information to another. The main 2023. Manuscript submitted to ACM measures used to characterize these two events are the number of fixations and their duration as well as the amplitudes of saccades [START_REF] Lemonnier | Oculométrie. In Ergonomie : 150 notions clés[END_REF]. In order to characterize the visual search of an individual, descriptive statistics such as the mean, the median or the standard deviation of the fixation times, or the saccade amplitudes, are calculated either by page or by area of interest (AOI).

These global indicators, can be represented by plots (e.g., histograms, box plots, scatter plots, line plots, etc.). Other visualizations exist for eye-tracking data. Each of these visualizations falls into one of two categories: those based on points (point-based) and those based on areas of interest (AOI-based) [START_REF] Blascheck | Visualization of Eye Tracking Data: A Taxonomy and Survey: Visualization of Eye Tracking Data[END_REF].

Point-based visualization techniques rely essentially on the coordinates and temporality of the eye-tracking data.

The two most widely used techniques are attention maps and scanpaths. As an illustration, in a systematic review of the literature published in 2020, 30% of the papers listed (from 2004 to 2019) used attention maps [START_REF] Strzelecki | Eye-Tracking Studies of Web Search Engines: A Systematic Literature Review[END_REF]. These visualization techniques are used to compare, for instance, different strategies among groups of individuals [START_REF] Gossen | Usability and Perception of Young Users and Adults on Targeted Web Search Engines[END_REF].

Attention maps are spatial visualization techniques where the fixation density of several individuals is aggregated and color-coded according to the number of fixations and their duration. The most common form is the heatmap (see Figure 1,A). This visualization colors the areas with a graduation from green to red, red representing the region most fixated. There are other types of visualisations such as the focus map, which masks in black the areas that are not looked at, and lets appear the looked ones (see Figure 1,B). Scanpaths (or gazeplots) are a spatio-temporal visualization technique. In contrast to the attention map, which is only spatial (see Figure 1, C), it presents all the fixations and saccades. Each fixation is materialized by a circle and each saccade by a line that joins two fixations. For the fixations, two other pieces of information are also represented graphically: the size of the circle which increases with the duration of the fixation and the sequence order of the fixation which is indicated by a number inside each circle.

Attention maps can highlight the most viewed areas by aggregating a large number of users in the same visual space. Scanpaths, on the other hand, are quickly cluttered, even unreadable, as the number of users increases. Nevertheless, the scanpaths have the double advantage of preserving individual specificities and showing the temporality of events. AOI-based visualization techniques rely on the definition of areas of interest, that is, the division of the visual environment into zones. These areas can be defined semantically [START_REF]Eye Tracking in User Experience Design[END_REF] (i.e., source of information relevant or not for the task), grid-based [START_REF] Tullis | Measuring the User Experience: Collecting, Analyzing, and Presenting Usability Metrics[END_REF] or data-based [START_REF] Drusch | Analyzing Web Pages Visual Scanpaths: Between and within Tasks Variability[END_REF][START_REF] Drusch | Analysing eye-tracking data: From scanpaths and heatmaps to the dynamic visualisation of areas of interest[END_REF][START_REF] Drusch | Analyzing Visual Scanpaths on the Web Using the Mean Shift Procedure and T-pattern Detection: A Bottom-up Approach[END_REF].

There are several AOI-based visualizations that use two-dimensional plots in which one axis represents the progress of time and the other axis the areas of interest in which the gaze can stay (e.g., time plot, parallel scanpath visualization, AOI rivers (Figure 2)) [START_REF] Blascheck | Visualization of Eye Tracking Data: A Taxonomy and Survey: Visualization of Eye Tracking Data[END_REF]. These visualizations provide a fine-grained way of studying the behavior of small groups of individuals. However, these classical examples were not designed to compare a large number of individuals.

Scarf plots illustrate gaze transitions among AOI on a timeline. This visualization has been applied to different eye-tracking datasets: visual interactions between a speaker and a listener [START_REF] Daniel | Looking To Understand: The Coupling Between Speakers' and Listeners' Eye Movements and Its Relationship to Discourse Comprehension[END_REF], scientific reading [START_REF] Yang | Alpscarf: Augmenting Scarf Plots for Exploring Temporal Gaze Patterns[END_REF] and the study of subway maps [START_REF] Burch | The Power of Linked Eye Movement Data Visualizations[END_REF]. However, this type of visualization has not been used in the context of information search on the Web.

The aim of this paper is to propose a new visualisation method which would allow us (1) to represent multiple eye-tracking and information search metrics on web pages from a large number of participants in a single visualization, and (2) to make groups of individuals salient. We have chosen to start from the scarf plots, which in our opinion allow us to fulfill these two objectives, and to adapt them to the specificities of information search on the Web. The main specificity of web search that makes visualizations complex is that a search for information requires browsing a collection of web pages. Moreover, it is difficult to visualize multiple pages for a group of individuals with scarf plots as well as heatmaps and scanpaths. The visualization inspired by the scarf plots that we propose in this study overcomes these drawbacks.

METHOD

Participants

A total of 46 participants were recruited at the University of Lorraine in order to carry out an information search task on a website. The sample was composed of 15 men (32.61%), 29 women (63.04%) and 2 others (4.35%), with an average age of 28.5 years (SD = 14.7 years). Eighty percent of the participants were students.

A large majority of participants used to search for information on the Internet several times a week or every day (93.4%), and felt comfortable doing this activity (89.1%). They searched on the Internet using a tablet or a smartphone rather than a computer (78.3%). More than seventy percent of participants had previously visited websites similar to the one proposed in this experiment. However, over three-quarters of the participants had never visited the selected website.

Material

The website of the metropolis of Nancy1 was selected in this experiment because it is mainstream, that is, used by a large population and does not require specific knowledge (see Figure 3). The apparatus was located in a usability lab at the University. The participants were provided with a computer screen (21.5 inch with a 1920x1080 resolution), a wired mouse and a keyboard to interact with the website.

A Tobii Pro Nano bar was placed under the participant's screen in order to capture their gaze. The eye tracker was run by the v.1.8.15.0 firmware and the setup and calibration was performed using the v.2.2.10 Eye Tracker Manager software. The sampling fixations was set to 60Hz.

A laptop was used with the Tobii Pro Lab software (v. 1.194) in order to conduct the experiment, to collect and manage the data.

Procedure

The test sessions were run individually in the observation room of the usability lab.

The aims of the study and the procedure of the experiment were presented to the participants and they were asked to complete a consent form in duplicate.

Once the individuals were settled, the eye tracker calibration phase began. Then, a written reminder of the general instructions was displayed on the monitor and the information seeking task phase started. This phase was conducted as follows: the search instruction appeared, followed by a fixation cross to be looked at, after which the web browser was launched with the home page of the website. The participants' task consisted in finding the name of a waste center that was open on Sundays in the metropolis of Nancy. Upon completion of the task, participants were invited to give the answer orally.

At the end of the experiment, the participants filled out a questionnaire concerning their socio-demographic information and the time spent on Internet. Finally, participants were thanked for their participation.

The experiment lasted an average of 9 min and 56 s (SD = 3 min and 40 s).

Data preparation and analysis

The Tobii Pro lab software was used to define and export several AOI for each web page. The relevant links for the success of the information search task were defined as AOI. The other areas of interest consisted in the header, content and footer of the web pages where relevant links were also located in order to provide additional information. Figure 4 illustrates the AOI of one of the web pages.

To analyze the data from this experiment, we proceeded in two steps: an analysis using the common visualizations (heatmaps and scanpaths) in eye-tracking followed by an exploratory analysis of the moment-to-moment behaviors with an adapted version of the scarf plot.

The construction of the adapted version of the scarf plot was developped using the programming language R [START_REF] Ghaoui | R: A Language and Environment for Statistical Computing[END_REF],

ggplot2 [START_REF] Wickham | Ggplot2: Elegant Graphics for Data Analysis[END_REF] and the Tidyverse packages [START_REF] Wickham | Welcome to the tidyverse[END_REF].

RESULTS

Forty-four participants (95.7%) successfully completed the information search task. Two participants (4.3%), who did not succeed, were excluded from the analyses. Successful participants took an average of 1 min and 21 s (SD = 50 s; Min = 26.76 s; Max = 3 min and 34.55 s) to complete the task.

As shown in Table 1, the number of pages viewed by participants varied from 3 (24 participants) to 17 (1 participant).

Several paths have been taken to find the information. However, the most used path was the sequence "07-16-23".

Heatmaps and Scanpaths

Heatmaps and scanpaths provide a quick way to see where participants focused their attention. As shown on Figures 5 and6, fixations remain primarily focused on the navigation menu links of the home page (page 7). On subsequent pages, participants took more time exploring the content of the page in search for information and links relevant to the task (see Figure 5 and 6, pages 16 and 23).

Heatmaps (Figure 5) are used to show the most viewed areas in each page. On the home page, for example (Figure 5, page 7), the relevant link is located in the menu at the top of the page. This visualization fits very well with a large number of participants as is the case here. However, the absence of a temporality indicator does not allow us to visualize the dynamics of the visual behaviors.

Using the same data, the scanpaths (Figure 6) also show that the visual exploration is mainly focused on the top of the home page. But it also highlights that a certain portion of the visual exploration is made outside of these main areas, giving a slightly more accurate idea of how the web pages were actually explored. However, the large number of participants makes this visualization particularly unreadable. The numbers inside the circles that give information on the sequence of the fixations, as well as their size, are information that cannot be displayed. All of this does not make it possible to highlight individual differences that might exist, or even possible groupings of individuals according to their patterns of exploration.

Web Scarf Plot

3.2.1

The big picture. The web scarf plot describes how each individual has searched for information on a website in a single figure (Figure 7). The timeline for each participant gives us information such as the duration of the search, the path taken, the number of pages consulted, the duration of exploration for each page and the areas of interest explored. The web pages materialized by rectangles have been color-coded. Each web page is assigned a specific color. This way, it is possible to know which pages have been browsed and for how long.

Inside each colored rectangle (i.e, the web pages), we find the AOIs previously defined. The AOIs delimiting the zones of the web page (i.e., header, content, and footer) are each placed on a different line. The visual exploration of a given AOI is materialized by a black vertical line. When relevant links are seen in an AOI, they are represented by yellow vertical lines. The number of vertical lines indicates the duration of fixation.

In Figure 7, participants were sorted on the basis of three criteria: the path taken, the duration of the total search and the time spent on the home page. This organisation facilitates the identification of similarities and differences in visual search behaviors of the participants. The web scarf plot also allows us to visually compare users both on the basis of their visual exploration and on more global metrics such as the duration of the search, the number of pages consulted, etc. Finally, it allows us to easily notice patterns at an inter-individual or individual level. If we look at the upper part of that figure, we have the 24 participants that went through web pages 7, 16 and 23. Their path is identical, and as it is easily noticeable, some of those partipcipants took approximately the same time to find the information they were looking for. But others spent a lot more time on page 23. And when looking at the figure, we easily observe the differences between the first 24 participants and the rest of the group.

Focus on four participants.

Even if this type of visualization lets you put all the participants and a certain number of metrics in the same illustration, it is also possible to zoom in on specific participants in order to compare their behavior more closely at different levels. To illustrates this, we chose to focus on four participants: 4, 39, 44 and 5 shown in Figure 8. These four participants are globally equivalent in terms of task duration. However, they differ on other metrics.

It can be noticed that participant 4, starting from the home page, consults different pages in comparison to the three other participants, who follow strictly the same path.

Participant 39, even if he visits the same pages and in the same order as participants 44 and 5, does not spend the same amount of time on each of these pages, with a very long visit duration on the home page, and conversely a very short duration on the final page.

Participants 44 and 5, differ in their visual exploration of the pages. On the home page in particular, we can notice that participant 5 focuses almost exclusively on the header AOI, then exclusively on the content AOI, before clicking on a link. Participant 44, on this same page, switches many times between these two AOIs.

DISCUSSION

In this paper, we have presented an extension of the scarf plots -web scarf plots -to support the visual analyses of information search behaviors on websites. This visualization proposes to depict the moment-to-moment of one or more individuals' visual behaviors across web pages. This visualization makes it possible to compare several users based on metrics commonly used in the field of human-computer interaction such as the total task duration, the path and the duration of each page exploration [START_REF] Tullis | Measuring the User Experience: Collecting, Analyzing, and Presenting Usability Metrics[END_REF].

Moreover, two other metrics from the visual behavior have been integrated to this visualization: the visited AOI, and on specific AOI, the relevant link that has to be clicked-on to accomplish the task. This was made possible by the way the AOIs were coded, which was done on two levels of granularity. AOIs were defined in order to divide the whole visual environment into three areas: the header, the content and the footer of the page. Then, in each of these AOI, the hyperlinks relevant for the task were defined as AOI. These two levels of coding were built semantically so as to be generalized to all the pages that could be visited. All this allows a simplified and efficient visualization of these visual behaviors.

In the field of information search on the Internet, to be able to classify users could facilitate the study of the dynamics of the visual search behaviors, the variability of those behaviors as well as the discovery of behavioral patterns. The identification of behavioral patterns through classification could also allow to adapt an interface to different users or to predict a risk of failure, which could complement the usual approach based on global indicators [START_REF] Becker | Patterns comportementaux sur la page d'accueil et performances de navigation sur les sites web[END_REF].

The way the metrics have been encoded to allow this visualization could be given as input to quantitative methods such as T-patterns [START_REF] Magnusson | Discovering Hidden Time Patterns in Behavior: T-patterns and Their Detection[END_REF] or classifiers (e.g., k-Nearest Neighbors [START_REF] Cover | Nearest Neighbor Pattern Classification[END_REF]). However, the objective of this study was to produce a visual classification tool. Indeed, the fact of classifying individuals according to certain indicators brings out visual groupings. In our example, by sorting the participants according to the path taken, the duration of the task, the number of pages consulted, the optimal path to find the requested information becomes obvious. A different sorting could have been done, for example, by sorting the participants only on the duration of the task, in order to see whether the number of pages correlates or not with task duration.

In the future, other eye-tracking metrics could be used such as those proposed by Poole and Ball [START_REF] Poole | Eye Tracking in HCI and Usability Research[END_REF] and Ball and Richardson [START_REF] Linden | Eye Movement in User Experience and Human-Computer Interaction Research[END_REF]: the coloring of the saccade/fixation ratio; the time to first fixation; the total length of scanpaths, which accounts for the efficiency of visual exploration; the spatial density, which accounts for a more or less direct visual search. In the same way, the coefficient K [START_REF] Krejtz | Discerning Ambient/Focal Attention with Coefficient K[END_REF], which accounts for the focal or ambient attention, could be added.

Still using eye-tracking data, where we had divided the AOI into relevant and other links, it would be possible to add a third category with the surrounded links. These links are those that are located in the same cluster as a relevant link. This would allow us to discuss the strategy of how a link is consulted, or even the significance of the links.

Finally, it would also be possible to add other more conventional indicators in the field of human-computer interaction, such as clicks and scrolls, which reflect the effort made by the individual. This would lead to a more complete view of the user experience.

CONCLUSION

In this work, we propose a visualization tool, the web scarf plots, which is an adaptation of the scarf plots to visual information search on websites. Despite the exploratory dimension of this work, it opens many perspectives, notably by the possible addition of indicators characteristic of visual exploration on the one hand or of user experience on the other hand. This tool can be used to look differently at the collected data. It could thus be used by researchers who wish to report on behavioral dynamics, as well as by user experience experts.

Fig. 1 .Fig. 2 .

 12 Fig. 1. The same data set represented by a heatmap, a focusmap and a scanpath.

Fig. 3 .

 3 Fig. 3. Home page screen of the selected website.

Fig. 4 .Fig. 5 .Fig. 6 .

 456 Fig. 4. Example of AOI definition for a given web page.

Table 1 .

 1 Number of participants having visually explored the different sequences of web pages. Each number under the clicstream column corresponds to a specific web page.

	Clickstreams

https://www.grandnancy.eu

Fig. 8. The scarf plot for four participants [START_REF] Burch | The Power of Linked Eye Movement Data Visualizations[END_REF]44,39,[START_REF] Blascheck | Visualization of Eye Tracking Data: A Taxonomy and Survey: Visualization of Eye Tracking Data[END_REF].