Включение функций в утверждения

Включение функций в утверждения

Булевы выражения не ограничиваются использованием атрибутов и локальных сущностей. Мы уже использовали возможность вызова функций в утверждениях: предусловие для put класса стек было not full, где full - функция

full: BOOLEAN is

-- Is stack full? (Заполнен ли стек?)

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

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

Использование функций ведет к получению более абстрактных утверждений. Например, кто-то предпочтет заменить предусловие в операциях над массивом, ранее выраженное как

index_not_too_small: lower <= i

index_not_too_large: i <= upper

одним предложением в форме

index_in_bounds: correct_index (i)

с определением функции

correct_index (i: INTEGER): BOOLEAN is

-- Является ли i внутри границ массива?

do

Result := (i >= lower) and (i <= upper)

ensure

definition: Result = ((i >= lower) and (i <= upper))

end

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

-- Result является максимумом нарезки массива t в интервале [t.lower,i]

формально может быть выражен так

Result = (t.slice (lower, i)).max

в предположении, что slice вырабатывает нарезку - массив с индексами от lower до i, - а функция max дает максимальный элемент этого массива.

Этот подход был исследован в [M 1995a] как способ расширения выразительной силы механизма утверждений, возможно ведущий к разработке полностью формального метода, - другими словами, к математическому доказательству корректности ПО. В этом исследовании есть две центральные идеи. Первая - использование библиотек в процессе доказательства, так что можно его проводить для реальных, широкомасштабных систем, строя многоярусную структуру, использующую условные доказательства. Вторая идея - определение ограниченного языка чисто аппликативной природы - IFL (Intermediate Functional Language), в котором выражаются функции, используемые в выражениях. Язык IFL является подмножеством нотации этой книги, включающий некоторые императивные конструкции, такие как любые присваивания.

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

Все же трудно сопротивляться мощи использования функций, поскольку все альтернативы имеют свои недостатки.

[x]. Включение полного языка спецификаций, как отмечалось, приводит к потере эффективности и простоты изучения.

[x]. Вероятно, хуже то, что неясно, достаточны ли общепринятые языки утверждений. Возьмем, например, такого естественного кандидата, в которого многие верят, - язык логики предикатов первого порядка. Этот формализм не позволяет нам выразить некоторые свойства, представляющие непосредственный интерес для разработчиков и часто используемые в утверждениях, такие как, например, "граф не имеет циклов" (типичный инвариант цикла). Математически это может быть выражено как r+ r = , где r - это отношение на графе, а+ его транзитивное замыкание. Хотя можно представить себе язык спецификации, поддерживающий эти понятия, большинство языков этого не делают.

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

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

Это неформальное требование достаточно ясно на практике; формализм подъязыка IFL исключает все императивные элементы, которые либо изменяют глобальное состояние системы, либо не имеют тривиальных аппликативных эквивалентов, в частности исключаются:

[x]. присваивания атрибутам;

[x]. присваивания в циклах;

[x]. вызовы программ, не входящих в IFL.

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

Некоторые технические вопросы могут потребовать внимания. Функция f, используемая в утверждении программы r, может сама иметь утверждения, что демонстрируют примеры функций full и correct_index. Возникает потенциальная проблема при мониторинге утверждений в период выполнения: если при вызове r мы вычисляем утверждение, вызывающее f, то не придется ли нам вычислять утверждение для f? Нетрудно сконструировать пример зацикливания, если пойти по этому пути. Но даже и без этого риска было бы неправильно вычислять утверждение для f. Это бы означало, что мы рассматриваем "на равных" программы, являющиеся предметом наших вычислений, такие как r, и их функции утверждения, такие как f. В противовес этому сформулируем правило, согласно которому утверждения должны иметь более высокий приоритет, чем программы, которые они защищают, их корректность должна быть кристально ясной. Правило простое:

Правило вычисления утверждения

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

Если вызов f встречается как часть проверки утверждения программы r, то слишком поздно спрашивать, удовлетворяет ли f своим утверждениям. Подходящим является время, когда решается вопрос использования f в утверждении, применимом к r.

Рассматривайте f как охранника ядерного предприятия, в обязанности которого входит проверка посетителей. Охранников тоже нужно проверять, но не тогда, когда они сопровождают посетителей.

Поделитесь на страничке

Следующая глава >

Похожие главы из других книг:

Совет 46. Передавайте алгоритмам объекты функций вместо функций

Из книги автора

Совет 46. Передавайте алгоритмам объекты функций вместо функций Часто говорят, что повышение уровня абстракции языков высокого уровня приводит к снижению эффективности сгенерированного кода. Александр Степанов, изобретатель STL, однажды разработал небольшой комплекс


11.11. Включение в приложения функций социального обмена контентом

Из книги автора

11.11. Включение в приложения функций социального обмена контентом Постановка задачи Требуется предоставить в приложении функции социального обмена контентом. Например, у пользователя мобильного устройства должна быть возможность написать твит или обновить статус в


Утверждения

Из книги автора

Утверждения Поскольку первое правило гласит, что отладку нужно проводить всегда, а вывод подразумевает, что не хотелось бы краснеть за недостаточный объем тестирования кода, необходимо научиться создавать защищенные программы. И первым средством из защитного арсенала


12.3.5. Адаптеры функций для объектов-функций

Из книги автора

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


Утверждения

Из книги автора

Утверждения Часто условия, проверяемые в WHERE, IF и т.д., не являются простыми предикатами, а группой нескольких предикатов, каждый из которых при вычислении делает вклад в вычисление общей истинности. Утверждение может состоять из одного предиката или из нескольких


19.11.2. Вызов функций из файла функций

Из книги автора

19.11.2. Вызов функций из файла функций Мы уже рассматривали, каким образом функции вызываются из командной строки. Эти типы функций обычно используются утилитами, создающими системные сообщения.А теперь воспользуемся снова описанной выше функцией, но в этом случае


Утверждения (Assertions)

Из книги автора

Утверждения (Assertions) Компоненты абстрактного типа данных имеют формально специфицированные свойства, отражаемые в соответствующих классах.Утверждения - предусловия и постусловия программ класса и инварианты классов - играют эту роль. Утверждения имеют три основных


Утверждения это не управляющие структуры

Из книги автора

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


Инструкция утверждения

Из книги автора

Инструкция утверждения Утверждения, рассматриваемые до сих пор - предусловия, постусловия, инварианты, - это основные составляющие метода. Они устанавливают связь между конструкциями ОО-программных систем и теорией АТД, лежащей в основе метода. Инварианты класса, в


Утверждения как средство для написания корректного ПО

Из книги автора

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


У11.3 Полные утверждения для стеков

Из книги автора

У11.3 Полные утверждения для стеков Покажите, что введение закрытой функции body, возвращающей тело стека, сделает возможным утверждениям класса STACK полностью отражать спецификацию соответствующего АТД. Обсудите теоретическую и практическую значимость такого


У11.6 Утверждения и экспорт

Из книги автора

У11.6 Утверждения и экспорт Обсудите использование функций в утверждениях, в частности, введение функции correct_index в предусловия программ put и item. Если добавить эту функцию в класс ARRAY, то какой статус экспорта следует ей


Переопределение и утверждения

Из книги автора

Переопределение и утверждения Если клиент класса POLYGON вызывает p.perimeter, то он ожидает получить значение периметра p, определенное спецификацией функции perimeter в определении этого класса. Но теперь, благодаря динамическому связыванию, клиент может вызвать другую программу,


Наследование и утверждения

Из книги автора

Наследование и утверждения Следствия красоты базисных идей:[x]. Связь наследования с утверждениями и Проектированием по Контракту.[x]. Глобальная структура наследования, где все классы согласованы.[x]. Замороженные компоненты, для которых не применим принцип


Требовать утверждения внешних подключений

Из книги автора

Требовать утверждения внешних подключений Отслеживание внешних подключений — это хорошее начало для восстановления контроля над вашей сетью. Но вам также следует заняться ограничением этих подключений. На самом деле, не каждому желающему действительно нужен такой