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

Содержательно это означает, что предикат ReaIInv становится истинным после выполнения инициализирующей части. Далее доказывается, что RealInv является инвариантом цикла:

(**) {Reallnv(x, z)& В} S(х, z){ReaLInv(х, z)}

На последнем шаге доказывается, что наш инвариант обеспечивает решение задачи после завершения цикла:

(***) ~B RealInv(x, z) — > Post(x,z)

Это означает, что из истинности инварианта и условия завершения цикла следует требуемое постусловие.

Определение 4 (подходящего инварианта): предикат ReaIInv, удовлетворяющий условиям (*), (**), (***) называется подходящим инвариантом цикла.

С циклом связано еще одно важное понятие — варианта цикла, используемое для доказательства завершаемости цикла.

Определение 5 (варианта цикла): целочисленное неотрицательное выражение Var (х, z) называется вариантом цикла, если выполняется следующая триада:

{(Var(x,z)= n) & В} S (х, z) { (Var(х, z)= m) & (m < n) }

Содержательно это означает, что каждое выполнение тела цикла приводит к уменьшению значения его варианта. После конечного числа шагов вариант достигает своей нижней границы, и цикл завершается. Простейшим примером варианта цикла является выражение n-i для цикла:

for(i=1; i<=n; i++) S(x, z);

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

Рекурсия

Рекурсия является одним из наиболее мощных средств в арсенале программиста. Рекурсивные структуры данных и рекурсивные методы широко используются при построении программных систем. Рекурсивные методы, как правило, наиболее всего удобны при работе с рекурсивными структурами данных — списками, деревьями. Рекурсивные методы обхода деревьев служат классическим примером.

Определение 6 (рекурсивного метода): метод P (процедура или функция) называется рекурсивным, если при выполнении тела метода происходит вызов метода P.

Рекурсия может быть прямой, если вызов P происходит непосредственно в теле метода P. Рекурсия может быть косвенной, если в теле P вызывается метод Q (эта цепочка может быть продолжена), в теле которого вызывается метод P. Определения методов P и Q взаимно рекурсивны, если в теле метода Q вызывается метод P, вызывающий, в свою очередь, метод Q.

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

public long factorial (int n)

{

   if (n<=1) return(1);

   else return(n*factorial(n-1));

}//factorial

Функция factorial является примером прямого рекурсивного определения — в ее теле она сама себя вызывает. Здесь, как и положено, есть нерекурсивная ветвь, завершающая вычисления, когда n становится равным единице. Это пример так называемой "хвостовой" рекурсии, когда в теле встречается ровно один рекурсивный вызов, стоящий в конце соответствующего выражения. Хвостовую рекурсию намного проще записать в виде обычного цикла. Вот циклическое определение той же функции:

public long fact(int n)

{

   long res =1;

   for (int i = 2; i <=n; i + +) res* = i;

   return(res);

}//factorial

Конечно, циклическое определение проще, понятнее и эффективнее, и применять рекурсию в подобных ситуациях не следует. Интересно сравнить время вычислений, дающее некоторое представление о том, насколько эффективно реализуется рекурсия. Вот соответствующий тест, решающий эту задачу:

public void TestTailRec()

{

    Hanoi han = new Hanoi (5);

    long time1, time2;

    long f=0;

    time1 = getTimeInMilliseconds();

    for (int i = 1; i <1000000; i + +)f =han.fact(15);

    time2 =getTimeInMilliseconds ();

    Console.WriteLine(" f= {0}, " + "Время работы циклической процедуры: 

            {1}",f,time2 — time1);

    time1 = getTimeInMilliseconds ();

    for(int i = 1; i <1000000; i + +)f =han.factorial (15);

    time2 =getTimeInMilliseconds ();

    Console.WriteLine(" f= {0}, " + "Время работы  рекурсивной процедуры:

            1}",f,time2 — time1);

Каждая из функций вызывается в цикле, работающем 1000000 раз. До начала цикла и после его окончания вычисляется текущее время. Разность этих времен и дает оценку времени работы функций. Обе функции вычисляют факториал числа 15.

Проводить сравнение эффективности работы различных вариантов — это частый прием, используемый при разработке программ. И я им буду пользоваться неоднократно. Встроенный тип DateTime обеспечивает необходимую поддержку для получения текущего времени. Он совершенно необходим, когда приходится работать с датами. Я не буду подробно описывать его многочисленные статические и динамические методы и свойства. Ограничусь лишь приведением функции, которую я написал для получения текущего времени, измеряемого в миллисекундах. Статический метод Now класса DateTime возвращает объект этого класса, соответствующий дате и времени в момент создания объекта. Многочисленные свойства этого объекта позволяют извлечь требуемые характеристики. Приведу текст функции getTimeInMilliseconds:

long getTimeInMilliseconds ()

{

    DateTime time = DateTime.Now;

    return(((time.Hour*60 + time.Minute)*60 + time.Second)*1000

        + time.Millisecond);

}

Результаты измерений времени работы рекурсивного и циклического вариантов функций слегка отличаются от запуска к запуску, но порядок остается одним и тем же. Эти результаты показаны на рис. 10.1.

Рис. 10.1. Сравнение времени работы циклической и рекурсивной функций

Вовсе не обязательно, что рекурсивные методы будут работать медленнее нерекурсивных.

Классическим примером являются методы сортировки. Известно, что время работы нерекурсивной пузырьковой сортировки имеет порядок с*n2, где с — некоторая константа. Для рекурсивной процедуры сортировки слиянием время работы — q*n*log(n), где q — константа. Понятно, что для больших n сортировка слиянием работает быстрее, независимо от соотношения значений констант. Сортировка слиянием — хороший пример применения рекурсивных методов. Она демонстрирует известный прием, называемый "разделяй и властвуй". Его суть в том, что исходная задача разбивается на подзадачи меньшей размерности, допускающие решение тем же алгоритмом. Решения отдельных подзадач затем объединяются, давая решение исходной задачи. В задаче сортировки исходный массив размерности n можно разбить на два массива размерности n/2, для каждого из которых рекурсивно