Основы объектно-ориентированного программирования полностью

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

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

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.

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

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

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

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

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

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

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

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