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

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

Как только корректность ПО определена как согласованность реализации с ее спецификацией, следует предпринять шаги по включению спецификации в сам программный продукт. Для большинства в программистском сообществе это все еще новая идея. Привычно писать программы, устанавливая тем самым, - как делать ( 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