Страница 283 из 371
Формальное доказательство корректности метода — задача ничуть не проще, чем написание корректной программы. Но вот парадокс. Чем сложнее метод, его алгоритм, а следовательно, и само доказательство, тем важнее использовать понятия предусловий и постусловий, понятия инвариантов циклов в процессе разработки метода. Рассмотрение этих понятий параллельно с разработкой метода может существенно облегчить построение корректного метода. Этот подход будет продемонстрирован в нашей лекции при рассмотрении метода Quicksort — быстрой сортировки массива.
Инварианты и варианты цикла
Циклы, как правило, являются наиболее сложной частью метода — большинство ошибок связано именно с ними. При написании корректно работающих циклов крайне важно понимать и использовать понятия инварианта и варианта цикла. Без этих понятий не обходится и формальное доказательство корректности циклов. Ограничимся рассмотрением цикла в следующей форме:
Init(x,z); while(В)S(х, z);
Здесь B — условие цикла while, S — его тело, a Init — группа предшествующих операторов, задающая инициализацию цикла. Реально ни один цикл не обходится без инициализирующей части.
Синтаксически было бы правильно, чтобы Init являлся бы формальной частью оператора цикла. В операторе for это частично сделано — инициализация счетчиков является частью цикла.
Определение 3 (инварианта цикла): предикат inv(x, z) называется инвариантом цикла while, если истинна следующая триада Хоара:
{Inv(x, z) & B} S(x,z){Inv(x,z)}
Содержательно это означает, что из истинности инварианта цикла до начала выполнения тела цикла и из истинности условия цикла, гарантирующего выполнение тела, следует истинность инварианта после выполнения тела цикла. Сколько бы раз ни выполнялось тело цикла, его инвариант остается истинным.
Для любого цикла можно написать сколь угодно много инвариантов. Любое тождественное условие (2*2 =4) является инвариантом любого цикла. Поэтому среди инвариантов выделяются так называемые подходящие инварианты цикла. Они называются подходящими, поскольку позволяют доказать корректность цикла по отношению к его пред- и постусловиям. Как доказать корректность цикла? Рассмотрим соответствующую триаду:
{Рге(х)} Init(x,z); while(В)S(х, z);{Post(х, z)}
Доказательство разбивается на три этапа. Вначале доказываем истинность триады:
(*) {Рге(х)} Init(х, z){RealInv(х, z)}
Содержательно это означает, что предикат 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.