Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода.




Скачать 233.99 Kb.
НазваниеЛекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода.
страница1/3
Дата21.12.2012
Размер233.99 Kb.
ТипЛекция
  1   2   3
Лекция 10. Корректность методов. Рекурсия

Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. Корректность метода по отношению к предусловию и постусловию. Частичная корректность. Завершаемость. Полная корректность. Инвариант цикла. Вариант цикла. Подходящий инвариант. Корректность циклов. Рекурсия. Прямая и косвенная рекурсия. Стратегия «разделяй и властвуй». Сложность рекурсивных алгоритмов. Задача «Ханойские башни». Быстрая сортировка Хоара.

Ключевые слова: корректность; частичная корректность; полная корректность; доказательство корректности; инвариант; вариант цикла; корректность цикла; рекурсия; рекурсивный метод.

Корректность методов

Написать метод, задающий ту или иную функциональность, нетрудно. Это может сделать каждый. Значительно сложнее написать метод, корректно решающий поставленную задачу. Корректность метода – это не внутреннее понятие, подлежащее определению в терминах самого метода. Корректность определяется по отношению к внешним спецификациям метода. Если нет спецификаций, то говорить о корректности некорректно.

Спецификации можно задавать по-разному. Мы определим их здесь через понятия предусловий и постусловий метода, используя символику триад Xoара, введенных Чарльзом Энтони Хоаром – выдающимся программистом и ученым, одну из знаменитых программ которого приведем чуть позже в этой лекции.

Пусть P(x,z) – программа P с входными аргументами x и выходными z. Пусть Q(y) – некоторое логическое условие (предикат) над переменными программы y. Язык для записи предикатов Q(y) формализовать не будем. Отметим только, что он может быть шире языка, на котором записываются условия в программах и включать, например, кванторы. Предусловием программы P(x,z) будем называть предикат Pre(x), заданный на входах программы. Постусловием программы P(x,z) будем называть предикат Post(x,z), связывающий входы и выходы программы. Для простоты будем полагать, что программа P не изменяет своих входов x в процессе своей работы. Теперь несколько определений:

Определение 1 (частичной корректности): Программа P(x,z) корректна (частично или условно) по отношению к предусловию Pre(x) и постусловию Post(x,z), если из истинности предиката Pre(x) следует, что для программы P(x,z), запущенной на входе x, гарантируется выполнение предиката Post(x,z) при условии завершения программы.

Условие частичной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:

[Pre(x)]P(x,z)[Post(x,z)]

Определение 2 (полной корректности): Программа P(x,z) корректна (полностью или тотально) по отношению к предусловию Pre(x) и постусловию Post(x,z), если из истинности предиката Pre(x) следует, что для программы P(x,z), запущенной на входе x, гарантируется ее завершение и выполнение предиката Post(x,z).

Условие полной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:

{Pre(x)}P(x,z){Post(x,z)}

Доказательство полной корректности обычно состоит из двух независимых этапов – доказательства частичной корректности и доказательства завершаемости программы. Заметьте, полностью корректная программа, запущенная на входе, не удовлетворяющему ее предусловию, вправе зацикливаться, вправе возвращать любой результат. Любая программа корректна по отношению к предусловию, заданному тождественно ложным предикатом False. Любая завершающаяся программа корректна по отношению к постусловию, заданному тождественно истинным предикатом True.

Корректная программа говорит своим клиентам, если вы хотите вызвать меня и ждете гарантии выполнения постусловия после моего завершения, то будьте добры гарантировать выполнение предусловия на входе. Задание предусловий и постусловий методов – это такая же важная часть работы программиста, как и написание самого метода. На языке C# пред и постусловия обычно задаются в теге summary, предшествующему методу, и являются частью XML-отчета. К сожалению, технология работы в Visual Studio не предусматривает возможности автоматической проверки предусловия перед вызовом метода и проверки постусловия после его завершения с выбрасыванием исключений в случае их невыполнения. Программисты, для которых требование корректности является важнейшим условием качества их работы, сами встраивают такую проверку в свои программы. Как правило, такая проверка обязательна на этапе отладки и может быть отключена в готовой системе, в корректности которой программист уверен. Проверку предусловий важно оставлять и в готовой системе, поскольку истинность предусловий должен гарантировать не разработчик метода, а клиент, вызывающий метод. Клиентам свойственно ошибаться и вызывать метод в неподходящих условиях.

Формальное доказательство корректности метода – задача ничуть не проще, чем написание корректной программы. Но вот парадокс. Чем сложнее метод, его алгоритм, а следовательно и само доказательство, тем важнее использовать в процессе разработки метода понятия предусловий и постусловий, понятия инвариантов циклов. Рассмотрение их параллельно с разработкой метода может существенно облегчить построение корректного метода. Этот подход будет продемонстрирован в этой лекции при рассмотрении метода QuickSort – быстрой сортировки массива.

Инварианты и варианты цикла

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

Init(x,z); while(B)S(x,z);

Здесь B – условие цикла while, S – его тело, а Init – группа предшествующих операторов, задающая инициализацию цикла. Реально ни один цикл не обходится без инициализирующей части. Синтаксически было бы правильно, чтобы Init являлся бы формальной частью оператора цикла. В операторе for эта частично сделано – инициализация счетчиков является частью цикла.

Определение 3 (инварианта цикла) Предикат Inv(x, z) называется инвариантом цикла while, если истинна следующая триада Хоара:

{Inv(x, z)& B}S(x,z){Inv(x,z)}

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

Для любого цикла можно написать сколь угодно много инвариантов. Любое тождественное условие (2*2 =4) является инвариантом любого цикла. Поэтому среди инвариантов выделяются так называемые подходящие инварианты цикла. Они называются подходящими, поскольку позволяют доказать корректность цикла по отношению к его пред и постусловиям. Как доказать корректность цикла? Рассмотрим соответствующую триаду:

{Pre(x)} Init(x,z); while(B)S(x,z);{Post(x,z)}

Доказательство разбивается на три этапа. Вначале доказываем истинность триады:

(*) {Pre(x)} Init(x,z){RealInv(x,z)}

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

(**) {RealInv(x, z)& B} S(x,z){ RealInv(x,z)}

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

(***) ~B & RealInv(x, z) –> Post(x,z)

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

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

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

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

{(Var(x,z)= n) & B} S(x,z){(Var(x,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 становится равным 1. Это пример так называемой «хвостовой» рекурсии, когда в теле встречается ровно один рекурсивный вызов, стоящий в конце соответствующего выражения. Хвостовую рекурсию намного проще записать в виде обычного цикла. Вот циклическое определение той же функции:

public long fact(int n)

{

long res =1;

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

return(res);

}//fact

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

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. Сравнение времени работы циклической и рекурсивной функций

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

На примере сортировки слиянием покажем, как можно оценить время работы рекурсивной процедуры. Обозначим через T(n) время работы процедуры на массиве размерности n. Учитывая, что слияние можно выполнить за линейное время, справедливо следующее соотношение :

T(n) = 2T(n/2) + cn

Предположим для простоты, что n задается степенью числа 2, то есть n = 2k. Тогда наше соотношение имеет вид:

T(2k) = 2T(2k-1) + c2k

Полагая, что T(1) =c, путем несложных преобразований, используя индукцию, можно получить окончательный результат:

T(2k) = c*k*2k = c*n*log(n)

Известно, что это лучшее по порядку время решения задачи сортировки. Когда исходную задачу удается разделить на подзадачи одинаковой размерности, то при условии существования линейного алгоритма слияния, рекурсивный алгоритм имеет аналогичный порядок сложности. К сожалению, не всегда удается исходную задачу разбить на k подзадач одинаковой размерности n/k. Часто такое разбиение не представляется возможным.
  1   2   3

Похожие:

Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconЛекция «Технология дидактической системы деятельностного метода»
Мотивационная лекция «Технология дидактической системы деятельностного метода» зам директора по увр захарова Г. В
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconПрограммная реализация метода отражений на языке программирования Pascal
Теоретические основы метода отражений (Хаусхолдера) для решения слау
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconПрограмма res2dinv версия 4 (или версия 49h) для Windows 95/98/Me/2000/NT/XP
Быстрая 2-d инверсия данных метода сопротивлений и вп с использованием метода наименьших квадратов
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconАлгебраический порядок точности численного метода (порядок точности численного метода, степень точности численного метода, порядок точности, степень точности) —
«Алгоритм — это конечный набор правил, который определяет последовательность операций для решения конкретного множества задач и обладает...
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconТемы курсовых работ для студентов 4 курса озо специальности «бизнес-администрирование» Модели и методы принятия решений
Использование графического метода и симплекс-метода решения задач линейного программирования
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. icon2 трилатеральная постфильтрация карт глубины 1 1
Видео, построенное с применением данного метода, показало большую стабильность как в пространстве кадра, так и во времени. Также...
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconКурсовая работа Применение метода проблемного обучения в школе
Iii. Практическое применение проблемного метода на примере организации групповой беседы
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. icon«оборачивание метода» в энергетике и физике имманентный логический закон оборачивания метода
Представляется возможным в этой работе рассмотреть пример подобного чрезмерного консерватизма в современной теоретической физике...
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. icon«Реализация метода шнур»
Для более понятного (для читателя) изложения материала были построены различные графики и таблицы, была проведена оценка эффективности...
Лекция 10. Корректность методов. Рекурсия Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. iconРеализация метода интервальной регрессии в пакете knime выпускная работа бакалавра
Даже сейчас, когда с использованием довольно больших вычислительных мощностей этот процесс невозможно проводить без задержек. Время,...
Разместите кнопку на своём сайте:
Библиотека


База данных защищена авторским правом ©lib.znate.ru 2014
обратиться к администрации
Библиотека
Главная страница