error := Overflow
else
check representation /= Void end
representation.put (x); error := 0
end
Здесь читатель может думать, что вызов в
check
representation_exists: representation /= Void
-- Поскольку предложение representation_exists истинно, когда
-- full ложно, что следует из инварианта реализации.
end
В обычных подходах к конструированию ПО, хотя вызовы и другие операции часто основываются на корректности различных предположений, последние, чаще всего, остаются неявными. Разработчик уверяет себя, что некоторое свойство всегда имеет место в некоторой точке, использует этот анализ при написании кода, но после всего этого, не фиксирует этого в тексте программы, в результате смысл работы потерян. Когда некто, возможно, сам автор, несколькими месяцами позже, захочет разобраться в программе, возможно, с целью ее модификации, ему придется начинать работу с нуля, поскольку все предположения остались в сознании автора. Инструкция
| Механизмы утверждений, рассмотренные в этой лекции, помимо того, что они дают преимущества все вещи делать правильно с самого начала, они еще позволяют найти то, что сделано неверно. Используя параметры компиляции можно включить проверку, и сделать инструкцию check реально проверяемой в период выполнения. Если все предположения выполняются, то проверка не оказывает воздействия на процесс вычислений, но, если вы ошиблись, и предположения не выполняются, то в точке их нарушения будет выброшено исключение и процесс остановится. Тем самым появляется возможность быстрого обнаружения содержательных ошибок. Механизм checking - включения проверок будет вкратце рассмотрен в дальнейшем. |
Наши следующие и последние конструкции утверждений помогут строить корректные циклы. Эти конструкции являются прекрасным дополнением рассмотренных ранее механизмов. Поскольку они не являются специфической частью ОО-метода, то вы вправе пропустить этот раздел при первом чтении.
Возможность повторять некоторые вычисления произвольное число раз, не поддаваясь усталости, без случайных потерь чего-либо важного, - в этом принципиальное отличие компьютерных вычислений от возможностей человека. Вот почему циклы так важны. Трудно вообразить, что можно было бы делать в языках, в которых были бы только две управляющие структуры - последовательность и выбор, - но не было бы циклов и не было бы поддержки рекурсии, еще одного базисного механизма поддержки итеративных вычислений.
Но с мощностью приходят и риски. У циклов дурная слава, - их трудно заставить работать правильно. Типичными для циклов являются:
[x]. Ошибки "больше-меньше" (выполнение цикла слишком много или слишком мало раз).
[x]. Ошибки управления пограничными ситуациями, например пустыми структурами. Цикл может правильно работать на больших массивах, но давать ошибки, когда у массива один элемент или он вообще пуст.
[x]. Ошибки завершения ("зацикливание") в некоторых ситуациях.
