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

Введение утверждений в программные тексты

Как только корректность ПО определена как согласованность реализации с ее спецификацией, следует предпринять шаги по включению спецификации в сам программный продукт. Для большинства в программистском сообществе это все еще новая идея. Привычно писать программы, устанавливая тем самым, - как делать (the how); менее привычно рассматривать описание целей - что делать (the what) - как часть программного продукта.

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

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

Синтаксически утверждения в нашей нотации будут обычными булевыми выражениями с небольшими расширениями. Одним из расширений является введение в нотацию термина "old", другим - введение символа ";" для обозначения конъюнкции (логического И). Вот пример:

n>0; x /= Void

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

Positive: n > 0

Not_void: x /= Void

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

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

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

Класс стек

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

class STACK [G] feature

... Объявление компонент:

count, empty, full, put, remove, item

end

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

[x]. Программы remove и item применимы, только если число элементов стека не равно нулю.

[x]. put увеличивает, remove - уменьшает число элементов на единицу.

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

indexing

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

%Последний пришел - Первый ушел"

class STACK1 [G] feature - Access (Доступ)

count: INTEGER

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

item: G is

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

require

not empty

do

...

end

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

empty: BOOLEAN is

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

do ... end

full: BOOLEAN is

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

do

...

end

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

put (x: G) is

-- Добавить элемент x на вершину.

require

not full

do

...

ensure

not empty

item = x

count = old count + 1

end

remove is

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

require

not empty

do

...

ensure

not full

count = old count - 1

end

end

Оба предложения require и ensure являются возможными; когда они присутствуют, то появляются в фиксированных местах, require - перед предложением local.

Обратите внимание на разделы feature, группирующие свойства по категориям, снабженных заголовками в виде комментариев. Категории Access, Status report, Element change - это несколько примеров из десятков стандартных категорий, используемых в библиотеках и применяемых повсеместно в примерах этой книги.

Предусловия

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

[x]. put не может быть вызвана, если стек заполнен;

[x]. remove и item не могут быть применены к пустому стеку.

Предусловия применяются ко всем вызовам программы, как внутри класса, так и у клиента. Корректная система никогда не вызовет программу в состоянии, в котором не выполняется ее предусловие.

Постусловия

Постусловие выражает свойство состояния, завершающего выполнение программы. Здесь:

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

[x]. После remove стек не может быть полон, число его элементов на единицу уменьшилось.

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

В постусловиях доступна специальная нотация old. Она используется, например, в программах remove и item для выражения изменения значения count. Запись old e, где e - выражение (в большинстве случаев - атрибут) обозначает значение, которое данное выражение имело на входе программы. Любое вхождение e, которому не предшествует old, означает значение выражения на выходе программы.

Постусловие программы put включает предложение:

count = old count + 1

устанавливающее, что put, примененное к любому объекту, должно увеличить на единицу значения поля count этого объекта.

Педагогическое замечание

Понятно ваше нетерпение и желание незамедлительно узнать, каков же эффект от утверждений при выполнении программы; что произойдет при вызове put при заполненном стеке, или что будет, когда empty дает true по завершении вызова put? Полный ответ на этот вопрос дать еще слишком рано, но предварительный использует любимое словечко адвокатов - это зависит (it depends).

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