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

с набором аксиом:
   − аксиомы для MakeRoot (∀ u: α):
             Root ( MakeRoot ( u ) ) = u;
             Null ( Left ( MakeRoot ( u ) ) ) = True;
             Null ( Right ( MakeRoot ( u ) ) ) = True;
   − аксиомы для SetLeft (∀u: α; ∀ b:NonNullBT: Null ( Left ( b ) ) ):
             Left ( SetLeft ( u , b ) ) = MakeRoot ( u );
             Root ( SetLeft ( u , b ) ) = Root ( b );
             Right ( SetLeft ( u , b ) ) = Right ( b );
   − аксиомы для SetRight (∀u: α; ∀b:NonNullBT: Null ( Right ( b ) ) ):
             Right ( SetRight ( u , b ) ) = MakeRoot ( u );
             Root ( SetRight ( u , b ) ) = Root ( b );
             Left ( SetRight ( u , b ) ) = Left ( b ).
   На уровне функциональной спецификации все эти функции могут быть
выражены через функцию ConsBT. При этом приводимые далее соотношения
имеют место для переменных u, b1, b2 таких, что ∀u: α;
∀b2:NonNullBT: Null ( Right ( b2 ) ); ∀b1: NonNullBT: Null ( Left ( b1 ) ):
     MakeRoot(u) = ConsBT( u, Λ, Λ);
     SetLeft ( u , b1) = ConsBT ( Root ( b1), MakeRoot ( u ), Right ( b1) );
     SetRight ( u , b2 ) = ConsBT ( Root ( b2 ), Left ( b2 ), MakeRoot ( u ) ).
   Абстрактные функции SetLeft и SetRight удобнее реализовать в виде проце-
дур, например:
  procedure SetLeft ( a: Elem; b: BinT);
    {Pred: Not Null ( b ) & Null ( Left ( b ) ) }
  begin
   if Null ( b ) then Otkaz ( 5 )
      else
       if Not Null ( Left ( b ) ) then Otkaz ( 6 )
       else b^.LSub := MakeRoot ( a )
  end {SetLeft}

   Рассмотрим ссылочную реализации ограниченного бинарного дерева на
базе вектора:

type Adr = 0 .. MaxAdr;             {диапазон “адресов”в векторе      }
     BinT = Adr;                    {представление бинарного дерева   }
     Node = record                  { узел :                          }
                Info : Elem;         { = содержимое                   }
                LSub : BinT;        { = левое поддерево               }
                RSub : BinT         {    = правое поддерево           }
     end { Node };
     Mem = array [Adr] of Node      { вектор для хранения дерева      }
                                          61