Интернет-журнал "Домашняя лаборатория", 2007 №9

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

/// <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 тоже пусто. Нетрудно показать, что эта ситуация возможна только в том случае, если случайно выбранный элемент множества, служащий критерием разбиения исходного множества на два подмножества, является минимальным элементом.

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

Рис. 10.3. Результаты быстрой сортировки массива

11. Массивы языка С#

_{Общий взгляд на массивы. Сравнение с массивами C++. Почему массивы C# лучше, чем массивы C++. Виды массивов — одномерные, многомерные и изрезанные. Динамические массивы.}

Общий взгляд

Массив задает способ организации данных. Массивом называют упорядоченную совокупность элементов одного типа. Каждый элемент массива имеет индексы, определяющие порядок элементов. Число индексов характеризует размерность массива. Каждый индекс изменяется в некотором диапазоне [а, Ь]. в языке С#, как и во многих других языках, индексы задаются целочисленным типом. В других языках, например, в языке Паскаль, индексы могут принадлежать счетному конечному множеству, на котором определены функции, задающие следующий и предыдущий элемент. Диапазон [а, Ь] называется граничной парой, а — нижней границей, b — верхней границей индекса. При объявлении массива границы задаются выражениями. Если все границы заданы константными выражениями, то число элементов массива известно в момент его объявления и ему может быть выделена память еще на этапе трансляции. Такие массивы называются статическими. Если же выражения, задающие границы, зависят от переменных, то такие массивы называются динамическими, поскольку память им может быть отведена только динамически в процессе выполнения программы, когда становятся известными значения соответствующих переменных. Массиву, как правило, выделяется непрерывная область памяти.

В языке C++ все массивы являются статическими; более того, все массивы являются 0-базируемыми. Это означает, что нижняя граница всех индексов массива фиксирована и равна нулю. Введение такого ограничения имеет свою логику, поскольку здесь широко используется адресная арифметика. Так, несколько странное выражение mas + i, где mas — это имя массива, a i — индексное выражение, имеет вполне определенный смысл для C++ программистов. Имя массива интерпретируется как адрес первого элемента массива, к этому адресу прибавляется число, равное произведению i на размер памяти, необходимой для одного элемента массива. В результате сложения в такой адресной арифметике эффективно вычисляется адрес элемента mas [i].