Корректная программа говорит своим клиентам: если вы хотите вызвать меня и ждете гарантии выполнения постусловия после моего завершения, то будьте добры гарантировать выполнение предусловия на входе. Задание предусловий и постусловий методов — это такая же важная часть работы программиста, как и написание самого метода. На языке 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, удовлетворяющий условиям (*), (**), (***) называется подходящим инвариантом цикла.