## In-Place Linked-List Reversal in Why3

This is a Why3 version of the classical example of in-place linked-list reversal

Authors: Claude Marché

Tools: Why3

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

# In-place linked list reversal

Version designed for the MPRI lecture ``Proof of Programs''

This is an improved version of this one: it does not use any Coq proofs, but lemma functions instead.

```module InPlaceRev

use map.Map
use ref.Ref
use int.Int
use list.List
use list.Quant as Q
use list.Append
use list.Mem
use list.Length
use export list.Reverse

type loc

val function eq_loc (l1 l2:loc) : bool
ensures { result <-> l1 = l2 }

val constant null : loc

predicate disjoint (l1:list loc) (l2:list loc) =
forall x:loc. not (mem x l1 /\ mem x l2)

predicate no_repet (l:list loc) =
match l with
| Nil -> true
| Cons x r -> not (mem x r) /\ no_repet r
end

let rec ghost mem_decomp (x: loc) (l: list loc)
: (l1: list loc, l2: list loc)
requires { mem x l }
variant  { l }
ensures  { l = l1 ++ Cons x l2 }
= match l with
| Nil -> absurd
| Cons h t -> if eq_loc h x then (Nil,t) else
let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
end

val acc (field: ref (map loc 'a)) (l:loc) : 'a
requires { l <> null }
reads { field }
ensures { result = get !field l }

val upd (field: ref (map loc 'a)) (l:loc) (v:'a):unit
requires { l <> null }
writes { field }
ensures { !field = set (old !field) l v }

inductive list_seg loc (map loc loc) (list loc) loc =
| list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p
| list_seg_cons: forall p q:loc, next:map loc loc, l:list loc.
p <> null /\ list_seg (get next p) next l q ->
list_seg p next (Cons p l) q

let rec lemma list_seg_frame_ext (next1 next2:map loc loc)
(p q r v: loc) (pM:list loc)
requires { list_seg p next1 pM r }
requires { next2 = set next1 q v }
requires { not (mem q pM) }
variant  { pM }
ensures  { list_seg p next2 pM r }
= match pM with
| Nil -> ()
| Cons h t ->
assert { p = h };
list_seg_frame_ext next1 next2 (get next1 p) q r v t
end

let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc)
requires { list_seg p next l1 null }
requires { list_seg p next l2 null }
variant  { l1 }
ensures  { l1 = l2 }
= match l1,l2 with
| Nil, Nil -> ()
| Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p)
| _ -> absurd
end

let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc)
requires { list_seg p next (l1 ++ Cons q l2) null }
variant { l1 }
ensures { list_seg q next (Cons q l2) null }
= match l1 with
| Nil -> ()
| Cons _ r -> list_seg_sublistl next r l2 (get next p) q
end

let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc)
requires { list_seg p next pM null }
variant  { pM }
ensures  { no_repet pM }
= match pM with
| Nil -> ()
| Cons h t ->
if mem h t then
(* absurd case *)
let (l1,l2) = mem_decomp h t in
list_seg_sublistl next (Cons h l1) l2 p h;
list_seg_functional next pM (Cons h l2) p;
assert { length pM > length (Cons h l2) }
else
list_seg_no_repet next (get next p) t
end

let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc)
requires { list_seg p next pM q }
requires { list_seg q next qM r }
variant  { pM }
ensures  { list_seg p next (pM ++ qM) r }
= match pM with
| Nil -> ()
| Cons _ t ->
list_seg_append next (get next p) q r t qM
end

val next : ref (map loc loc)

let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc
requires { list_seg l1 !next l1M null }
requires { list_seg l2 !next l2M null }
requires { disjoint l1M l2M }
ensures { list_seg result !next (l1M ++ l2M) null }
=
if eq_loc l1 null then l2 else
let p = ref l1 in
let ghost pM = ref l1M in
let ghost l1pM = ref (Nil : list loc) in
while not (eq_loc (acc next !p) null) do
invariant { !p <> null }
invariant { list_seg l1 !next !l1pM !p }
invariant { list_seg !p !next !pM null }
invariant { !l1pM ++ !pM = l1M }
invariant { disjoint !l1pM !pM }
variant   { !pM }
match !pM with
| Nil -> absurd
| Cons h t ->
pM := t;
assert { disjoint !l1pM !pM };
assert { not (mem h !pM) };
l1pM := !l1pM ++ Cons h Nil;
end;
p := acc next !p
done;
upd next !p l2;
assert { list_seg l1 !next !l1pM !p };
assert { list_seg !p !next (Cons !p Nil) l2 };
assert { list_seg l2 !next l2M null };
l1

let in_place_reverse (l:loc) (ghost lM:list loc) : loc
requires { list_seg l !next lM null }
ensures  { list_seg result !next (reverse lM) null }
= let p = ref l in
let ghost pM = ref lM in
let r = ref null in
let ghost rM = ref (Nil : list loc) in
while not (eq_loc !p null) do
invariant { list_seg !p !next !pM null }
invariant { list_seg !r !next !rM null }
invariant { disjoint !pM !rM }
invariant { (reverse !pM) ++ !rM = reverse lM }
variant   { !pM }
let n = get !next !p in
upd next !p !r;
assert { list_seg !r !next !rM null };
r := !p;
p := n;
match !pM with
| Nil -> absurd
| Cons h t -> rM := Cons h !rM; pM := t
end
done;
!r

end

```

Using sequences instead of lists

```module InPlaceRevSeq

use int.Int
use map.Map as Map
use seq.Seq
use seq.Mem
use seq.Reverse

type loc

val function null: loc

val function eq_loc (l1 l2:loc) : bool
ensures { result <-> l1 = l2 }

predicate disjoint (s1: seq 'a) (s2: seq 'a) =
(* forall x:'a. not (mem x s1 /\ mem x s2) *)
forall i1. 0 <= i1 < length s1 ->
forall i2. 0 <= i2 < length s2 ->
s1[i1] <> s2[i2]

predicate no_repet (s: seq loc) =
forall i. 0 <= i < length s -> not (mem s[i] s[i+1..])

lemma non_empty_seq:
forall s: seq 'a. length s > 0 ->
s == cons s[0] s[1..]

let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc)
requires { mem x s }
variant  { length s }
ensures  { s == s1 ++ cons x s2 }
=
if eq_loc s[0] x then (empty, s[1..])
else begin
assert { s == cons s[0] s[1..] };
let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2)
end

use ref.Ref

type memory 'a = ref (Map.map loc 'a)

val acc (field: memory 'a) (l:loc) : 'a
requires { l <> null }
reads    { field }
ensures  { result = Map.get !field l }

val upd (field: memory 'a) (l: loc) (v: 'a) : unit
requires { l <> null }
writes   { field }
ensures  { !field = Map.set (old !field) l v }

type next = Map.map loc loc

predicate list_seg (next: next) (p: loc) (s: seq loc) (q: loc) =
let n = length s in
(forall i. 0 <= i < n -> s[i] <> null) /\
(   (p = q /\ n = 0)
\/ (1 <= n /\ s[0] = p /\ Map.get next s[n-1] = q /\
forall i. 0 <= i < n-1 -> Map.get next s[i] = s[i+1]))

lemma list_seg_frame_ext:
forall next1 next2: next, p q r v: loc, pM: seq loc.
list_seg next1 p pM r ->
next2 = Map.set next1 q v ->
not (mem q pM) ->
list_seg next2 p pM r

let rec lemma list_seg_functional (next: next) (l1 l2: seq loc) (p: loc)
requires { list_seg next p l1 null }
requires { list_seg next p l2 null }
variant  { length l1 }
ensures  { l1 == l2 }
= if length l1 > 0 && length l2 > 0 then begin
assert { l1[0] = l2[0] = p };
list_seg_functional next l1[1..] l2[1..] (Map.get next p)
end

let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc)
requires { list_seg next p l1 q }
requires { length l1 > 0 }
variant  { length l1 }
ensures  { list_seg next (Map.get next p) l1[1..] q }
= if length l1 > 1 then
list_seg_tail next l1[1..] (Map.get next p) q

let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc)
requires { list_seg next p pM q }
requires { list_seg next q qM r }
variant  { length pM }
ensures  { list_seg next p (pM ++ qM) r }
=  if length pM > 0 then
list_seg_append next (Map.get next p) q r pM[1..] qM

lemma seq_tail_append:
forall l1 l2: seq 'a.
length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2

let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc)
requires { list_seg next p (l1 ++ cons q l2) null }
variant  { length l1 }
ensures  { list_seg next p l1 q }
= if length l1 > 0 then begin
list_seg_tail next (l1 ++ cons q l2) p null;
list_seg_prefix next l1[1..] l2 (Map.get next p) q
end

let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc)
requires { list_seg next p (l1 ++ cons q l2) null }
variant  { length l1 }
ensures  { list_seg next q (cons q l2) null }
= assert { list_seg next p l1 q };
if length l1 > 0 then begin
list_seg_tail next l1 p q;
list_seg_sublistl next l1[1..] l2 (Map.get next p) q
end

lemma get_tail:
forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1]
lemma tail_suffix:
forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..]

let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc)
requires { list_seg next p pM null }
variant  { length pM }
ensures  { no_repet pM }
= if length pM > 0 then begin
let h = pM[0] in
let t = pM[1..] in
if mem h t then
(* absurd case *)
let (l1,l2) = mem_decomp h t in
list_seg_sublistl next (cons h l1) l2 p h;
list_seg_functional next pM (cons h l2) p;
assert { length pM > length (cons h l2) }
else begin
assert { not (mem pM[0] pM[0+1..]) };
list_seg_no_repet next (Map.get next p) t;
assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) }
end
end

val next : ref next

let app (l1 l2: loc) (ghost l1M l2M: seq loc) : loc
requires { list_seg !next l1 l1M null }
requires { list_seg !next l2 l2M null }
requires { disjoint l1M l2M }
ensures  { list_seg !next result (l1M ++ l2M) null }
=
if eq_loc l1 null then l2 else
let p = ref l1 in
let ghost pM = ref l1M in
let ghost l1pM = ref (empty : seq loc) in
ghost list_seg_no_repet !next l1 l1M;
while not (eq_loc (acc next !p) null) do
invariant { !p <> null }
invariant { list_seg !next l1 !l1pM !p }
invariant { list_seg !next !p !pM null }
invariant { !l1pM ++ !pM == l1M }
invariant { disjoint !l1pM !pM }
variant   { length !pM }
assert { length !pM > 0 };
assert { not (mem !p !l1pM) };
let ghost t = !pM[1..] in
ghost l1pM := !l1pM ++ cons !p empty;
ghost pM := t;
p := acc next !p
done;
upd next !p l2;
assert { list_seg !next l1 !l1pM !p };
assert { list_seg !next !p (cons !p empty) l2 };
assert { list_seg !next l2 l2M null };
l1

let in_place_reverse (l:loc) (ghost lM: seq loc) : loc
requires { list_seg !next l lM null }
ensures  { list_seg !next result (reverse lM) null }
= let p = ref l in
let ghost pM = ref lM in
let r = ref null in
let ghost rM = ref (empty: seq loc) in
while not (eq_loc !p null) do
invariant { list_seg !next !p !pM null }
invariant { list_seg !next !r !rM null }
invariant { disjoint !pM !rM }
invariant { (reverse !pM) ++ !rM == reverse lM }
variant   { length !pM }
let n = acc next !p in
upd next !p !r;
assert { list_seg !next !r !rM null };
r := !p;
p := n;
rM := cons !pM[0] !rM;
pM := !pM[1..]
done;
!r

end

```

This time with a fully automated proof.

The key to a fully automated proof is to introduce an array of cells, called `cell` below, and then to resort to arithmetic and universal quantifiers to define lists (predicates `listLR` and `listRL` below).

This proof requires no lemma function and no transformation. A single call to Z3 completes the proof in no time (0.04 s).

```module YetAnotherInPlaceRev

use int.Int
use map.Map

type loc

val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }

val constant null : loc

type mem = { mutable next: loc -> loc }

val mem: mem

let cdr (p: loc) : loc
requires { p <> null }
ensures  { result = mem.next p }
= mem.next p

let set_cdr (p: loc) (v: loc) : unit
requires { p <> null }
ensures  { mem.next = (old mem.next)[p <- v] }
= let m = mem.next in
mem.next <- fun x -> if x = p then v else m x

predicate valid_cells (s: int -> loc) (n: int) =
(forall i. 0 <= i < n -> s i <> null) &&
(forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)

predicate listLR (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
0 <= lo <= hi &&
if lo = hi then l = null else
l = s lo && m.next (s (hi-1)) = null &&
forall k. lo <= k < hi-1 -> m.next (s k) = s (k+1)

predicate listRL (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
0 <= lo <= hi &&
if lo = hi then l = null else
m.next (s lo) = null && l = s (hi-1) &&
forall k. lo < k < hi -> m.next (s k) = s (k-1)

predicate frame (m1 m2: mem) (s: int -> loc) (n: int) =
forall p. (forall i. 0 <= i < n -> p <> s i) ->
m1.next p = m2.next p

let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
requires { valid_cells s n }
requires { listLR mem s l 0 n }
ensures  { listRL mem s r 0 n }
ensures  { frame mem (old mem) s n }
= let ref l = l in
let ref p = null in
let ghost ref i = 0 in
while l <> null do
invariant { if n = 0 then l = p = null else
i = 0     && p = null    && l = s 0
|| i = n     && p = s (n-1) && l = null
|| 0 < i < n && p = s (i-1) && l = s i }
invariant { listRL mem s p 0 i }
invariant { listLR mem s l i n }
invariant { frame mem (old mem) s n }
variant   { n - i }
let tmp = l in
l <- cdr l;
set_cdr tmp p;
p <- tmp;
i <- i + 1
done;
return p

let rec ghost predicate is_list (m: mem) (l: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
variant  { n }
= if n = 0 then l = null else
l = s 0 <> null && is_list m (m.next l) (fun i -> s (i+1)) (n - 1)

let rec lemma cells_of_list (l: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
requires { is_list mem l s n }
variant  { n }
ensures  { valid_cells s n }
ensures  { listLR mem s l 0 n }
= if n <> 0 then cells_of_list (cdr l) (fun i -> s (i+1)) (n - 1)

let rec lemma list_of_cells (r: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
requires { valid_cells s n }
requires { listRL mem s r 0 n }
variant  { n }
ensures  { is_list mem r (fun i -> s (n-1-i)) n }
= if n <> 0 then list_of_cells (cdr r) s (n - 1)

let list_reversal_final (ghost s) (ghost n: int) (l: loc) : (r: loc)
requires { n >= 0 }
requires { is_list mem l s n }
ensures  { is_list mem r (fun i -> s (n-1-i)) n }
ensures  { frame mem (old mem) s n }
= cells_of_list l s n;
let r = list_reversal s n l in
list_of_cells r s n;
r

end

module Termination
```

On a null-terminated list, `list_reversal` terminates. We have shown it already e.g. in the previous module.

But `list_reversal` actually terminates on *any* list, even when it contains a loop. Indeed, the code will reach the loop while reversing the initial segment, will reverse the loop, and then will restore the initial segment. So we end up with a list where only the loop has been reversed.

before +---o<--o<--+ v | o-->o-->o-->o-->o-->o-->o

after +-->o-->o---+ | V o-->o-->o-->o<--o<--o<--o

In the module below, we show that `list_reversal` always terminates. This requires ruling out inifitely-long lists i.e. assuming a finite amount of memory.

```  use int.Int
use int.NumOf
use map.Map

type loc

val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }

val constant null : loc

type mem = { mutable next: loc -> loc }

val mem: mem

let cdr (p: loc) : loc
requires { p <> null }
ensures  { result = mem.next p }
= mem.next p

let set_cdr (p: loc) (v: loc) : unit
requires { p <> null }
ensures  { mem.next = (old mem.next)[p <- v] }
= let m = mem.next in
mem.next <- fun x -> if x = p then v else m x

(* Finite memory hypothesis: the list is entirely contained in a finite
set `s` of `n` cells *)

predicate valid_cells (s: int -> loc) (n: int) =
(forall i. 0 <= i < n -> s i <> null) &&
(forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)

predicate inside_memory (s: int -> loc) (n: int) (l: loc) =
l = null || exists i. 0 <= i < n && l = s[i]

predicate finite_memory (m: mem) (s: int -> loc) (n: int) =
forall i. 0 <= i < n -> inside_memory s n (m.next s[i])

(* The variant is lexicographic, as follows:

- as long as we still discover new cells, we mark them with
increasing numbers (with function `idx` below) and the number
of unmarked cells decreases;

- once we reach a marked cell, this means we are back in the initial
segment and then the mark decreases.
*)

function seen (s: int -> loc) (idx: loc -> int) (lo hi: int) : int =
numof (fun i -> idx s[i] > 0) lo hi

let ghost set_idx (s: int -> loc) (n: int) (idx: loc -> int) (l: loc) (k: int)
requires { valid_cells s n }
requires { inside_memory s n l }
requires { l <> null }
requires { idx l = -1 }
requires { k = seen s idx 0 n >= 0 }
ensures  { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n }
= assert { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n by
exists il. 0 <= il < n && l = s[il] so
seen s idx 0 n = seen s idx 0 il + seen s idx (il+1) n &&
seen s idx[l <- k+1] 0 n =
seen s idx[l <- k+1] 0 il + 1 + seen s idx[l <- k+1] (il+1) n }

let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
requires { n >= 0 }
requires { valid_cells s n }
requires { finite_memory mem s n }
requires { inside_memory s n l }
= let ref l = l in
let ref r = null in
(* marking function: -1 for unmarked / 0 for null / >0 for marked *)
let ghost ref idx = fun p -> if p = null then 0 else -1 in
let ghost ref k = 0 in (* last mark *)
while l <> null do
invariant { inside_memory s n l }
invariant { inside_memory s n r }
invariant { finite_memory mem s n }
invariant { k = seen s idx 0 n >= 0 }
invariant { forall i. 0 <= i < n -> -1 <= idx s[i] <= k }
invariant { forall p. idx p = 0 <-> p = null }
invariant { if idx l = -1 then
idx r = k && forall i. 0 <= i < n ->
0 < idx s[i] -> idx (mem.next s[i]) = idx s[i] - 1
else forall i. 0 <= i < n ->
0 < idx s[i] <= idx l -> idx (mem.next s[i]) = idx s[i] - 1 }
variant { n - k, 1 + idx l }
if idx l = -1 then (set_idx s n idx l k; k <- k + 1; idx <- idx[l <- k]);
let tmp = l in
l <- cdr l;
set_cdr tmp r;
r <- tmp;
done;
return r

end
```

# Why3 Proof Results for Project "linked_list_rev"

## Theory "linked_list_rev.InPlaceRev": fully verified

 Obligations Alt-Ergo 2.3.3 VC for mem_decomp 0.04 VC for list_seg_frame_ext 0.04 VC for list_seg_functional 0.03 VC for list_seg_sublistl 0.05 VC for list_seg_no_repet 0.06 VC for list_seg_append 0.03 VC for app --- split_vc postcondition 0.01 loop invariant init 0.00 loop invariant init 0.00 loop invariant init 0.00 loop invariant init 0.01 loop invariant init 0.01 precondition 0.01 unreachable point 0.01 assertion 0.02 assertion 0.01 precondition 0.00 loop variant decrease 0.02 loop invariant preservation 0.00 loop invariant preservation 0.06 loop invariant preservation 0.02 loop invariant preservation 0.04 loop invariant preservation 0.06 precondition 0.00 assertion 0.02 assertion 0.02 assertion 0.08 postcondition 0.04 VC for in_place_reverse --- split_vc loop invariant init 0.00 loop invariant init 0.00 loop invariant init 0.00 loop invariant init 0.00 precondition 0.00 assertion 0.02 unreachable point 0.01 loop variant decrease 0.02 loop invariant preservation 0.02 loop invariant preservation 0.02 loop invariant preservation 0.21 loop invariant preservation 0.01 postcondition 0.01

## Theory "linked_list_rev.InPlaceRevSeq": fully verified

 Obligations Alt-Ergo 2.0.0 Alt-Ergo 2.3.3 CVC4 1.8 Eprover 2.0 Z3 4.12.1 non_empty_seq --- 0.01 --- --- --- VC for mem_decomp --- --- --- --- --- split_vc precondition --- 0.01 --- --- --- assertion --- 0.01 --- --- --- precondition --- 0.00 --- --- --- variant decrease --- 0.01 --- --- --- precondition --- 0.01 --- --- --- postcondition --- 0.08 --- --- --- list_seg_frame_ext --- 0.03 --- --- --- VC for list_seg_functional --- --- --- --- --- split_vc assertion --- 0.01 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.00 --- --- --- variant decrease --- 0.01 --- --- --- precondition --- 0.05 --- --- --- precondition --- 0.10 --- --- --- postcondition --- 5.30 --- --- --- VC for list_seg_tail --- --- --- --- --- split_vc precondition --- 0.00 --- --- --- variant decrease --- 0.01 --- --- --- precondition --- 0.03 --- --- --- precondition --- 0.01 --- --- --- postcondition --- 0.08 --- --- --- VC for list_seg_append --- --- --- --- --- split_vc precondition --- 0.00 --- --- --- variant decrease --- 0.01 --- --- --- precondition --- 0.01 --- --- --- precondition --- 0.00 --- --- --- postcondition --- 2.87 --- --- --- seq_tail_append --- 0.03 --- --- --- VC for list_seg_prefix --- --- --- --- --- split_vc precondition --- 0.01 --- --- --- precondition --- 0.01 --- --- --- precondition --- 0.01 --- --- --- variant decrease --- 0.02 --- --- --- precondition --- 0.02 --- --- --- postcondition --- --- --- --- 0.32 VC for list_seg_sublistl --- --- --- --- --- split_vc assertion --- 0.00 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.00 --- --- --- variant decrease --- 0.02 --- --- --- precondition --- 0.02 --- --- --- postcondition --- --- --- --- --- destruct H postcondition --- 0.00 --- --- --- postcondition --- --- --- --- --- assert (l1 = empty) asserted formula --- --- --- 0.05 --- postcondition --- --- --- --- --- assert (forall l:seq 'a. empty ++ l = l) asserted formula --- --- --- --- --- assert (forall l:seq 'a. empty ++ l == l) asserted formula --- 0.03 --- --- --- asserted formula --- 0.02 --- --- --- postcondition --- 0.01 --- --- --- get_tail --- 0.01 --- --- --- tail_suffix --- 0.02 --- --- --- VC for list_seg_no_repet --- --- --- --- --- split_vc precondition --- 0.00 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.41 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.01 --- --- --- assertion --- 0.03 --- --- --- assertion --- 0.00 --- --- --- variant decrease --- 0.01 --- --- --- precondition --- 0.01 --- --- --- assertion --- --- 0.69 --- --- postcondition --- 0.05 --- --- --- VC for app --- --- --- --- --- split_vc postcondition --- 0.03 --- --- --- precondition --- 0.00 --- --- --- loop invariant init --- 0.00 --- --- --- loop invariant init --- 0.01 --- --- --- loop invariant init --- 0.00 --- --- --- loop invariant init --- 0.02 --- --- --- loop invariant init --- 0.01 --- --- --- precondition --- 0.00 --- --- --- assertion --- 0.01 --- --- --- assertion --- 0.06 --- --- --- precondition --- 0.01 --- --- --- precondition --- 0.01 --- --- --- loop variant decrease --- 0.04 --- --- --- loop invariant preservation --- 0.01 --- --- --- loop invariant preservation --- 0.44 --- --- --- loop invariant preservation --- 0.01 --- --- --- loop invariant preservation --- 0.05 --- --- --- loop invariant preservation 1.64 --- --- --- --- remove zero,one,(-),(>),(<=),(>=),get1,set1,([]'),([<-]'),(!),([]),singleton,cons,snoc,(++),reverse,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,length_nonnegative,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'def,([.._])'def,mem_append,mem_tail,eq_loc'spec,non_empty_seq,list_seg_frame_ext,list_seg_functional,list_seg_tail,list_seg_append,seq_tail_append,list_seg_prefix,list_seg_sublistl,get_tail,tail_suffix,Requires2,Requires1,Requires,Ensures11,H1,Ensures10,LoopInvariant8,LoopInvariant7,Ensures9,H,Assert,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures3,LoopInvariant3,LoopInvariant2,LoopInvariant1 loop invariant preservation 0.04 0.05 --- --- --- precondition --- 0.01 --- --- --- assertion --- 0.20 --- --- --- assertion --- 0.07 --- --- --- assertion --- 2.06 --- --- --- postcondition 1.55 --- --- --- --- remove zero,one,(-),(>),(<=),(>=),get1,set1,([]'),([<-]'),(!),([]),singleton,cons,snoc,(++),mem,reverse,disjoint,no_repet,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,length_nonnegative,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,mem_append,mem_tail,eq_loc'spec,non_empty_seq,list_seg_frame_ext,list_seg_functional,list_seg_tail,list_seg_append,seq_tail_append,list_seg_prefix,list_seg_sublistl,get_tail,tail_suffix,list_seg_no_repet,Requires1,Requires,Ensures3,H1,Ensures2,LoopInvariant4,LoopInvariant3,LoopInvariant postcondition 0.94 4.14 --- --- --- VC for in_place_reverse --- --- --- --- --- split_vc loop invariant init --- 0.00 --- --- --- loop invariant init --- 0.01 --- --- --- loop invariant init --- 0.01 --- --- --- loop invariant init --- 0.02 --- --- --- precondition --- 0.00 --- --- --- precondition --- 0.00 --- --- --- assertion --- 0.34 --- --- --- precondition --- 0.01 --- --- --- loop variant decrease --- 0.03 --- --- --- loop invariant preservation --- 0.28 --- --- --- loop invariant preservation --- 6.91 --- --- --- loop invariant preservation --- --- 0.55 --- --- loop invariant preservation --- --- --- --- --- assert (length pM1 > 0) asserted formula --- 0.02 --- --- --- loop invariant preservation --- --- --- --- --- remove LoopInvariant,LoopInvariant1,LoopInvariant2,LoopInvariant4,LoopInvariant5,LoopInvariant6,Ensures2,Ensures3,Ensures4,Ensures5,Ensures6,Ensures7,Ensures8 loop invariant preservation 1.17 --- --- --- --- remove zero,one,(-),(>),(<=),(>=),get1,set1,([]'),([<-]'),(!),([]),singleton,cons,snoc,(++),mem,disjoint,no_repet,list_seg,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,length_nonnegative,empty'def,set'spec,set'def,([<-])'def,singleton'spec,snoc'spec,([..])'def,([.._])'def,mem_append,mem_tail,eq_loc'spec,non_empty_seq,list_seg_frame_ext,list_seg_functional,list_seg_tail,list_seg_append,seq_tail_append,list_seg_prefix,list_seg_sublistl,get_tail,tail_suffix,list_seg_no_repet,Requires,H,Assert loop invariant preservation 0.02 0.05 --- --- --- postcondition --- 0.08 --- --- ---

## Theory "linked_list_rev.YetAnotherInPlaceRev": fully verified

 Obligations Alt-Ergo 2.4.0 CVC4 1.7 CVC5 1.0.5 Z3 4.12.2 VC for cdr --- --- 0.07 --- VC for set_cdr --- --- 0.09 --- VC for list_reversal --- --- --- 0.04 VC for is_list --- --- 0.07 --- VC for cells_of_list --- --- --- --- split_vc precondition --- --- 0.04 --- variant decrease --- --- 0.02 --- precondition --- --- 0.03 --- precondition --- --- 0.56 --- postcondition 0.79 --- --- --- postcondition 0.06 --- --- --- VC for list_of_cells --- --- --- 1.18 split_vc precondition --- --- 0.04 --- variant decrease --- --- 0.04 --- precondition --- --- 0.03 --- precondition --- --- 0.08 --- precondition --- --- 0.10 --- postcondition --- --- 0.24 --- VC for list_reversal_final --- 0.26 --- ---

## Theory "linked_list_rev.Termination": fully verified

 Obligations Alt-Ergo 2.4.0 CVC5 1.0.5 Z3 4.12.2 VC for cdr --- 0.03 --- VC for set_cdr --- 0.03 --- VC for set_idx --- --- --- split_vc assertion --- --- --- split_vc assertion --- 0.04 --- VC for set_idx --- 0.13 --- VC for set_idx --- 0.55 --- VC for set_idx --- --- 1.02 postcondition --- 0.04 --- VC for list_reversal --- --- --- split_vc loop invariant init --- 0.04 --- loop invariant init --- 0.04 --- loop invariant init --- 0.03 --- loop invariant init --- 0.05 --- loop invariant init --- 0.05 --- loop invariant init --- 0.04 --- loop invariant init --- 0.04 --- precondition --- 0.03 --- precondition --- 0.03 --- precondition --- 0.03 0.01 precondition --- 0.04 --- precondition --- 0.03 --- precondition --- 0.03 --- precondition --- 0.04 --- loop variant decrease --- 0.06 --- loop invariant preservation --- 0.08 --- loop invariant preservation --- 0.04 --- loop invariant preservation --- 0.24 --- loop invariant preservation --- 0.04 --- loop invariant preservation --- 0.05 --- loop invariant preservation --- 0.04 --- loop invariant preservation --- --- --- case (idx l = -1) true case (loop invariant preservation) --- 0.07 --- false case (loop invariant preservation) --- 0.07 --- case (idx l = 0) true case (loop invariant preservation) --- 0.04 --- false case (loop invariant preservation) --- 0.09 --- precondition --- 0.04 --- precondition --- 0.04 --- loop variant decrease --- --- --- right right case --- --- --- split_vc right case --- 0.05 --- right case --- 0.05 --- loop invariant preservation --- 0.08 --- loop invariant preservation --- 0.03 --- loop invariant preservation --- 0.43 --- loop invariant preservation --- 0.04 --- loop invariant preservation --- 0.05 --- loop invariant preservation 0.01 --- --- loop invariant preservation --- --- --- case (idx l = 0) true case (loop invariant preservation) --- --- --- rewrite h true case (loop invariant preservation) --- --- --- compute_in_goal true case (loop invariant preservation) --- 0.04 --- false case (loop invariant preservation) --- 0.04 ---