Синтаксис цикла

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

[x]. Инвариант цикла inv - утверждение.

[x]. Условие выхода exit, чья конъюнкция с inv дает желаемую цель.

[x]. Вариант var - целочисленное выражение.

[x]. Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.

[x]. Множество инструкций body, которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv), сохраняет инвариант и уменьшает var, в то же время следя за тем, чтобы оно не стало меньше нуля.

[x]. Синтаксис цикла честно комбинирует эти ингредиенты:

from

init

invariant

inv

variant

var

until

exit

loop

body

end

Предложения invariant и variant являются возможными. Предложение from по синтаксису требуется, но инструкция init может быть пустой.

Эффект выполнения цикла можно описать так: вначале выполняется init, затем 0 или более раз выполняется тело цикла, которое перестает выполняться, как только exit принимает значение false.

В языках Pasal, C и других такой цикл называется "циклом while ", в отличие от цикла типа " repeat... until ", в котором тело цикла выполняется, по меньшей мере, один раз. Здесь же тест является условием выхода, а не условием продолжения, и синтаксис цикла явно содержит фазу инициализации. Потому эквивалент записи нашего цикла на языке Pascal выглядит следующим образом:

init;

while not exit do body

С вариантами и инвариантами цикл для maxarray выглядит так:

from

i:= t.lower; Result:= t @ lower

invariant

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

variant

t.lower - i

until

i = t.upper

loop

i:= i + 1

Result:= Result.max (t @ i)

End

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

Вот еще один пример, ранее показанный без вариантов и инвариантов. Целью следующей функции является вычисление наибольшего общего делителя - НОД (gcd - greatest common divisor) двух положительных целых a и b, следуя алгоритму Эвклида:

gcd (a, b: INTEGER): INTEGER is

-- НОД a и b

require

a > 0; b > 0

local

x, y: INTEGER

do

from

x:= a; y:= b

until

x = y

loop

if x > y then x:= x - y else y:= y - x end

end

Result:= x

ensure

-- Result является НОД a и b

end

Как узнать, что функция gcd удовлетворяет своему постусловию и действительно вычисляет наибольший общий делитель a и b? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации:

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

Это и будет служить инвариантом цикла inv. Ясно, что inv выполняется после инициализации. Если выполняется inv и условие цикла x /= y, то после выполнения тела цикла:

if x > y then x:= x - y else y:= y - x end

инвариант inv остается истинным, замена большего из двух положительных неравных чисел их разностью не меняет их gcd и оставляет их положительными. Тогда по завершению цикла следует:

x = y and «Пара <x, y> имеет тот же НОД, что и пара <a, b>»

Отсюда, в свою очередь, следует, что x является наибольшим общим делителем. По определению НОД (x, x) = x.

Как узнать, что цикл всегда завершается? Необходим вариант. Если x больше чем y, то в теле цикла x заменяется разностью x-y. Если y больше x, то y заменяется разностью y-x. Нельзя в качестве варианта выбрать ни x, ни y, поскольку для каждого из них нет гарантии уменьшения. Но можно быть уверен, что максимальное из них обязательно будет уменьшено. Поэтому разумно выбрать в качестве варианта x.max(y). Заметьте, вариант всегда остается положительным. Теперь можно написать цикл со всеми предложениями:

from

x:= a; y:= b

invariant

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

variant

x.max (y)

until

x = y

loop

if x > y then x:= x - y else y:= y - x end

end

Как отмечалось, предложения invariant и variant являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность. Для любого нетривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.

Использование утверждений

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

[x]. Помощь в создании корректного ПО.

[x]. Поддержка документирования.

[x]. Поддержка тестирования, отладки и гарантия качества.

[x]. Поддержка приемлемого способа обработки неисправностей.

Только два последних пункта предполагают мониторинг утверждений в период выполнения.

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

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

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

Использование утверждений для документирования: краткая форма класса

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

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

Вот пример краткой формы класса STACK4:

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

%Первый пришел - Последний ушел, с фиксированной емкостью"

class interface STACK4 [G] creation

make

feature -- Initialization (Инициализация)

make (n: INTEGER) is

-- Создать стек, содержащий максимум n элементов

require

non_negative_capacity: n >= 0

ensure

capacity_set: capacity = n

end

feature -- Access (Доступ)

capacity: INTEGER

-- Максимальное число элементов стека

count: INTEGER

-- Число элементов стека

item: G is

-- Элемент в вершине стека

require

not_empty: not empty -- i.e. count > 0

end

feature -- Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

ensure

empty_definition: Result = (count = 0)

end

full: BOOLEAN is

-- Заполнен ли стек?

ensure

full_definition: Result = (count = capacity)

end

feature -- Element change (Изменение элементов)

put (x: G) is

-- Втолкнуть x в вершину стека

require

not_full: not full

ensure

not_empty: not empty

added_to_top: item = x

one_more_item: count = old count + 1

end

remove is

-- Удалить элемент вершины стека

require

not_empty: not empty -- i.e. count > 0

ensure

not_full: not full

one_fewer: count = old count - 1

end

invariant

count_non_negative: 0 <= count

count_bounded: count <= capacity

empty_if_no_elements: empty = (count = 0)

end

Эта краткая форма не является синтаксически правильным текстом класса, посему здесь используется термин class interface вместо обычного термина class. Хотя достаточно просто превратить эту форму в правильный отложенный класс, известное понятие, рассматриваемое в деталях при изучении наследования.

В среде ISE получить краткую форму можно одним щелчком соответствующей кнопки в Class Tool; можно генерировать либо плоский текст, либо текст в форматах HTML, RTF, MML (FrameMaker), TEX и других. Можно определить и свой собственный формат.Если сравнить краткую форму утверждений с их оригиналами в классе, то можно заметить, что исчезли все предложения, включающие representation, так как этот атрибут не экспортируется.

Краткая форма документации особенно интересна по следующим причинам:

[x]. Документация является более высокой формой абстракции, чем объект, который она описывает. Это основное требование, предъявляемое к качественной документации. Фактическая реализация, описывающая "как", удаляется. Утверждения, объясняющие "что", а в некоторых случаях и "почему", остаются. Сохраняются заголовочные комментарии к программам и описания, включаемые в предложение indexing, дополняющие в менее формальной форме утверждения, поясняя цель и назначение программы.

[x]. Являясь прямым следствием принципа Самодокументирования, изучаемого в нашем обзоре концепций модульности, краткая форма рассматривает документацию как информацию, содержащуюся в самом программном продукте. Это означает, что есть только один сопровождаемый продукт, - важное требование, проходящее через всю книгу. Как результат, появляется больше шансов корректности документации. Сохраняя все в одном месте, вы уменьшаете риск несоответствия документации обновленному продукту.

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

Интересно сравнить этот подход с понятием интерфейса пакета в языке Ada, где модуль (пакет) состоит из двух частей - интерфейса и реализации. Java использует подобный механизм. Интерфейс пакета имеет некоторое сходство с краткой формой, но имеет и существенные различия:

[x]. Здесь нет утверждений, так что вся спецификация сводится к объявлению типов и комментариям.

[x]. Интерфейс не создается автоматически, а пишется независимо от реализации. Поэтому разработчик дважды должен задавать многие вещи: заголовки программ, их сигнатуры, комментарии к заголовкам, объявления открытых переменных. Эта навязанная избыточность утомительна (вдвойне при включении утверждений) и, как обычно, повышает риск несоответствия; всегда есть шанс, обновить одну часть и забыть про другую.

Краткая форма, дополненная ее вариантом - плоско-краткой формой (flat-short form), изучаемой при рассмотрении наследования, является принципиальным вкладом в ОО-метод. В повседневной практике ОО-разработки она появляется не только как средство документирования, но и как стандартный формат, в котором разработчики и менеджеры изучают существующие проекты, разрабатывают новые и обсуждают предложения по изменению проектов.

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

Мониторинг утверждений в период выполнения

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

Напомню также, что Lace один из возможных языков, позволяющих управлять сборкой системы; он не является неизменяемым компонентом метода. Но всегда необходимо подобное средство для перехода от отдельных компонент к полной компилируемой системе.Вот пример применения Ace файла, устанавливающего некоторые параметры мониторинга утверждений:

system painting root

GRAPHICS

default

assertion (require)

cluster

base_library: ""

graphical_library: ""

option

assertion (all): BUTTON, color_BITMAP

end

painting_application: ""

option

assertion (no)

end

end -- system painting

Предложение default указывает, что для большинства классов системы проверяться будут только предусловия (require). Два кластера переопределяют установки умолчания. Кластер graphical_library будет наблюдать за всеми (all) утверждениями в классах BUTTON и color_BITMAP. Кластер painting_application вообще отменяет наблюдение за утверждениями во всех его классах. Этот пример иллюстрирует возможности мониторинга на разных уровнях - всей системы, отдельных кластеров, отдельных классов.

Следующие ключевые слова, управляющие проверкой утверждений, могут появиться в круглых скобках assertion(...):

[x]. no - не выполнять никакое из утверждений. В этом режиме оказывают на выполнение не больший эффект, чем комментарии;

[x]. require - только проверка выполнимости предусловий на входе программ;

[x]. ensure - проверка выполнимости постусловий на выходе из программы;

[x]. invariant - проверка выполнимости инвариантов класса на входе и выходе программы для квалифицированных вызовов (obj.f);

[x]. loop - проверка выполнимости инвариантов цикла перед и после каждой итерации; проверка уменьшения вариантов на каждой итерации с сохранением их не отрицательности;

[x]. check - выполнение предложений check, проверяющих выполнимость соответствующих утверждений. Ключевое слово all является синонимом check.

За исключением " no " каждый уровень автоматически влечет выполнение всех предыдущих уровней. В частности, не имеет смысла управлять постусловиями, если не проверить выполнимость предусловий. Этим объясняется эквивалентность check и all.

При включенном мониторинге пока утверждения выполняются никакого видимого эффекта на процесс вычислений они не оказывают, если не считать затрат процессорного времени. Но если одно из утверждений принимает значение false, то это довольно серьезное событие, приводящее обычно к завершению работы. Фактически, возбуждается исключение, и, если не принять специальных мер по захвату этого исключения, то выполнение остановится. При этом, однако, будет создана таблица истории исключения (exception history table) в ее общей форме:

Failure: object: O2 class: YOUR_CLASS routine: your_routine

Cause: precondition violation, clause: not_too_small

Called by: object: O2 class: YOUR_CLASS routine: his_routine

Called by: object: O1 class: HER_CLASS routine: her_routine

...

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

Возможные метки, допускаемые в утверждениях, такие как not_too_small в

your_routine (x: INTEGER) is

require

not_too_small: x >= Minimum_value

...

перечисляются при трассировке исключения, что помогает идентифицировать, что же именно пошло не так.

Каков оптимальный уровень мониторинга?

Какой уровень трассировки следует включать? Ответ вырабатывается в результате компромисса, с учетом следующих факторов: уровня доверия к корректности ПО, насколько критичны потери эффективности, насколько серьезны последствия не обнаруженных ошибок в период выполнения.

В экстремальных ситуациях все ясно:

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

[x]. Для системы с полной степенью доверия в приложениях, критичных по времени выполнения, где каждая микросекунда на счету, - следует полностью удалять мониторинг.

Последний совет парадоксален, при отсутствии формальных доказательств корректности говорить о "полной степени доверия" вряд ли возможно. Стоит привести красноречивое высказывание C. A. Hoare:

Абсурдно выполнять проверку в период отладки, когда не требуется доверие к получаемым результатам, и отключать ее в рабочем состоянии, когда ошибочный результат может стоить дорого или вообще катастрофичен. Что бы вы подумали о любителе плавания, который надевает спас-жилет во время тренировок на берегу и снимает его, бросаясь в море [Hoare 1973].Интересную возможность дает параметр, включающий проверку предусловий. В рабочем режиме, когда отладка завершена и даны гарантии качества, крайне важно избежать катастроф в результате необнаруженных вызовов программ вне области их применения. Эта проверка обходится намного дешевле, чем проверка постусловий и инвариантов. Инварианты, в частности, особенно дороги, поскольку они проверяются на входе и выходе каждого квалифицированного вызова, и, что более важно, они всегда сложны, поскольку включают условия согласованности компонент класса.

Проверка предусловий - это параметр, устанавливаемый по умолчанию в Ace файле. Его появление в примере не было необходимым.

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

Вероятно, наиболее очевидным примером является проверка границ массива. В классе ARRAY мы видели, что put, item и его синоним - инфиксный знак операции @, - все они имеют предусловие:

index_not_too_small: lower <= i

index_not_too_large: i <= upper

Включение предусловий для класса решает хорошо известную проблему любого продукта, использующего массивы: возможность выхода индекса за границы массива, что приводит к попаданию в область памяти, отведенную другим данным или коду, и может иметь разрушительные последствия. Большинство компиляторов предлагают специальный параметр компиляции, позволяющий управлять доступом к массиву в период выполнения. Но в объектной технологии массивы рассматриваются с общих позиций класса и объектов, а не как специальные конструкции. Мониторинг границ становится доступным благодаря общему механизму проверки условий. Просто скомпилируйте класс ARRAY, включив assertion(require).

Следует ли всегда включать проверку границ? Вот что говорит по этому поводу Тони Хоар:

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

Кто-то может занимать менее экстремальную позицию. Прежде всего, это компании, поставляющие ПО, в котором ошибки предусловий, "часто встречающиеся в работающей системе", связаны и с низким качеством самой системы, не решаемые мониторингом утверждений. Мониторинг фиксирует следствия - неисправности (fault), но не причины - ошибки и дефекты. Это правда, что мониторинг полезен конечным пользователям даже в системе низкого качества. Лучше часто получать сообщения об ошибках, чем получать неверные результаты. Есть один неприятный эффект, возникающий у разработчиков, поставляющих системы с некоторым уровнем мониторинга утверждений. У них может возникнуть, даже неосознанная, беззаботная позиция по отношению к корректности. Нестрашно, что есть ошибки в поставляемом ПО - пользователи их обнаружат в процессе мониторинга, и мы исправим их в очередной версии. Так не стоит ли остановить отладку прямо сейчас и начать поставку системы?

Трудно дать абсолютный ответ на вопрос "следует ли оставлять включенным некоторый уровень мониторинга?". Без знания потери производительности на мониторинг утверждений на него не ответить. Если добавление мониторинга увеличивает время работы системы в 10 раз, то немногие поддержат точку зрения Хоара, кроме тех, кто занимается критически важными приложениями, где за ошибки приходится дорого платить. Если потери производительности на мониторинг составляют два процента, то немногие решатся отключить мониторинг. На практике, конечно, потери находятся где-то посредине.

Но, между прочим, каковы они? Ясно, что многое зависит от того, что делает ПО, и как много в нем утверждений, но можно сообщить некоторые эмпирические наблюдения. По опыту ISE стоимость мониторинга предусловий (параметр по умолчанию, включающий, конечно, и проверку границ массивов) составляет 50%. Что самое удивительное, - 75% этой стоимости не связано с проверкой предусловий, а идет на поддержку трассировки вызовов, чтобы при нарушении предусловия можно было точно сказать, кто нарушил и где. Это может быть названо Парадоксом Проверки Предусловия: проверка предусловия сама по себе недорого стоит, но, чтобы получить ее, нужно заплатить за дополнительные услуги. Что касается постусловий и инвариантов, то штраф может достигать от 100% до 200%.

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

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

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

Давайте не остановимся на этом, а зададим действительно трудный вопрос. Предположим, что 12 часов уходит на работу системы с включенными проверками, Хотелось ли бы вам удалить их, чтобы получить прогноз за 6 часов, а не за 12, или тратить те же 12 часов, но перейти к более сложному алгоритму, дающему лучший прогноз? Я думаю, что если предлагается "возможность выключить проверки в интересах эффективности производственной системы", почти каждый ответит "да".

В конечном итоге, выбор уровня мониторинга в производственных системах не так прост, как предполагает Хоаровское правило. Следует соблюдать несколько точных и строгих правил.

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

[x]. Если вы являетесь менеджером проекта, никогда не позволяйте своим разработчикам предполагать, что в производственной версии проверки будут включены. Заставьте каждого исходить из того, - все проверки могут быть выключены. Это особенно важно для больших систем, в природе которых устрашающие последствия ошибок.

[x]. Убедитесь, что в процессе разработки системы проверка утверждений всегда включена, по меньшей мере, на уровне предусловий.

[x]. Выполняйте интенсивное тестирование со всеми включенными проверками. Включайте также все проверки при каждом найденном жучке и устранении его последствий.

[x]. Для стандартной производственной версии решите, выберите ли версию без проверок или защищенную версию. Напомню о трех факторах, рассмотренных в самом начале этого раздела, которые следует учитывать при принятии решения.

[x]. Если вы решите выбрать версию без проверок в качестве стандарта, то включите в поставку и версию с проверками, по меньшей мере, предусловий. В случае, если система у пользователей начнет вести себя непредсказуемым способом, вопреки ожиданиям, вы сможете попросить пользователей перейти на защищенную версию, что поможет быстро отыскать неисправности системы.

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

Дата добавления: 2014-01-07