Пример. Сортировка простыми вставками

Рассмотрим задачу сортировки простыми вставками [6]. На ее примере демонстрируются типовые методы построения предикатных программ, доказательства их корректности и получения эффективных программ. Представлен нетривиальный способ кодирования списков.

В алгоритме [6] сортируемый список s рассматривается в виде конкатенации u + b + v, где u и v - списки, а b - элемент, причем список u - сортированный.
На очередном шаге работы алгоритма элемент b вставляется внутрь списка u таким образом, чтобы сохранить сортированность обновленного списка u. На следующем шаге в качестве элемента b рассматривается начальный элемент v, и процесс повторяется.

Элементы списка имеют произвольный тип T с линейным порядком “£”. Типы элементов и списков представлены описаниями:

type T{ £: axiom "a. a £ a, axiom "a, b. a £ b & b £ a Þ a = b,

axiom "a, b, c. a £ b & b £ c Þ a <= c, axiom "a, b. a £ b Ú b £ a };

type S = list (T);

Свойство сортированности списка s определяется предикатом:

SORT(s) @ "s1, s2 Î S. "a, b Î T. (s = s1 + a + b + s2 Þ a £ b)

Лемма 7.1. Список не более, чем из одного элемента - сортированный, т. е. SORT(nil) & "a. SORT([[a]]).

Лемма 7.2. length(s) ≤ 1 Û s = nil Ú $a. s = [[a]].

Лемма 7.3. length(s) ≤ 1 Þ SORT(s).

Допустим, список v является результатом сортировки исходного списка u. Списки u и v состоят из одной и той же совокупности элементов. Тогда список v можно получить из u применением серии перестановок элементов. Обозначим это свойство через PERM(u, v). Элементарную перестановку можно определить предикатом:

perm(u, v) @ $s1,s2,s3ÎS. $a,bÎT. u = s1 + a + s2+ b + s3 & v = s1 + b + s2+ a + s3

Тогда свойство перестановочности PERM(u, v) можно определить следующим образом:

PERM(u, v) @ u = v Ú $ w. perm(u, w) & PERM(w, v).

Приведенное рекурсивное определение эквивалентно следующему нерекурсивному:

PERM(u, v) º $n³1. $w₁…w_n Î S. u = w₁ & v = w_n & "i=1..n-1. perm(w_i, w_i+1).

Лемма 7.4. length(u) ≤ 1 & PERM(u, v) Þ u = v.

Доказательство. Пусть истинны length(u) ≤ 1 и PERM(u, v). Предикат perm(u, w) - ложный для любого списка w, поскольку в определении предиката u должна содержать не менее двух элементов. Поэтому ложна вторая альтернатива предиката PERM(u, v), а значит, истинна первая, т. е. u = v. □

Спецификацию задачи сортировки представим определением:

sort(S s: S s’) post SORT(s’) & PERM(s, s’);

Напомним, что штрих в имени s’ предполагает склеивание переменных s и s’ в реализации, см. разд. 6.3.

Сначала задачу sort следует свести к более общей задаче sort1, в которой s = u + b + v, где u и v - списки, а b - элемент, причем список u - сортированный. Спецификация задачи sort1 следующая:

sort1(S u, T b, S v: S r) pre u ≠ nil & SORT(u) post SORT(r) & PERM(u + b + v, r);

Лемма 7.5. Спецификация sort1 реализуема и однозначна, т. е. существует единственный список r, удовлетворяющий постусловию.

Возможность сведения задачи sort к sort1 обеспечивается следующей леммой.

Лемма 7.6. length(s) > 1 Þ s = s.car + s.cdr.car + s.cdr.cdr.

Дадим определение предиката sort и докажем его корректность.

sort(S s: S s’)

{ if (length(s) ≤ 1) s' = s

else sort1(s.car, s.cdr.car, s.cdr.cdr: s')

} post SORT(s’) & PERM(s, s’);

Доказательство корректности. Поскольку спецификация реализуема, а тело предиката sort - однозначный оператор, то в соответствии с теоремой 2.1 тождества спецификации и программы достаточно доказать истинность тела предиката из постусловия. Пусть SORT(s’) и PERM(s, s’) истинны. Пусть истинно условие length(s) ≤ 1. Истинность оператора s' = s следует из леммы 7.4. Пусть истинно условие length(s) > 1. Докажем истинность вызова sort1. Прежде всего, истинны условия корректности для полей car и cdr, поскольку s и s.cdr отличны от nil. Далее, истинно предусловие для аргументов вызова sort1, т. е. истинны SORT(s.car) (по лемме 7.3) и s.car ¹ nil. По лемме 2.8. предикат sort1 тождественен постусловию. Поэтому достаточно доказать истинность формулы:

SORT(s’) & PERM(s.car + s.cdr.car + s.cdr.cdr, s’).

Ее истинность следует из леммы 7.6 и предусловия sort. □

Задача sort1 содержит независимую подзадачу pop_into вставки элемента b внутрь отсортированного списка u:

pop_into(S u, T b: S w) pre u ≠ nil & SORT(u) post SORT(w) & PERM(u + b, w);

Лемма 7.7. Спецификация pop_into реализуема и однозначна.

Дадим определение предиката sort1 и докажем его корректность.

sort1(S u, T b, S v: S r) pre u ≠ nil & SORT(u)

{ pop_into(u, b: S w);

if (v = nil) r = w

else sort1(w, v.car, v.cdr: r)

} post SORT(r) & PERM(u + b + v, r);

Доказательство. Доказательство истинности тела предиката из предусловия и постусловия сводится к доказательству истинности условного оператора. Предусловие оператора pop_into(u, b: S w) истинно. Поэтому оператор полагается истинным при доказательстве истинности условного оператора. Мы можем заменить его постусловием SORT(w) & PERM(u + b, w). Переменная v является индуктивной. Используется отношение порядка: v ⊑ t @ $q. q + v = t. Тогда истинно v.cdr ⊏ v. Минимальный элемент nil покрывается условием v = nil в условном операторе. Пусть истинно условие v = nil. Тогда из истинности PERM(u + b, r) и PERM(u + b, w) следует истинность оператора r = w. Ввиду истинности предусловия операций v.car и v.cdr, истинности предусловия рекурсивного вызова sort1 и истинности v.cdr ⊏ v в соответствии с индуктивным предположением можно заменить вызов sort1 постусловием SORT(r) & PERM(w + v, r). Истинность PERM(w + v, r) следует из истинности PERM(u + b, w) и PERM(u + b + v, r). □

Задачу pop_into необходимо свести к более общей задаче pop_into1, в которой u = y + a + z, где текущий элемент a разделяет списки y и z; при этом все элементы из z больше, чем b. Спецификация задачи pop_into1 следующая:

pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z ≠ nil Þ b ≤ z.car)

post SORT(w) & PERM(y + a + b + z, w);

Лемма 7.8. Спецификация pop_into1 реализуема и однозначна.

Дадим определение предиката pop_into и докажем его корректность.

pop_into(S u, T b: S w) pre u ≠ nil & SORT(u)

{ pop_into1(prec(u), nil, last(u), b: w)

} post SORT(w) & PERM(u + b, w);

Доказательство. Нетрудно проверить истинность предусловия вызова pop_into1. Заменим вызов pop_into1 его постусловием SORT(w) & PERM(u + b, w) и обнаружим, что оно совпадает с постусловием pop_into, что доказывает его истинность. □

Определение pop_into1 реализуется разбором случаев. Докажем его корректность.

pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z ≠ nil Þ b ≤ z.car)

{ if (a ≤ b) w = y + a + b + z

else if (y = nil ) w = b + a + z

else pop_into1(prec(y), a + z, last(y), b: w)

} post SORT(w) & PERM(y + a + b + z, w);

Доказательство. Из предусловия и постусловия докажем истинность объемлющего условного оператора. Пусть истинно условие a ≤ b. Тогда список y + a + b + z является сортированным. Истинность оператора w = y + a + b + z следует из леммы 7.9.

Лемма 7.9. PERM(v, w) & SORT(v) & SORT(w) Þ v =w.

Пусть истинно a > b. Доказательство истинности внутреннего условного оператора проводится индукцией по переменной y. Отношение порядка несколько иное по сравнению с используемым в предикате sort1: y ⊑ t @ $q. y + q = t. Минимальный элемент nil покрывается условием y = nil в условном операторе. Пусть истинно y = nil. Тогда список b + a + z является сортированным и по лемме 7.9 истинен оператор w = b + a + z. Ввиду истинности предусловия операций prec(y) и last(y), истинности предусловия рекурсивного вызова pop_into1 и истинности prec(y) ⊏ y в соответствии с индуктивным предположением можно заменить вызов pop_into1 его постусловием SORT(w) & PERM(y + b + a + z, w). Истинность PERM(y + b + a + z, w) следует из истинности PERM(y + b + a + z, y + a + b + z). □

Применим к предикатной программе сортировки, составленной из определений предикатов sort, sort1, pop_into и pop_into1, систему трансформаций для получения эффективной императивной программы. На первом этапе реализуются склеивания переменных. Ниже приводится результат склеивания для первых трех предикатов; в pop_into1 склеиваний не производится. Перед определением предиката перечисляется список применяемых склеиваний. Отметим, что замена s r не является склеиванием - она делается для облегчения проведения дальнейшей подстановки определения.

s s’

sort(S s: S s)

{ if (length(s) ≤ 1) s = s

else sort1(s.car, s.cdr.car, s.cdr.cdr: s)

}

s r; u w;

sort1(S u, T b, S v: S s)

{ pop_into(u, b: S u);

if (v = nil) s = u

else sort1(u, v.car, v.cdr: s)

}

u w;

pop_into(S u, T b: S u)

{ pop_into1(prec(u), nil, last(u), b: u) };

На втором этапе трансформаций заменим хвостовую рекурсию циклом в определениях sort1 и pop_into1. Раскроем групповые операторы присваивания и оформим циклы. При раскрытии группового оператора в pop_into1 возникает две коллизии, которые устраняются перестановками присваиваний.

sort1(S u, T b, S v: S s)

{ for (;;) {

pop_into(u, b: S u);

if (v = nil) {s = u; break }

else { b = v.car; v = v.cdr}

}

}

pop_into1(S y, z, T a, b: S u)

{ for (;;) {

if (a ≤ b) { u = y + a + b + z; break }

else if (y = nil ) { u = b + a + z; break }

else {z = a + z; a = last(y); y = prec(y)}

}

}

На третьем этапе подставим sort1 на место вызова в sort и pop_into1 в pop_into.

sort(S s: S s)

{ if (length(s) ≤ 1) return

S u =s.car; T b = s.cdr.car; S v = s.cdr.cdr;

for (;;) {

pop_into(u, b: S u);

if (v = nil) {s = u; break }

else { b = v.car; v = v.cdr}

}

}

pop_into(S u, T b: S u)

{ T a = last(u); S y = prec(u); S z = nil;

for (;;) {

if (a ≤ b) { u = y + a + b + z; break }

else if (y = nil ) { u = b + a + z; break }

else {z = a + z; a = last(y); y = prec(y)}

}

}

Далее, подставим определение pop_into на место вызова в sort.

sort(S s: S s)

{ if (length(s) ≤ 1) return;

S u = s.car; T b = s.cdr.car; S v = s.cdr.cdr;

for (;;) {

T a = last(u); S y = prec(u); S z = nil;

for (;;) {

if (a ≤ b) { u = y + a + b + z; break }

else if (y = nil ) { u = b + a + z; break }

else {z = a + z; a = last(y); y = prec(y)}

}

if (v = nil) {s = u; break }

else { b = v.car; v = v.cdr}

}

}

На четвертом этапе реализуется кодирование списков s, u, v, y и z вырезками одного массива. Особенность кодирования в том, что списки u и v находятся внутри s, а y и z - внутри u. Тип массива представим описанием:

type SEQ(int p, q) = array p..q of T;

Пусть список w кодируется вырезкой W[p..q]. Кодирование используемых в программе конструкций реализуется следующим образом:

S w ® SEQ(p, q)

w = nil → p > q

length(w) → q – p + 1

b = w.car; w:= w.cdr → b:= W[p]; p:= p + 1

a = last(w); w:= prec(w) → a:= W[q]; q:= q – 1

Пусть список s кодируется вырезкой K[0..n].

int n; // номер последнего элемента списка

SEQ(0, n) K;

Пусть s = u + b + v. Здесь u и v являются частью списка s и кодируются вырезками массива K. Пусть позиция элемента b в массиве K есть i. Тогда

u → K[0.. i - 1]; b → K[ i ]; v → K[i + 1.. n]. (7.11)

Отметим, что здесь один индекс i используется для представления двух соседних списков u и v. Особенность в том, что изменение индекса i определяет синхронное изменение этих списков. Аналогичным образом реализуется представление для u = y + a + b + z.
В представлении используется другой индекс j.

y → K[0..j - 2]; a → K[j - 1]; b → K[j]; z→ K[j + 1.. i].

Позиция элемента b здесь иная, нежели в представлении (7.11). Другая особенность: позиция последнего элемента z совпадает с позицией b в (7.11). Это значит, что весь список z сдвинут на один элемент по сравнению с тем положением, которое имеет z в составе u в (7.11).

Приведем программу, полученную в результате кодирования списков вырезками массива. В ней описание с инициализацией int i = 1 используется как эквивалент двух конструкций S u = s.car и S v = s.cdr.cdr, которым соответствуют вырезки K[0..0] и K[2..n]. Аналогичным образом конструкция int j = i используется вместо S y = prec(u) и S z = nil, отображающихся в вырезки K[0..i - 2] и K[i + 1.. i]. Кроме того, используется кодирование z = a + z → K[j] = a.

sort(S s: S s)

{ if (n ≤ 0) return;

int i = 1; T b = K[1];

for (;;) {

T a = K[i - 1]; int j = i;

for (;;) {

if (a ≤ b) { K[j] = b; break }

else if (j < 2 ) { K[0] = b; K[1] = a; break }

else {K[j] = a; a = K[j - 2]; j = j - 1 }

}

if (i >= n) break

else { b = K[i + 1]; i = i + 1 }

}

}

Наконец, приведем итоговую программу сортировки, отличающуюся от предыдущей деталями оформления циклов и упрощением условий.

type SEQ(int p, q) = array p..q of T;

int n; //номер последнего элемента списка

SEQ(0, n) K;

...

if (n ≤ 0) return;

T b = K[1];

for (int i = 1;;) {

T a = K[i - 1];

for (int j = i;; j = j – 1) {

if (a ≤ b) { K[j] = b; break }

else if (j = 1 ) { K[0] = b; K[1] = a; break }

else { K[j] = a; a = K[j - 2] }

}

if (i = n) break

else { i = i + 1; b = K[i] }

}

Приведенный пример построения программы сортировки простыми вставками в достаточной степени демонстрирует стиль и технологию предикатного программирования. Корректность предикатной программы строго доказывается применением системы правил, определенных в разд. 2 и 5. Эффективность и компактность итоговой программы не хуже написанной вручную. Отметим нетривиальность применяемого синхронного способа кодирования смежных списков с использованием общего индекса.

Можно отметить следующую неэффективность итоговой программы. Если после выполнения оператора b = K[i] обнаруживается, что a ≤ b для a = K[i - 1], то оператор K[j] = b является избыточным. Данный недостаток легко устраняется другим алгоритмом, представленным ниже. Отметим, что предикатное программирование обладает гораздо большей гибкостью в сравнении с императивным и позволяет эффективно реализовать любое проектное решение.

pop_into(S u, T b: S w) pre u ≠ nil & SORT(u)

{ T a = last(u);

if (a ≤ b) w = u + b

else pop_into2(prec(u), a, b: w)

} post SORT(w) & PERM(u + b, w);

pop_into2(S y, z, T b: S w) pre SORT(y + z) & z ≠ nil & b ≤ z.car

{ if (y = nil ) w = b + z

else T c = last(y);

if (c ≤ b) w = y + b + z

else pop_into2(prec(y), c + z, b: w)

} post SORT(w) & PERM(y + b + z, w);

Императивная программа, полученная по этой версии предикатной программы, более эффективна, однако несколько сложнее и длиннее. Данный алгоритм используется в работе [7], однако представлен для массивов, а не списков. Использование массивов вместо списков делает алгоритм существенно сложнее. Намного сложнее становится доказательство корректности, поскольку программа представляется логикой второго порядка.