, если из истинности предиката 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, |