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

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

Спецификации можно задавать по-разному. Мы определим их здесь через понятия предусловий и постусловий метода, используя символику триад 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 - быстрой сортировки массива.