Интернет-журнал "Домашняя лаборатория", 2007 №9
Шрифт:
Условие полной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:
{Pre(x) } Р (х, z) {Post(x,z) }
Доказательство полной корректности обычно состоит из двух независимых этапов — доказательства частичной корректности и доказательства завершаемости программы. Заметьте, полностью корректная программа, которая запущена на входе, не удовлетворяющем ее предусловию, вправе зацикливаться, а также возвращать любой результат. Любая программа корректна по отношению к предусловию, заданному тождественно ложным предикатом False. Любая завершающаяся программа корректна по отношению к постусловию, заданному
Корректная программа говорит своим клиентам: если вы хотите вызвать меня и ждете гарантии выполнения постусловия после моего завершения, то будьте добры гарантировать выполнение предусловия на входе. Задание предусловий и постусловий методов — это такая же важная часть работы программиста, как и написание самого метода. На языке C# пред- и постусловия обычно задаются в теге <summary>, предшествующем методу, и являются частью XML-отчета. К сожалению, технология работы в Visual Studio не предусматривает возможности автоматической проверки предусловия перед вызовом метода и проверки постусловия после его завершения с выбрасыванием исключений в случае их невыполнения. Программисты, для которых требование корректности является важнейшим условием качества их работы, сами встраивают такую проверку в свои программы. Как правило, подобная проверка обязательна на этапе отладки и может быть отключена в готовой системе, в корректности которой программист уже уверен. А вот проверку предусловий важно оставлять и в готовой системе, поскольку истинность предусловий должен гарантировать не разработчик метода, а клиент, вызывающий метод. Клиентам же свойственно ошибаться и вызывать метод в неподходящих условиях.
Формальное доказательство корректности метода — задача ничуть не проще, чем написание корректной программы. Но вот парадокс. Чем сложнее метод, его алгоритм, а следовательно, и само доказательство, тем важнее использовать понятия предусловий и постусловий, понятия инвариантов циклов в процессе разработки метода. Рассмотрение этих понятий параллельно с разработкой метода может существенно облегчить построение корректного метода. Этот подход будет продемонстрирован в нашей лекции при рассмотрении метода 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.