1
2
3
4
5
6
7
8
9
10
11
12
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
(** {1 Removing duplicate elements in an array}
Given an array `a` of size `n`, removes its duplicate elements,
in-place, as follows: return `r` such that `a[0..r-1]` contains the same
elements as `a[0..n-1]` and no duplicate
*)
(** {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 RemoveDuplicateQuadratic
use Spec
use ref.Refint
type t
val predicate eq (x y: t)
ensures { result <-> x = y }
let rec test_appears (ghost w: ref int) (v: t) (a: array t) (s: int) : bool
requires { 0 <= s <= length a }
ensures { result <-> appears v a s }
ensures { result -> 0 <= !w < s && a[!w] = v }
variant { s }
= s > 0 &&
if eq a[s-1] v then begin w := s - 1; true end else test_appears w v a (s-1)
let remove_duplicate (a: array t): int
ensures { 0 <= result <= length a }
ensures { nodup a result }
ensures { forall v. appears v (old a) (length a) <-> appears v a result }
= let n = length a in
let r = ref 0 in
let ghost from = make n 0 in
let ghost to_ = make n 0 in
for i = 0 to n - 1 do
invariant { 0 <= !r <= i }
invariant { nodup a !r }
invariant { forall j: int. 0 <= j < !r ->
0 <= to_[j] < i /\ a[j] = (old a)[to_[j]] }
invariant { forall j: int. 0 <= j < i ->
0 <= from[j] < !r /\ (old a)[j] = a[from[j]] }
invariant { forall j: int. i <= j < n -> a[j] = (old a)[j] }
let ghost w = ref 0 in
if not (test_appears w a[i] a !r) then begin
a[!r] <- a[i];
from[i] <- !r;
to_[!r] <- i;
incr r
end else begin
from[i] <- !w;
()
end
done;
!r
end
|
