Wiki Agenda Contact Version française

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


download ZIP archive

Why3 Proof Results for Project "coincidence_count"

Theory "coincidence_count.CoincidenceCount": fully verified in 2.18 s

ObligationsAlt-Ergo (0.95.2)Alt-Ergo (0.99.1)Z3 (4.3.1)
4. VC for coincidence_count---------
  1. loop invariant init0.01------
2. loop invariant init0.02------
3. loop invariant init0.01------
4. index in array bounds0.01------
5. index in array bounds0.02------
6. loop invariant preservation0.01------
7. loop invariant preservation0.02------
8. loop invariant preservation1.19------
9. loop variant decrease0.01------
10. index in array bounds0.01------
11. index in array bounds0.02------
12. loop invariant preservation0.02------
13. loop invariant preservation0.01------
14. loop invariant preservation1.29------
15. loop variant decrease0.02------
16. assertion------2.19
17. assertion---------
  1. assertion0.69------
18. loop invariant preservation0.01------
19. loop invariant preservation0.02------
20. loop invariant preservation0.70------
21. loop variant decrease0.01------
22. postcondition0.08------
23. postcondition0.08------