mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
69 lines
1.7 KiB
Plaintext
69 lines
1.7 KiB
Plaintext
|
|
|
|
(** {1 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).
|
|
|
|
*)
|
|
|
|
(** {2 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
|
|
|
|
(** {2 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
|