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

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

Класс стек

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

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 - это несколько примеров из десятков стандартных категорий, используемых в библиотеках и применяемых повсеместно в примерах этой книги.

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