Wiki Agenda Contact Version française

Removing duplicate elements in an array, using a mutable set


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

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



Removing duplicate elements in an array, using a mutable set

Given an array a of size n, returns a fresh array containing the elements of a without duplicates, using a mutable set (typically a hash table).


Specification

module Spec

  use export int.Int
  use export array.Array

v appears in a[0..s-1]

  predicate appears (v: 'a) (a: array 'a) (s: int) =
    exists i: int. 0 <= i < s /\ a[i] = v

a[0..s-1] contains no duplicate element

  predicate nodup (a: array 'a) (s: int) =
    forall i: int. 0 <= i < s -> not (appears a[i] a i)

end

module MutableSet

  use import set.Fset

  type elt

  type t = private { ghost mutable s: set elt }

  val create () : t
    ensures { is_empty result.s }

  val add (t: t) (x: elt) : unit
    writes  { t.s }
    ensures { t.s = add x (old t.s) }

  val contains (t: t) (x: elt) : bool
    ensures { result <-> mem x t.s }

  val clear (t: t) : unit
    writes  { t.s }
    ensures { is_empty t.s }

  val size (t: t) : int
    ensures { result = cardinal t.s }

end

Quadratic implementation, without extra space

module RemoveDuplicate

  use import Spec
  use import set.Fset
  use import MutableSet
  use import ref.Refint
  use import array.Array

  let remove_duplicate (a: array elt) : array elt
    requires { 1 <= length a }
    ensures  { nodup result (length result) }
    ensures  { forall x: elt.
               appears x a (length a) <-> appears x result (length result) }
  =
    let s = MutableSet.create () in
    for i = 0 to Array.length a - 1 do
      invariant { forall x: elt. appears x a i <-> mem x s.s }
      MutableSet.add s a[i]
    done;
    'L:
    let r = Array.make (MutableSet.size s) a[0] in
    MutableSet.clear s;
    let j = ref 0 in
    for i = 0 to Array.length a - 1 do
      invariant { forall x: elt. appears x a i <-> mem x s.s }
      invariant { forall x: elt. mem x s.s <-> appears x r !j }
      invariant { nodup r !j }
      invariant { 0 <= !j = cardinal s.s <= length r }
      invariant { subset s.s (at s.s 'L) }
      if not (MutableSet.contains s a[i]) then begin
        MutableSet.add s a[i];
        r[!j] <- a[i];
        incr j
      end
    done;
    r

end

download ZIP archive

Why3 Proof Results for Project "remove_duplicate_hash"

Theory "remove_duplicate_hash.RemoveDuplicate": fully verified in 1.18 s

ObligationsAlt-Ergo (0.99.1)
VC for remove_duplicate---
split_goal_wp
  1. index in array bounds0.02
2. array creation size0.01
3. postcondition0.02
4. postcondition0.02
5. loop invariant init0.02
6. loop invariant init0.01
7. loop invariant init0.00
8. loop invariant init0.02
9. loop invariant init0.01
10. index in array bounds0.00
11. index in array bounds0.01
12. index in array bounds0.01
13. type invariant0.01
14. index in array bounds0.01
15. loop invariant preservation0.03
16. loop invariant preservation0.06
17. loop invariant preservation0.01
18. loop invariant preservation0.02
19. loop invariant preservation0.01
20. loop invariant preservation0.00
21. loop invariant preservation0.01
22. loop invariant preservation0.01
23. loop invariant preservation0.01
24. loop invariant preservation0.00
25. type invariant0.01
26. postcondition0.01
27. postcondition0.02
28. loop invariant init0.01
29. index in array bounds0.01
30. loop invariant preservation0.02
31. index in array bounds0.01
32. array creation size0.01
33. postcondition0.02
34. postcondition0.01
35. loop invariant init0.02
36. loop invariant init0.02
37. loop invariant init0.01
38. loop invariant init0.02
39. loop invariant init0.02
40. index in array bounds0.02
41. index in array bounds0.00
42. index in array bounds0.01
43. type invariant0.01
44. index in array bounds---
split_goal_wp
  1. VC for remove_duplicate0.00
2. VC for remove_duplicate0.04
45. loop invariant preservation0.01
46. loop invariant preservation0.17
47. loop invariant preservation0.21
48. loop invariant preservation0.01
49. loop invariant preservation0.02
50. loop invariant preservation0.02
51. loop invariant preservation0.02
52. loop invariant preservation0.01
53. loop invariant preservation0.02
54. loop invariant preservation0.02
55. type invariant0.01
56. postcondition0.01
57. postcondition0.02