/// <summary>
/// Небольшая по размеру процедура содержит три
/// вложенных цикла while, два оператора if и рекурсивные
/// вызовы. Для таких процедур задание инвариантов и
/// обоснование корректности облегчает отладку.
/// </summary>
/// <param name="start">нaчaльный индекс сортируемой части
/// массива tower</param>
/// <param name="finish">конечный индекс сортируемой части
/// массива tower</param>
/// Предусловие: (start <= finish)
/// Постусловие: массив tower отсортирован по возрастанию
void QSort (int start, int finish)
{
if (start!= finish)
//если (start = finish), то процедура ничего не делает,
//но постусловие выполняется, поскольку массив из одного
//элемента отсортирован по определению. Докажем истинность
//постусловия для массива с числом элементов >1.
{
int ind = rnd.Next(start,finish);
int item = tower1[ind];
int ind1 = start, ind2 = finish;
int temp;
/// Введем три непересекающихся множества:
/// S1: {tower1(i), start <= i =< ind1-1}
/// S2: {tower1(i), ind1 <= i =< ind2}
/// S3: {tower1(i), ind2+1 <= i =< finish}
/// Введем следующие логические условия,
/// играющие роль инвариантов циклов нашей программы:
/// Р1: объединение S1, S2, S3 = towerl
/// Р2: (S1 (i) < item) Для всех элементов S1
/// Р3: (S3 (i) >= item) Для всех элементов S3
/// Р4: item — случайно выбранный элемент tower1
/// Нетрудно видеть, что все условия становятся
/// истинными после завершения инициализатора цикла.
/// Для пустых множеств S1 и S3 условия Р2 и РЗ
/// считаются истинными по определению.
/// Inv = P1 & Р2 & РЗ & Р4
while (ind1 <=ind2)
{
while((ind1 <=ind2)&& (tower1[ind1] < item)) ind1++;
// (Inv == true) & ~B1 (B1 — условие цикла while)
while ((ind1 <=ind2)&& (tower1[ind2] >= item)) ind2-;
// (Inv == true) & ~B2 (B2 — условие цикла while)
if (ind1 < ind2)
// Из Inv & ~B1 & ~B2 & ВЗ следует истинность:
// ((tower1[ind1] >= item)&&(tower1[ind2]<item))==true.
// Это условие гарантирует, что последующий обмен
// элементов обеспечит выполнение инварианта Inv
{
temp = tower1[ind1]; tower1[ind1] = tower1[ind2];
tower1[ind2] = temp;
ind1++; ind2-;
}
//(Inv ==true)
}
// из условия окончания цикла следует: (S2 — пустое множество)
if (ind1 == start)
// В этой точке S1 и S2 — это пустые множества, — > //(S3 = tower1)
// Нетрудно доказать, что отсюда следует истинность:
// (item = min)
// Как следствие, можно минимальный элемент сделать первым,
// а к оставшемуся множеству применить рекурсивный вызов.
{
temp = tower1[start]; towerl[start] = item;
tower1[ind] = temp;
QSort(start+1,finish);
}
else
// Здесь оба множества S1 и S3 не пусты.
// К ним применим рекурсивный вызов.
{
QSort(start,ind1-1);
QSort(ind2+1, finish);
}
// Индукция по размеру массива и истинность инварианта
// доказывает истинность постусловия в общем случае.
}
}// Quicksort
Приведу некоторые пояснения к этому доказательству. Задание предусловия и постусловия процедуры QSort достаточно очевидно — сортируемый массив должен быть не пустым, а после работы метода должен быть отсортированным. Важной частью обоснования является четкое введение трех множеств — S1, S2, S3 — и условий, накладываемых на их элементы. Эти условия и становятся частью инварианта, сохраняющегося при работе различных циклов нашего метода. Вначале множества S1 и S3 пусты, в ходе вычислений пустым становится множество S2. Так происходит формирование подзадач, к которым рекурсивно применяется алгоритм. Особым представляется случай, когда множество S1 тоже пусто. Нетрудно показать, что эта ситуация возможна только в том случае, если случайно выбранный элемент множества, служащий критерием разбиения исходного множества на два подмножества, является минимальным элементом.