Аксиомы

Для всех x: G, s: STACK [G],

[x]. (A1) item (put (s, x)) = x

[x]. (A2) remove (put (s, x)) = s

[x]. (A3) empty (new)

[x]. (A4) not empty (put (s, x))

Первые две аксиомы выражают основные свойства стеков (последним пришел - первым ушел) LIFO. Чтобы понять их, предположим, что у нас есть стек s и экземпляр x, и определим s' как результат put(s, x), т. е. как результат вталкивания x в s. Приспособим один из предыдущих рисунков:

Рис. 6.4. Применение функции put

Здесь аксиома A1, говорит о том, что вершиной s' является x - последний элемент, который мы втолкнули, а аксиома A2 объясняет, что при удалении верхнего элемента s' мы снова получаем тот же стек s, который был до вталкивания x. Эти две аксиомы дают лаконичное описание главного свойства стеков в чисто математических терминах без всякой помощи императивных рассуждений или ссылок на свойства представлений.

Аксиомы A3 и A4 говорят о том, когда стек пуст, а когда - нет: стек, полученный в результате работы конструктора new пустой, а всякий стек, полученный после вталкивания элемента в уже существующий стек (пустой или непустой) не является пустым.

Эти аксиомы, как и остальные, являются предикатами (в смысле логики), выражающими истинность некоторых свойств для всех возможных значений s и x. Некоторые предпочитают рассматривать A3 и A4 в другой эквивалентной форме как определение функции empty индукцией по размеру стеков:

Для всех x: G, s: STACK [G]

A3' · empty (new) = true

A4' · empty (put (s, x)) = false

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