Основы программирования на C#


Быстрая сортировка Хоара - часть 2


Вот чистый текст рекурсивной процедуры быстрой сортировки Хоара:

void QSort(int start, int finish) { if(start != finish) { int ind = rnd.Next(start,finish); int item = tower1[ind]; int ind1 = start, ind2 = finish; int temp; while (ind1 <=ind2) { while((ind1 <=ind2)&& (tower1[ind1] < item)) ind1++; while ((ind1 <=ind2)&&(tower1[ind2] >= item)) ind2--; if (ind1 < ind2) { temp = tower1[ind1]; tower1[ind1] = tower1[ind2]; tower1[ind2] = temp; ind1++; ind2--; } } if (ind1 == start) { temp = tower1[start]; tower1[start] = item; tower1[ind] = temp; QSort(start+1,finish); } else { QSort(start,ind1-1); QSort(ind2+1, finish); } } }// QuickSort

Проведите эксперимент - закройте книгу и попробуйте написать эту процедуру самостоятельно. Если вам удастся сделать это без ошибок и она пройдет у вас с первого раза, то вы - блестящий программист и вам нужно читать другие книги. Я полагаю, что в таких процедурах ошибки неизбежны и для их исправления требуется серьезная отладка. Полагаю также, что помимо обычного тестирования полезно применять обоснование корректности, основанное на предусловиях и постусловиях, инвариантах цикла. Проектируя эту процедуру, я параллельно встраивал обоснование ее корректности. Это не строгое доказательство, но, дополняя тестирование, оно достаточно, чтобы автор поверил в корректность процедуры и представил ее на суд зрителей, как это сделал я.

/// <summary> /// Небольшая по размеру процедура содержит три /// вложенных цикла while, два оператора if и рекурсивные /// вызовы. Для таких процедур задание инвариантов и /// обоснование корректности облегчает отладку. /// </summary> /// <param name="start">начальный индекс сортируемой части /// массива 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} /// Введем следующие логические условия, /// играющие роль инвариантов циклов нашей программы: /// P1: объединение S1, S2, S3 = tower1 /// P2: (S1(i) < item) Для всех элементов S1 /// P3: (S3(i) >= item) Для всех элементов S3 /// P4: item - случайно выбранный элемент tower1 /// Нетрудно видеть, что все условия становятся /// истинными после завершения инициализатора цикла. /// Для пустых множеств S1 и S3 условия P2 и P3 /// считаются истинными по определению. /// Inv = P1 & P2 & P3 & P4 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 & B3 следует истинность: //((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]; tower1[start] = item; tower1[ind] = temp; QSort(start+1,finish); } else // Здесь оба множества S1 и S3 не пусты. // К ним применим рекурсивный вызов. { QSort(start,ind1-1); QSort(ind2+1, finish); } //Индукция по размеру массива и истинность инварианта //доказывает истинность постусловия в общем случае. } }// QuickSort




Начало  Назад  Вперед