## Removing an element from a singly-linked list

Removing an element from a singly-linked list.

**Authors:** Jean-Christophe Filliâtre / Andrei Paskevich

**Topics:** List Data Structure / Pointer Programs

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

Removing an element from a singly-linked list.

Authors: Jean-Christophe FilliĆ¢tre (CNRS) Andrei Paskevich (Univ Paris-Saclay)

The following is inspired by this interview of Linus Torvalds:

https://www.youtube.com/watch?v=o8NPllzkFhE

Assume that you are given singly-linked lists in C, like this:

typedef struct Entry *entry; struct Entry { entry next; }; typedef struct List { entry head; } *list;

That is, there is a header structure (struct List) with a 'head' field to the first element of a singly-linked list of list cells (struct Entry).

You are given a list 'l' and some entry 'e' that belongs to the list, and you have to remove it from the list. There is a pedestrian way of doing it, like this:

void remove(list l, entry e) { entry prev = NULL, curr = l->head; while (curr != e) { prev = curr; curr = curr->next; } if (prev) prev->next = curr->next; else l->head = curr->next; }

But there is another one which avoids making a particular case for the first element, like this:

void remove2(list l, entry e) { entry *ind = &l->head; while ( *ind != e ) ind = &( *ind )->next; *ind = ( *ind )->next; }

In the following, we explore the loop invariants involved in the verification of these two programs. We make the following two simplifications:

- The memory model does not make a distinction between the two types of structures. In practice, this is an important point in the discussion. But here we are rather focusing on the loop invariants.

- In the function contract, we underspecify the problem, using only the length of the list, not its contents.

use int.Int use map.Map

Minimal memory model

type loc val (=) (x y: loc) : bool ensures { result <-> x=y } type mem = loc -> loc val ref mem: mem val constant null: loc val constant head: loc val constant entry: loc (* the entry to be removed from the list *)

Program global variables

axiom head_is_not_null : head <> null axiom entry_is_not_null: entry <> null axiom head_is_not_entry: head <> entry

Chains of pointers.

let rec predicate list (mem: loc -> loc) (x: loc) (n :int) (y: loc) requires { n >= 0 } variant { n } = if n = 0 then x = y else x <> null && list mem mem[x] (n - 1) y

When starting from `x`

and dereferencing pointers `n`

times we get `y`

val get (x: loc) : loc requires { x <> null } ensures { result = mem[x] } val set (x y: loc) : unit requires { x <> null } writes { mem } ensures { mem = (old mem)[x <- y] } let rec lemma list_concat (mem: mem) (x: loc) (n1: int) (y: loc) (n2: int) (z: loc) requires { n1 >= 0 } requires { n2 >= 0 } requires { list mem x n1 y } requires { y <> null } requires { list mem mem[y] n2 z } ensures { list mem x (n1 + 1 + n2) z } variant { n1 } = if n1 > 0 then list_concat mem mem[x] (n1 - 1) y n2 z lemma path_shorten: forall mem x n y. list mem x n y -> n > 0 -> list mem mem[x] (n - 1) y lemma path_extend: forall mem x n y. n >= 0 -> list mem y n x -> x <> null -> list mem y (n + 1) mem[x] let rec lemma no_cycle_to_null (mem: mem) (e: loc) (n n': int) requires { 0 < n } requires { 0 <= n' } requires { e <> null } requires { list mem e n e } requires { list mem e n' null } ensures { false } variant { n' } = if n' > 0 then begin list_concat mem mem[e] (n-1) e 0 mem[e]; no_cycle_to_null mem mem[e] n (n' - 1) end let lemma jump_over (mem: mem) (x: loc) (n1: int) (y: loc) (n2: int) requires { n1 >= 0 } requires { list mem x n1 y } requires { y <> null } requires { mem[y] <> null } requires { n2 > 0 } requires { list mem mem[y] n2 null } ensures { list mem[y <- mem[mem[y]]] x (n1 + n2) null } = assert { list mem mem[mem[y]] (n2 - 1) null }; let mem' = mem[y <- mem[mem[y]]] in let rec frame_after (n': int) (z: loc) (n: int) requires { 0 <= n' } requires { list mem y n' z } requires { z <> y } requires { 0 <= n } requires { list mem z n null } ensures { list mem' z n null } variant { n } = if n > 0 then frame_after (n' + 1) mem[z] (n - 1) in let rec frame_before (z: loc) (n: int) requires { n >= 0 } requires { list mem z n y } ensures { list mem' z n y } variant { n } = if n > 0 then frame_before mem[z] (n - 1) in frame_after 1 mem[y] n2; assert { list mem' mem[mem[y]] (n2 - 1) null }; assert { list mem' y n2 null }; frame_before x n1; () (* Code 1 *) let remove1 (ghost n1 n2: int) : unit requires { n1 > 0 } requires { n2 > 0 } requires { list mem head n1 entry } requires { list mem entry n2 null } ensures { list mem head (n1 + n2 - 1) null } = let ref prev = null in let ref curr = get head in let ghost ref n = 1 in while curr <> entry do invariant { 0 < n <= n1 } invariant { list mem head n curr } invariant { curr <> null } invariant { prev = null -> n = 1 } invariant { prev <> null -> mem[prev] = curr } invariant { prev <> null -> list mem head (n - 1) prev } invariant { list mem curr (n1 - n) entry } invariant { list mem entry n2 null } variant { n1 - n } prev <- curr; curr <- get curr; n <- n + 1 done; if prev = null then ( jump_over mem head 0 head n2; set head (get curr); ) else set prev (get curr) (* Code 2 *) let remove2 (ghost n1 n2: int) : unit requires { n1 > 0 } requires { n2 > 0 } requires { list mem head n1 entry } requires { list mem entry n2 null } ensures { list mem head (n1 + n2 - 1) null } = let ref ind = head in let ghost ref n = 1 in while get ind <> entry do invariant { 0 < n <= n1 } invariant { ind <> null } invariant { list mem head (n - 1) ind } invariant { list mem mem[ind] (n1 - n) entry } invariant { list mem entry n2 null } variant { n1 - n } ind <- get ind; n <- n + 1 done; set ind (get entry)

download ZIP archive

# Why3 Proof Results for Project "list_removal"

## Theory "list_removal.Top": fully verified

Obligations | Alt-Ergo 2.3.0 | CVC4 1.7 | Eprover 2.0 | Z3 4.8.6 | ||

VC for list | --- | --- | --- | --- | ||

split_vc | ||||||

variant decrease | 0.00 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

VC for list_concat | --- | --- | --- | --- | ||

split_vc | ||||||

variant decrease | 0.00 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | 0.01 | --- | --- | --- | ||

path_shorten | 0.00 | --- | --- | --- | ||

path_extend | --- | --- | 0.01 | --- | ||

VC for no_cycle_to_null | --- | --- | --- | --- | ||

split_vc | ||||||

precondition | 0.02 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | --- | 0.04 | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

variant decrease | 0.01 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | 0.01 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

VC for jump_over | --- | --- | --- | --- | ||

split_vc | ||||||

assertion | --- | 0.06 | --- | --- | ||

variant decrease | --- | 0.02 | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.06 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

postcondition | --- | 0.02 | --- | --- | ||

variant decrease | --- | 0.02 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

postcondition | --- | 0.10 | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

assertion | --- | 0.03 | --- | --- | ||

assertion | --- | 0.03 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

postcondition | --- | 0.08 | --- | --- | ||

VC for remove1 | --- | --- | --- | --- | ||

split_vc | ||||||

precondition | --- | 0.03 | --- | --- | ||

loop invariant init | --- | --- | --- | --- | ||

split_vc | ||||||

loop invariant init | 0.01 | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | --- | 0.02 | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

loop variant decrease | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | ||

loop invariant preservation | --- | 0.01 | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.01 | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.03 | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | 0.02 | --- | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

postcondition | --- | --- | --- | 0.02 | ||

precondition | 0.00 | --- | --- | --- | ||

precondition | --- | --- | --- | --- | ||

split_vc | ||||||

precondition | --- | --- | --- | 0.03 | ||

postcondition | --- | 2.60 | --- | --- | ||

VC for remove2 | --- | --- | --- | --- | ||

split_vc | ||||||

loop invariant init | 0.01 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | ||

precondition | 0.01 | --- | --- | --- | ||

precondition | 0.01 | 0.02 | --- | --- | ||

loop variant decrease | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

postcondition | --- | --- | --- | 0.02 |