Commit 12ade68a authored by MARCHE Claude's avatar MARCHE Claude

Fix bad why3documentation

parent 84791d05
(** Given an array a of size n, removes its duplicate elements,
in-place, as follows: return r such that a[0..r[ contains the same
elements as a[0..n[ and no duplicate *)
(** {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[ *)
(** 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[ contains no duplicate element *)
(** [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
(** Quadratic implementation, without extra space *)
(** {2 Quadratic implementation, without extra space} *)
module RemoveDuplicateQuadratic
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment