coincidence_count.mlw 2.12 KB
Newer Older
1 2 3 4 5 6 7 8 9

(** 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).
10 11 12

    Authors: Jean-Christophe Filliâtre (CNRS)
             Andrei Paskevich (Université Paris Sud)
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
*)

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 }
59
      if a[!i] < b[!j] then
60
        incr i
61
      else if a[!i] > b[!j] then
62
        incr j
63
      else begin
64 65 66 67 68 69 70 71 72 73 74
        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