## Searching a Linked List, in Why3

Searching the index of the first occurrence of 0 in a linked list of integers, Why3 version

**Authors:** Jean-Christophe Filliâtre

**Topics:** List Data Structure / Searching Algorithms

**Tools:** Why3

**References:** The 1st Verified Software Competition / The VerifyThis Benchmarks

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

(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 3: searching a linked list Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) *) module SearchingALinkedList use import int.Int use import option.Option use import list.List use import list.Length use import list.Nth predicate zero_at (l: list int) (i: int) = nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0 predicate no_zero (l: list int) = forall j:int. 0 <= j < length l -> nth j l <> Some 0 let rec search (i: int) (l: list int) variant {l} ensures { (i <= result < i + length l /\ zero_at l (result - i)) \/ (result = i + length l /\ no_zero l) } = match l with | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end let search_list (l: list int) ensures { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } = search 0 l (* imperative version, with a loop *) use import ref.Ref use import list.HdTl let head (l : list 'a) requires { l <> Nil } ensures { hd l = Some result } = match l with Nil -> absurd | Cons h _ -> h end let tail (l : list 'a) requires { l <> Nil } ensures { tl l = Some result } = match l with Nil -> absurd | Cons _ t -> t end let search_loop l ensures { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } = let i = ref 0 in let s = ref l in while !s <> Nil && head !s <> 0 do invariant { 0 <= !i /\ !i + length !s = length l /\ (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) /\ forall j:int. 0 <= j < !i -> nth j l <> Some 0 } variant { !s } i := !i + 1; s := tail !s done; !i end

download ZIP archive

# Why3 Proof Results for Project "vstte10_search_list"

## Theory "vstte10_search_list.SearchingALinkedList": fully verified in 3.29 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | Coq (8.4pl6) | Z3 (3.2) | ||

VC for search | 0.07 | --- | --- | --- | ||

VC for search_list | 0.01 | 0.00 | --- | 0.00 | ||

VC for head | 0.00 | 0.01 | --- | 0.01 | ||

VC for tail | 0.02 | 0.01 | --- | 0.02 | ||

VC for search_loop | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. loop invariant init | 0.01 | 0.01 | --- | 0.00 | ||

2. precondition | 0.01 | 0.01 | --- | 0.00 | ||

3. precondition | 0.01 | 0.01 | --- | 0.02 | ||

4. loop invariant preservation | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. VC for search_loop | 0.01 | 0.02 | --- | 0.02 | ||

2. VC for search_loop | 0.02 | 0.02 | --- | 0.02 | ||

3. VC for search_loop | --- | --- | 0.88 | --- | ||

4. VC for search_loop | --- | --- | 1.04 | --- | ||

5. loop variant decrease | 0.01 | 0.01 | --- | --- | ||

6. postcondition | --- | --- | 0.96 | --- | ||

7. postcondition | 0.01 | 0.02 | --- | 0.02 |