Постусловия

Постусловия

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

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

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

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

В постусловиях доступна специальная нотация old. Она используется, например, в программах remove и item для выражения изменения значения count. Запись old e, где e - выражение (в большинстве случаев - атрибут) обозначает значение, которое данное выражение имело на входе программы. Любое вхождение e, которому не предшествует old, означает значение выражения на выходе программы.

Постусловие программы put включает предложение:

count = old count + 1

устанавливающее, что put, примененное к любому объекту, должно увеличить на единицу значения поля count этого объекта.