Removing duplicate elements in an array, using a mutable set
Auteurs: Jean-Christophe Filliâtre
Catégories: Array Data Structure
Outils: 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 predicate appears (v: 'a) (a: array 'a) (s: int) = exists i: int. 0 <= i < s /\ a[i] = v
v
appears in a[0..s-1]
predicate nodup (a: array 'a) (s: int) = forall i: int. 0 <= i < s -> not (appears a[i] a i)
a[0..s-1]
contains no duplicate element
end
Quadratic implementation, without extra space
module RemoveDuplicate use Spec use ref.Refint use array.Array type elt clone import set.SetImp as MutableSet with type elt = elt 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.empty () in for i = 0 to Array.length a - 1 do invariant { forall x: elt. appears x a i <-> mem x s } MutableSet.add a[i] s done; label L in let r = Array.make (MutableSet.cardinal 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 } invariant { forall x: elt. mem x s <-> appears x r !j } invariant { nodup r !j } invariant { 0 <= !j = cardinal s <= length r } invariant { subset s (s at L) } if not (MutableSet.mem a[i] s) then begin MutableSet.add a[i] s; 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
Obligations | Alt-Ergo 2.2.0 | CVC4 1.6 | Eprover 1.8-001 | |
VC for remove_duplicate | --- | --- | --- | |
split_vc | ||||
loop invariant init | --- | 0.04 | --- | |
index in array bounds | --- | 0.02 | --- | |
loop invariant preservation | 0.03 | --- | --- | |
index in array bounds | --- | 0.02 | --- | |
array creation size | --- | 0.04 | --- | |
loop invariant init | --- | 0.04 | --- | |
loop invariant init | --- | 0.05 | --- | |
loop invariant init | --- | 0.04 | --- | |
loop invariant init | --- | 0.04 | --- | |
loop invariant init | --- | 0.04 | --- | |
index in array bounds | --- | 0.04 | --- | |
index in array bounds | --- | 0.02 | --- | |
index in array bounds | --- | 0.02 | --- | |
index in array bounds | 0.02 | --- | --- | |
loop invariant preservation | 0.04 | --- | --- | |
loop invariant preservation | 0.12 | --- | --- | |
loop invariant preservation | 0.12 | --- | --- | |
loop invariant preservation | 0.02 | --- | --- | |
loop invariant preservation | --- | 0.29 | --- | |
loop invariant preservation | --- | 0.41 | --- | |
loop invariant preservation | --- | 0.04 | --- | |
loop invariant preservation | --- | 0.02 | --- | |
loop invariant preservation | --- | 0.02 | --- | |
loop invariant preservation | --- | 0.02 | --- | |
postcondition | --- | --- | 0.90 | |
postcondition | --- | --- | 5.16 | |
out of loop bounds | --- | 0.02 | --- | |
out of loop bounds | --- | 0.05 | --- |