## Coincidence count

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

**Topics:** Array Data Structure

**Tools:** Why3

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

Coincidence count

Exercise proposed by Rustan Leino at Dagstuhl seminar 14171, April 2014

You are given two sequences of integers, sorted in increasing order and without duplicate elements, and you count the number of elements that appear in both sequences (in linear time and constant space).

Authors: Jean-Christophe FilliÃ¢tre (CNRS) Andrei Paskevich (UniversitÃ© Paris Sud)

module CoincidenceCount use import array.Array use import ref.Refint use import set.Fsetint use import set.FsetComprehension function setof (a: array 'a) : set 'a = map (get a) (interval 0 (length a)) function drop (a: array 'a) (n: int) : set 'a = map (get a) (interval n (length a)) lemma drop_left: forall a: array 'a, n: int. 0 <= n < length a -> drop a n == add a[n] (drop a (n+1)) predicate increasing (a: array int) = forall i j: int. 0 <= i < j < length a -> a[i] < a[j] function cc (a b: array int) : int = cardinal (inter (setof a) (setof b)) lemma not_mem_inter_r: forall a: array int, i: int, s: set int. 0 <= i < length a -> not (mem a[i] s) -> inter (drop a i) s == inter (drop a (i+1)) s lemma not_mem_inter_l: forall a: array int, i: int, s: set int. 0 <= i < length a -> not (mem a[i] s) -> inter s (drop a i) == inter s (drop a (i+1)) let coincidence_count (a b: array int) : int requires { increasing a } requires { increasing b } ensures { result = cc a b } = let i = ref 0 in let j = ref 0 in let c = ref 0 in while !i < length a && !j < length b do invariant { 0 <= !i <= length a } invariant { 0 <= !j <= length b } invariant { !c + cardinal (inter (drop a !i) (drop b !j)) = cc a b } variant { length a + length b - !i - !j } if a[!i] < b[!j] then incr i else if a[!i] > b[!j] then incr j else begin assert { inter (drop a !i) (drop b !j) == add a[!i] (inter (drop a (!i+1)) (drop b (!j+1))) }; assert { not (mem a[!i] (drop a (!i+1))) }; incr i; incr j; incr c end done; !c end

download ZIP archive

# Why3 Proof Results for Project "coincidence_count"

## Theory "coincidence_count.CoincidenceCount": fully verified in 8.67 s

Obligations | Alt-Ergo (0.95.2) | Alt-Ergo (0.99.1) | Z3 (4.3.1) | ||

drop_left | --- | 0.15 | --- | ||

not_mem_inter_r | 1.02 | --- | --- | ||

not_mem_inter_l | 1.01 | --- | --- | ||

VC for coincidence_count | --- | --- | --- | ||

split_goal_wp | |||||

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

2. loop invariant init | 0.02 | --- | --- | ||

3. loop invariant init | 0.01 | --- | --- | ||

4. index in array bounds | 0.01 | --- | --- | ||

5. index in array bounds | 0.02 | --- | --- | ||

6. loop invariant preservation | 0.01 | --- | --- | ||

7. loop invariant preservation | 0.02 | --- | --- | ||

8. loop invariant preservation | 1.19 | --- | --- | ||

9. loop variant decrease | 0.01 | --- | --- | ||

10. index in array bounds | 0.01 | --- | --- | ||

11. index in array bounds | 0.02 | --- | --- | ||

12. loop invariant preservation | 0.02 | --- | --- | ||

13. loop invariant preservation | 0.01 | --- | --- | ||

14. loop invariant preservation | 1.29 | --- | --- | ||

15. loop variant decrease | 0.02 | --- | --- | ||

16. assertion | --- | --- | 2.23 | ||

17. assertion | --- | --- | --- | ||

inline_goal | |||||

1. assertion | 0.69 | --- | --- | ||

18. loop invariant preservation | 0.01 | --- | --- | ||

19. loop invariant preservation | 0.02 | --- | --- | ||

20. loop invariant preservation | 0.70 | --- | --- | ||

21. loop variant decrease | 0.01 | --- | --- | ||

22. postcondition | 0.08 | --- | --- | ||

23. postcondition | 0.08 | --- | --- |