cleaned-up qsort, do not compare equal objects for GCC

This commit is contained in:
Jan (janneke) Nieuwenhuizen 2022-10-25 11:02:10 +02:00
parent 386341092e
commit ac1800c08d
No known key found for this signature in database
GPG Key ID: F3C1A0D9C1D65273
1 changed files with 25 additions and 95 deletions

View File

@ -1,6 +1,7 @@
/* -*-comment-start: "//";comment-end:""-*-
* GNU Mes --- Maxwell Equations of Software
* Copyright © 2017,2018 Jan (janneke) Nieuwenhuizen <janneke@gnu.org>
* Copyright © 2021 Paul Dersey <pdersey@gmail.com>
*
* This file is part of GNU Mes.
*
@ -45,112 +46,41 @@ qswap (void *a, void *b, int size)
}
#endif
/**
* Assuming precondition (P) that `end - begin >= 2`, this function reorders the elements
* of range [begin, end) and returns a pointer `ret` such that the following
* postconditions hold:
* - (Q1): `ret > begin`
* - (Q2): `ret < end`
* and, for some value `p` in [begin, end):
* - (Q3): all values in [begin, ret) are lower than or equal to `p`
* - (Q4): all values in [ret, end) are greater than or equal to `p`
*/
char *
qpart (char *low, char *high, size_t size,
size_t
qpart (char *base, size_t count, size_t size,
int (*compare) (void const *, void const *))
{
char *pivot = (low + (high - low)/2);
// Loop invariants, all trivially verified at the start of the loop:
// - (A): values strictly to the left of `low` are lower than or equal to `pivot`
// - (B): there is at least one value at or to the right of `low` that is greater
// than or equal to `pivot`
// - (C): values at or to the right of `high` are greater than or equal to `pivot`
// - (D): there is at least one value strictly to the left of `high` that is lower
// than or equal to `pivot`
// - (E): `low <= high`
//
// The loop terminates because `high - low` decreases strictly at each execution of
// the body (obvious).
while (1)
void *p1 = base + count * size;
size_t i = 0;
for (size_t j = 0; j < count; j++)
{
// This loop terminates because of (B).
int c = compare (low, pivot);
while (c < 0)
low += size;
// Here, we have
// - (1): `*low >= pivot`
// - (2): `low <= high` because of (E) and (C)
// - properties (A) and (B) still hold because `low` has only moved
// past values strictly less than `pivot`
// This loop terminates because of (D).
do {
--high;
int c = compare (pivot, high);
} while (c < 0);
// Here, we have
// - (3): `*high <= pivot`
// - (4): by (C) which held before this loop, elements strictly to the
// right of `high` are known to be greater than or equal to `pivot`
// (but now (C) may not hold anymore)
if (low >= high)
char *p2 = base + j * size;
if (p1 == p2)
i++;
else if (compare (p2, p1) < 0)
{
// Due to (1), (A) and (4), (Q3) and (Q4) are established with `pivot`
// as `p`.
// Clearly, (B) proves Q2.
// See the rest of the answer below for a proof of (Q1).
// This correctly finishes the qpart.
return low;
char *p1 = base + i * size;
qswap (p1, p2, size);
i++;
}
// We have `low < high` and we swap...
qswap (low, high, size);
// ...and now,
// - by (1) and (4), invariant (C) is re-established
// - by (1), invariant (D) is re-established
// - (5): by (3), `*low <= pivot`
++low;
// (A) already held before this increment. Thus, because of (5), (A)
// still holds. Additionally, by (1), after the swap, (B) is
// re-established. Finally, (E) is obvious.
}
}
void
_qsort (char *low, char *high, size_t size,
int (*compare) (void const *, void const *))
{
// Trivial base case...
if (low - high < size)
return;
// ...therefore pre-condition (P) of `qpart` is satisfied.
char *p = qpart (low, high, size, compare);
// Thanks to postconditions (Q1) and (Q2) of `qpart`, the ranges
// [low, p) and [p, high) are non-empty, therefore the size of the ranges
// passed to the recursive calls below is strictly lower than the size of
// [low, high) in this call. Therefore the base case is eventually reached
// and the algorithm terminates.
// Thanks to postconditions (Q3) and (Q4) of `qpart`, and by induction
// on the size of [low, high), the recursive calls below sort their
// respective argument ranges and [low, high) is sorted as a result.
_qsort (low, p, size, compare);
_qsort (p, high, size, compare);
char *p2 = base + i * size;
if (p1 != p2 && compare (p1, p2) < 0)
qswap (p1, p2, size);
return i;
}
void
qsort (void *base, size_t count, size_t size,
int (*compare) (void const *, void const *))
{
char *high = base + count * size;
_qsort (base, high, size, compare);
if (count <= 1)
return;
size_t p = qpart (base, count - 1, size, compare);
qsort (base, p, size, compare);
char *pbase = base;
char *p1 = pbase + p * size;
size_t c1 = count - p;
qsort (p1, c1, size, compare);
}