if x >= 0 then y := sqrt (x) end
Но проверка может быть чуть менее очевидной, если, например:
x := a^2 + b^2
Инструкция check дает возможность выразить наше предположение о свойствах объектов:
x := a^2 + b^2
... Другие инструкции ...
check
x >= 0
-- Поскольку x был вычислен как сумма квадратов.
end
y := sqrt (x)
Здесь нет конструкции if... then..., защищающей вызов sqrt; но check показывает, что вызов корректен. Хорошей практикой является сопровождать инструкцию комментарием с обоснованием утверждения, как это сделано в примере. Отступы при записи инструкции это тоже часть рекомендованного стиля; они подчеркивают, что при нормальных обстоятельствах инструкция проверки никак не влияет на ход алгоритмического процесса вычислений.
Этот пример типичен для демонстрации того, что наиболее вероятное применение инструкции проверки состоит в добавлении ее, как раз перед вызовом программы, имеющей предусловие. В качестве еще одного примера рассмотрим вызов
s.remove
в точке, где вы точно знаете, что стек s не пуст, поскольку до этого в стек засылалось n элементов, а удалялось m, и вам известно, что n>m. В этом случае нет необходимости защищать вызов: if (not s.empty) then ...; но, если причина корректности вызова непосредственно следует из контекста, то есть смысл напомнить читателю, что "беззащитный" вызов является осознанным решением, а не недосмотром. Этого можно достичь, добавляя проверку:
check not s.empty end
Вариант такой ситуации встречается, когда пишется вызов в форме x.f в полной уверенности, что x/=Void, так что нет необходимости заключать этот вызов в оператор if (x/=Void) then ..., но, тем не менее, существование x не очевидно из контекста. Вернемся к рассмотрению процедур put и remove нашего "защищенного" класса STACK3. Вот текст тела процедуры put:
if full then
error := Overflow
else
check representation /= Void end
representation.put (x); error := 0
end
Здесь читатель может думать, что вызов в else ветви: representation.put(x) потенциально не безопасен, поскольку ему не предшествует тест: (representation /=Void). Но, исследуя текст класса, можно понять, что из условия (full = false) следует положительность capacity, откуда, в свою очередь, следует, что representation не может быть Void. Это важное и не совсем тривиальное свойство, которое должно быть частью инварианта реализации класса. Фактически, с полностью установленным инвариантом реализации следует переписать инструкцию проверки следующим образом:
check
representation_exists: representation /= Void
-- Поскольку предложение representation_exists истинно, когда
-- full ложно, что следует из инварианта реализации.
end
В обычных подходах к конструированию ПО, хотя вызовы и другие операции часто основываются на корректности различных предположений, последние, чаще всего, остаются неявными. Разработчик уверяет себя, что некоторое свойство всегда имеет место в некоторой точке, использует этот анализ при написании кода, но после всего этого, не фиксирует этого в тексте программы, в результате смысл работы потерян. Когда некто, возможно, сам автор, несколькими месяцами позже, захочет разобраться в программе, возможно, с целью ее модификации, ему придется начинать работу с нуля, поскольку все предположения остались в сознании автора. Инструкция check помогает избежать подобных проблем, требуя документирования нетривиальных предположений.
| Механизмы утверждений, рассмотренные в этой лекции, помимо того, что они дают преимущества все вещи делать правильно с самого начала, они еще позволяют найти то, что сделано неверно. Используя параметры компиляции можно включить проверку, и сделать инструкцию check реально проверяемой в период выполнения. Если все предположения выполняются, то проверка не оказывает воздействия на процесс вычислений, но, если вы ошиблись, и предположения не выполняются, то в точке их нарушения будет выброшено исключение и процесс остановится. Тем самым появляется возможность быстрого обнаружения содержательных ошибок. Механизм checking - включения проверок будет вкратце рассмотрен в дальнейшем. |
Инварианты и варианты цикла
Наши следующие и последние конструкции утверждений помогут строить корректные циклы. Эти конструкции являются прекрасным дополнением рассмотренных ранее механизмов. Поскольку они не являются специфической частью ОО-метода, то вы вправе пропустить этот раздел при первом чтении.
Трудности циклов
Возможность повторять некоторые вычисления произвольное число раз, не поддаваясь усталости, без случайных потерь чего-либо важного, - в этом принципиальное отличие компьютерных вычислений от возможностей человека. Вот почему циклы так важны. Трудно вообразить, что можно было бы делать в языках, в которых были бы только две управляющие структуры - последовательность и выбор, - но не было бы циклов и не было бы поддержки рекурсии, еще одного базисного механизма поддержки итеративных вычислений.
Но с мощностью приходят и риски. У циклов дурная слава, - их трудно заставить работать правильно. Типичными для циклов являются:
[x]. Ошибки "больше-меньше" (выполнение цикла слишком много или слишком мало раз).
[x]. Ошибки управления пограничными ситуациями, например пустыми структурами. Цикл может правильно работать на больших массивах, но давать ошибки, когда у массива один элемент или он вообще пуст.
[x]. Ошибки завершения ("зацикливание") в некоторых ситуациях.
Бинарный поиск - один из ключевых элементов базового курса "Введение в информатику" (Computer Science 101) - хорошая иллюстрация "коварства" циклов даже в относительно тривиальной ситуации. Рассмотрим целочисленный, упорядоченный по возрастанию массив t с индексами от 1 до n. Используем алгоритм бинарного поиска для ответа на вопрос: появляется ли целое x среди элементов массива. Если массив пуст, ответ должен быть "нет", если в массиве ровно один элемент, то ответ "да" тогда и только тогда, когда элемент массива совпадает с x. Суть бинарного поиска, использующего упорядоченность массива, проста: вначале x сравнивается со средним элементом массива, если есть совпадение, то задача решена, если x меньше среднего элемента, то поиск продолжается в верхней половине массива, в противном случае - в нижней половине. Каждое сравнение уменьшает размер массива вдвое. Ниже представлены четыре попытки реализации этой простой идеи. К несчастью, все они содержат ошибки. Вам предоставляется случай поупражняться в поиске ошибок и установить, в какой ситуации каждый из алгоритмов не работает нужным образом.
| Напомню, t @ m означает элемент массива t с индексом m. Знак операции // означает деление нацело, так что 7 // 2 и 6 // 2 дают значение 3. Синтаксис цикла будет дан ниже, но он должен быть и так понятен. Предложение from вводит инициализацию цикла. |