Бертран Мейер - Основы объектно-ориентированного программирования

check

representation_exists: representation /= Void

-- Поскольку предложение representation_exists истинно, когда

-- full ложно, что следует из инварианта реализации.

end

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

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

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

Но с мощностью приходят и риски. У циклов дурная слава, - их трудно заставить работать правильно. Типичными для циклов являются:

[x].Ошибки "больше-меньше" (выполнение цикла слишком много или слишком мало раз).

[x].Ошибки управления пограничными ситуациями, например пустыми структурами. Цикл может правильно работать на больших массивах, но давать ошибки, когда у массива один элемент или он вообще пуст.

[x].Ошибки завершения ("зацикливание") в некоторых ситуациях.

Бинарный поиск - один из ключевых элементов базового курса "Введение в информатику" (Computer Science 101) - хорошая иллюстрация "коварства" циклов даже в относительно тривиальной ситуации. Рассмотрим целочисленный, упорядоченный по возрастанию массив t с индексами от 1 до n . Используем алгоритм бинарного поиска для ответа на вопрос: появляется ли целое x среди элементов массива. Если массив пуст, ответ должен быть "нет", если в массиве ровно один элемент, то ответ "да" тогда и только тогда, когда элемент массива совпадает с x . Суть бинарного поиска, использующего упорядоченность массива, проста: вначале x сравнивается со средним элементом массива, если есть совпадение, то задача решена, если x меньше среднего элемента, то поиск продолжается в верхней половине массива, в противном случае - в нижней половине. Каждое сравнение уменьшает размер массива вдвое. Ниже представлены четыре попытки реализации этой простой идеи. К несчастью, все они содержат ошибки. Вам предоставляется случай поупражняться в поиске ошибок и установить, в какой ситуации каждый из алгоритмов не работает нужным образом.

Таблица 11.3.Четыре (ошибочных) попытки реализации бинарного поиска

Разумное использование утверждений может помочь справиться с такими проблемами. Цикл может иметь связанное с ним утверждение, так называемый инвариант цикла ( loop invariant), который не следует путать с инвариантом класса. Он может также иметь вариант цикла ( loop variant), являющийся не утверждением, а, обычно целочисленным выражением. Совместно, инвариант и вариант позволяют гарантировать корректность цикла.

Для понимания этих понятий необходимо осознать, что цикл - это способ вычислить некоторый результат последовательными приближениями (successive approximations).

Рассмотрим тривиальный пример вычисления максимума в целочисленном массиве, используя очевидный алгоритм:

maxarray (t: ARRAY [INTEGER]): INTEGER is

-- Максимальное значение массива t

require

t.capacity >= 1