A Verified Implementation of the Bounded List Container

Implementation: The code is written in a very simple fragment of C, which may be easily translated to most imperative programming languages. It uses records and pointers to records, dynamic memory allocation, classic accesses to record fields and array elements, basic integer type and its operations. Like in the original code, the container does not support concurrency and has been written to obtain efficient operations and not to ease the verification. The container elements are designated through cursors, which represent valid positions in the list; they may be moved forward and backward in the list. The container interface includes 30 operations including classic operations (creation, copy, size access, clearing and deallocation, equality test, searching) and a rich set of utilities (inserting or deleting bunches of elements at some position, searching from the end, merging lists, swapping elements or links, reversing in place, sorting).

Specification: The functional specification is model based [28]. Two mathematical models are used: algebraic lists (i.e., finite sequences) to represent the content of the list and finite partial maps to model the set of valid cursors (see Sect. 2.3 for details). The contracts employ operations on these mathematical models that are beyond their classic usage. For example, the test of inclusion between the set of elements of two sequences, or the test that the domain of a partial mapping has been truncated from a given value. For this reason, we enriched the library of mathematical models provided by our prover with such operations and the corresponding axiomatizations (see Sect. 3.2).

An important feature of our functional specification is the usage of a refined abstraction for the list to ease the proof that the operations satisfy their contracts. We introduce a precise model for the list, which is an algebraic list of abstract cells, storing container values together with the links between the cells. This precise model is mapped to the abstract model (sequence of values) using a catamorphic mapping [35], called . Moreover, the precise model is used to compute the (abstract) model of cursors, based on a catamorphic mapping, called . The use of the precise model facilitates the verification effort for proving that implementations of operations satisfy their contracts (see Sect. 3.1).

The functional specification is complete in the sense given by [27]: the post-condition of each operation uniquely defines its result and the side effect on the model of the container and of its cursors. However, it does not check for memory overflow at the container creation.

For the syntax of specifications, we employ in the following the specification language of VeriFast, which extends the normalized specification language for C, ACSL [3], with shorthand notations and operators for Separation Logic. Therefore, we employ ‘ ’ to introduce existentially quantified variables, ‘ ’ for both classic conjunction and the separating one, ‘ ’ for the points-to operator that defines the content (right operand) of an allocated memory cell (left operand), and for the empty heap. Algebraic lists of VeriFast have type and are polymorphic; the operations on lists have classic names. The definition of new logic types (and functions) is introduced by the keyword (resp. ).

List Elements: The data stored in the list container is typed by an abstract type , defined as an alias to the integer type in our code. This coding is sound for the proof of the functional correctness of the container implementation because the container assumes only that values of may be compared for equality.

List Cell: Also called node in the following, the list cell encapsulates the container element together with links to the next and previous cell in the list. A node is also an element of the array allocated for the container.

The values of the C type are abstracted by the ghost type , defined at line 1 in Fig. 1, which records the values of node fields. The logic functions , , and to access first, second, resp. third component of a value.

The predicate (line 6 in Fig. 1) relates a node allocated in the heap with its model . The allocation property is expressed by the predefined predicate . The values of the fields are bound to existentially quantified variables and used to build the model of the node. The predicate constrains the fields and to be indexes in an array starting at index 0 and ending at index .

There are two kinds of nodes in the array managed by the container: nodes occupied by list elements and nodes not yet used in the list, i.e., free. Free nodes have the field at \(-1\) and the field is irrelevant. They are specified by the predicate (line 14 in Fig. 1), which also constraints the parameter to be equal to the value of the field . Occupied nodes have the field set to a non-negative integer and the field is relevant. The predicate (line 19 in Fig. 1) relates the node with its abstract model.

Acyclic Doubly Linked List: The container stores the doubly linked list (BDLL) into an array of fixed capacity, which is given at the container creation. The number of elements stored in the list can not exceed the container capacity. The nodes of the BDLL are stored starting from the index 1; index 0 plays the role of the null reference. The type of the list container is given by the following record:

The length of the list is given by the field . The first and the last cells of the lists are stored at indexes resp. . Field denotes the start of the list registering the free nodes. The operation creating the container allocates the array and sets at free all nodes in the array. The fields denoting the size and the extreme cells of the doubly linked list are set to 0. The initialization of the field is detailed in the next paragraph.

The representation predicate of the BDLL formed by the occupied nodes, , is defined at line 22 in Fig. 1 as a doubly linked list segment starting by the node at index , ending by the node at index ; the starting node stores as previous node , and the ending node stores as next node . The predicate definition is classic in Separation Logic [24], except the bound constraint on the node indexes (locations). If the source and target indexes are equal, the list is empty; otherwise an occupied node is present at index and it is linked to the previous node and the remainder of the list. Notice the use of pointer arithmetics to access the node at index . The predicate relates the heap specification with the mathematical model of the list, i.e., the sequence of abstract nodes. We employ the polymorphic algebraic type available in VeriFast mathematical library and we instantiate it with the logic type . This precise model of the list content is mapped by the inductively defined ghost function to the abstract model, sequence of values of stored.

Acyclic List of Free Nodes: The free nodes are organized in a singly linked list, called the free-list. The start of this list is given by the field of the type . If is negative, the list is built from all nodes stored between and included; this permits a fast initialization of the free-list at the container creation. If is positive, the free-list starts at index , uses as successor relation the field, and ends at index 0. Figure 2 illustrates the two kinds of free list. The representation predicate (line 31 in Fig. 1) is used when is negative. It collects in the parameter the sequence of the indexes of free nodes. For the second case, we define the predicate (line 38 in Fig. 1). The two kinds of free-list are combined in the predicate (line 45 of Fig. 1) that calls the correct predicate depending on the sign of . Notice that the constraints required by this predicates (the relation between container capacity, BDLL and free-list sizes) are all present in the Ada 2012 specification [12].

Representation Predicate: The invariants of the container are collected in the predicate (line 52 in Fig. 1) which mainly specifies that the container is allocated in the heap (predefined predicate), and its field is also allocated as a block containing \(+1\) records of type . The first node of this array (at address ) has its and fields set to \(-1\) resp. 0. The set of remaining nodes is split between the lists specified by the and predicates due to the separating conjunction. The size of the BDLL is exactly the one of its model and stored in the field .

Examples of Container Contracts: We illustrate the usage of representation predicates defined above by presenting some contracts specifying container operations. For example, the contract of the constructor is:

It states that the resulting container (denoted by the ghost variable ) is a well formed but empty bounded doubly linked list (its abstract model is the empty list) with free nodes. As said before, the above contract (like in Ada 2012 specification), does not consider the case of memory shortage.

The contract of illustrates how the catamorphism is used to obtain the abstract contract on the sequence of values from the precise models (given by variables and for each list parameter):

The operation frees all occupied nodes. Its contract only constrains the content of the doubly linked list and leaves unspecified the free list.

Following the Ada 2012 semantics [1], “a cursor designates a particular node within a list (...). A cursor keeps designating the same node (...) as long as the node is part of the container, even if the node is moved in the container. [...] If [a cursor] is not otherwise initialized, it is initialized to [...] .” Therefore, a cursor is a record storing an array index. The special cursor is defined as a global constant storing the index 0, indeed invalid for a list node (recall that valid nodes are stored from index 1).

The logic type abstracts the cursor implementation (line 1 in Fig. 3). The representation predicate for cursors, (line 3 in Fig. 3), checks that the cursor content, , corresponds to an occupied node in the list using the precise model of the BDLL (see line 13). Moreover, the predicate computes from and , the BDLL starting index, the segments and , into which the cursor splits .

Given a BDLL container, the model of valid cursors for this container is defined (following Ada 2012 specification) as the finite bijection between the set of abstract cursors and the positions (from 1 to the size) in the list. We encode the mathematical type map by an association list, using the polymorphic type provided in the libraries of VeriFast. The cursor model is computed by the logic function (line 19 in Fig. 3) from the container model, the index of the first node in the BDLL, and the first position in the list.

Notice that this manner of specifying cursor model is coherent with the sequence model of the container, because the access to the elements of a sequence is based on positions. However, this specification choice does not combine well with inductive reasoning and induces additional work for the proof (see Sect. 3). We have to enrich the inductive list model with operations using positions. For example, we define the operation which returns the th element of the list . We also defined operations and on association lists to test if an abstract cursor is in the domain of the map resp. to obtain the value to which it is bound.

An example of a contract using cursors is the operation , which returns the value stored at the position in the list given by the cursor :

Contracts of functions changing the positions in the list (e.g., insert or delete) are complete with respect to the model of cursors. For example, consider the post-condition of operation given below, which deletes first elements of the list. It uses a conditional expression (syntax like in C) to specify two contract cases. The first case corresponds to an input container with size less than . In the second case, the container preserved its content after position (predicate ) and the positions of valid cursors in the new container (of model ) are shifted by (predicate ) with respect to the old container.

The contracts provided for our container are in a first order logic over sequences and maps, which employs recursive logic functions. This theory is undecidable so we have to provide lemma to help the prover to tackle verification conditions.

Let us explain why this methodology leads to efficient verification in our case. Consider the specification where (i) the model for the container is the sequence of the values stored and (ii) the model for the cursors is the mapping of occupied nodes to list positions. To capture these models with the representation predicate for the heap, i.e., the predicate defined at line 22 in Fig. 1, we have to replace the model by the sequence of values and the map of cursors . The verification of iterative operations on the list requires to provide a lemma that allows to compose “well linked” list segments into a new list segment, i.e.,

This lemma employs an operation , that concatenates two models of counters and such that the positions associated with counters in are shifted by the size of the domain of . This operation is more difficult to axiomatize than list concatenation. Moreover, all invariant proofs require to keep together the two loosely related models (sequence and map) which leads to less modular proofs. Our solution to this problem is to employ the precise model of the list segment represented by the predicate, as has been presented in Sect. 2.2. The composition lemma for predicate is simpler because it avoids the reasoning on the model of cursors.

The catamorphism mappings used to obtain the abstract model of the container and the model of valid cursors have good inductive definitions and enable efficient decision procedures [35]. However, these decision procedures are not available in our verification tool; this work may be a motivation to add them.

Specification of user types by representation predicates mapping them to inductive types is classical in Separation Logic. We encode the invariant of the BDLL data structure in the predicate . The adoption of C for the implementation keeps us away from the problems of verifying object-related properties, for example. However, this choice leads to an overburden in annotations because we have to specify that parameters of type ‘ ’ satisfy the invariant.

Additional annotation have been supplied to axiomatize global constants (like the record in Fig. 1) and arrays of user-defined structures (like in ).

Contract cases are intensively used in the considered GNAT library. We got around the absence of contract cases in VeriFast using conditional expressions and logic predicate and functions that relate two models (old and new). We do not observe any expressivity or performance problems with this method of encoding contracts.

Specification of model types is done based on the mathematical models sequence (or inductive polymorphic list) and map (or inductive polymorphic association list). The VeriFast libraries including these models (mainly list.*) contain 9 predicates and 20 lemmas, and are not enough for the operations on models required in our specifications. We added tens of lemma and predicates. They are useful not only for the container proof but also for the verification of client programs with inductive back-end solvers. (Nowadays, these proofs are done by GNATprove by calling SMT solvers with quantifiers support.)

More problematic was the lack of support for finite maps and automation of inductive reasoning. VeriFast does not provide sets and finite maps as primitives. The encoding of cursor models by association lists renders more complex the lemmas needed on cursor models. For example, the map inclusion property is defined as follows:

This definition is not as easy to reason about as we might expect. In particular, some properties of this definition of inclusion such as reflexivity are only provable under the additional assumption that the keys are distinct.

We proved that the models of cursors fulfill the constraint (defined also in VeriFast libraries) because keys are index positions in the array used to denote separated cells.

Notice that these proofs are not necessary for provers with support for finite maps and sets. Although VeriFast supports as back-end solver Z3 [9], it does not use it for such theories. The inductive theories are supported by other back-end solvers, e.g., CVC4 [30] that are not connected to VeriFast.

The annotations required by the proof of our library belong to two categories: (1) mandatory annotations including function contracts and predicates employed by these contracts and (2) auxiliary annotations including loop invariants, open/close of predicates, definitions and calls of lemmas.

The prover VeriFast includes all this annotation burden, since we can not direct the prover in the usage of these annotations. VeriFast provides two mechanisms to limit the burden of the auxiliary annotations: (i) lemmas can be marked as automated which means they will be given to the backend solver on all problems, (ii) inductive predicate definitions can be automatically folded and unfolded when used with computed parameters.

We introduce few automated lemmas and call them in order to lighten the prover load. We don’t observe performance problems by including all these annotations and despite the absence of modular proofs. The frame reasoning rule of Separation Logic seems to play an important role in this good behavior.

To resume, we faced the following challenges during the verification process: