Динамические структуры данных. Алексеев А.Ю - 37 стр.

идентифицирующий пустую последовательность ∆, и 2) либо константу, обо-
значающую пустую последовательность, либо функцию, порождающую зна-
чение ∆, например Create : → Sequence ( El ).
    Рассмотрим формальную спецификацию стека из элементов типа α
( Stack of α ≡ Stack ( α ) ). При этом для обозначения функций First, Rest, Prefix
будем использовать исторически сложившиеся синонимы Top, Pop и Push со-
ответственно (Top − верхушка стека, Pop ( up ) − вытолкнуть (вверх), Push
( down ) – втолкнуть, вжать (вниз)). Функциональная спецификация стека за-
дается следующими определениями (множество непустых стеков обозначим
как Non_null_stack):
    1) Create: → Stack ( α ) ;
    2) Null: Stack ( α ) → Boolean ;
    3) Top: Non_null_stack ( α ) → α ;
    4) Pop: Non_null_stack ( α ) → Stack ( α ) ;
    5) Push: α ⊗ Stack ( α ) → Stack ( α )
и набором аксиом (∀p: α; ∀s: Stack ( α ); ∀t: Non_null_stack ( α ) ):
    A1) Null ( Create ) = true ;
    A2) Null ( Push ( p , s ) ) = false ;
    A3) Top ( Push ( p , s ) ) = p ;
    A4) Pop ( Push ( p , s ) ) = s ;
    A5) Push ( Top ( s ) , Pop ( s ) ) = s.
    Можно заметить, что так определенный абстрактный тип Stack ( α ) факти-
чески (с точностью до обозначений и несущественных деталей) совпадает с
ранее рассмотренным в 1.6 типом L_list ( α ).
    Часто при определении стека вместо функции Pop используют функцию
(процедуру), совмещающую результат действия функций Top и Pop. Обозна-
чим такую процедуру Pop2. Тогда
                   Pop2: Non_null_stack ( α ) → α ⊗ Stack ( α ).
    Можно явно определить Pop2 через функции Top и Pop:
        procedure Pop2 ( out p: α; in-out s: Stack ( α ) );
        begin
         p := Top ( s );
         s := Pop ( s )
      end
   Функциональная спецификация очереди из элементов                     типа    α
( Queue of α ≡ Queue ( α ) ) задается следующими определениями:
   1) Create: → Queue ( α ) ;
   2) Null: Queue ( α ) → Boolean ;
   3) First: Non_null_queue ( α ) → α ;
   4) Rest: Non_null_queue ( α ) → Queue ( α ) ;
   5) Postfix: Queue ( α ) ⊗ α → Queue ( α ) ;
и набором аксиом (∀p: α; ∀ q: Queue ( α ) ):

                                       37