Основы объектно-ориентированного программирования
Постусловия
Постусловие выражает свойство состояния, завершающего выполнение программы. Здесь:
- После завершения put стек не может быть пуст; на его вершине находится только что втолкнутый элемент, число его элементов увеличилось на единицу.
- После remove стек не может быть полон, число его элементов на единицу уменьшилось.
Постусловие в программе выражает гарантию, представленную создателем программы, что выполнение программы завершается и приводит к состоянию с заданными свойствами, в предположении, что программа была запущена в состоянии, удовлетворяющем предусловию.
В постусловиях доступна специальная нотация old. Она используется, например, в программах remove и item для выражения изменения значения count. Запись old e, где e - выражение (в большинстве случаев - атрибут) обозначает значение, которое данное выражение имело на входе программы. Любое вхождение e, которому не предшествует old, означает значение выражения на выходе программы.
Постусловие программы put включает предложение:
count = old count + 1
устанавливающее, что put, примененное к любому объекту, должно увеличить на единицу значения поля count этого объекта.
