end
feature -- Element change (Изменение элементов)
put (x: G) is
-- Добавить элемент x на вершину
require
not_full: not full -- т.е. count < capacity в этом представлении
do
count := count + 1
representation.put (count, x)
ensure
not_empty: not empty
added_to_top: item = x
one_more_item: count = old count + 1
in_top_array_entry: representation @ count = x
end
remove is
-- удалить элемент вершины стека
require
not_empty: not empty -- i.e. count > 0
do
count := count - 1
ensure
not_full: not full
one_fewer: count = old count - 1
end
feature {NONE} -- Implementation (Реализация)
representation: ARRAY [G]
-- Массив, используемый для хранения элементов стека
invariant
... Будет добавлен позднее ...
end
Текст класса иллюстрирует простоту работы с утверждениями. Это полный текст, за исключением предложений invariant, задающих инварианты класса, которые будут добавлены позднее в этой лекции. Давайте исследуем различные свойства класса.
Это первый законченный класс этой лекции, не слишком далеко отличающийся от того, что можно найти в профессиональных библиотеках повторно используемых ОО-компонентов, таких как Базовые библиотеки. Одно замечание о структуре класса. Поскольку класс имеет более двух-трех компонентов, возникает необходимость сгруппировать его компоненты подходящим образом. Нотация позволяет реализовать такую возможность введением множества предложений feature. Это свойство группировки компонентов, введенное в предыдущей лекции, использовалось там, как способ задания различного статуса экспорта компонентов. И здесь в последней части класса, помеченной Implementation, это свойство используется для указания защищенности компонента
Стандартные категории feature и связанные с ними комментарии к предложениям Feature являются частью общих правил организации повторно используемых библиотек классов.
Императив и аппликатив (применимость)
Утверждения из
Утверждения
full: BOOLEAN is
-- Заполнен ли стек?
do
Result := (count = capacity)
ensure
full_definition: Result = (count = capacity)
end
Постусловие говорит, что
Фактически между двумя конструкциями большая разница. Присваивание это команда, отданная виртуальному компьютеру на изменение его состояния. Утверждение ничего не делает, оно специфицирует свойство ожидаемого заключительного состояния, полученное клиентом, вызвавшим программу.
Инструкция предписывает (prescriptive), утверждение описывает (descriptive). Инструкция описывает 'как', утверждение описывает 'что'. Инструкция является частью реализации, утверждение - элементом спецификации.
Инструкция императивна, утверждение - аппликативно. Эти два термина выражают фундаментальную разницу между программированием и математикой.
[x]. Компьютерные операции могут изменять состояние аппаратно-программной машины. Инструкции в языках программирования являются командами (императивные конструкции), заставляющие машину выполнять такие операции.
[x]. Математические вычисления никогда ничего не меняют. Как отмечалось при рассмотрении АТД, взятие квадратного корня от числа 2 не меняет это число. Вместо этого математики описывают как, используя свойства одних объектов, вывести свойства других, таких как v2, полученных применением (applying - отсюда и термин 'аппликативный') математических трансформаций.
То, что две нотации в нашем примере так близки, - присваивание и эквивалентность - не должно затемнять фундаментальное различие. Утверждение описывает ожидаемый результат, инструкция предписывает способ его достижения. Клиенты модуля обычно интересуются утверждениями, а не реализациями.
Причина близости нотаций в том, что присваивание зачастую кратчайший путь достижения
