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

Op7: { s0 = s & not Null( s ) & not EOList( s ) & R = Right( s ) }
     GetEl( s, e )
     { e = First( R ) & s = s0 };
Op8: { L = Left( s ) & R = Right( s ) }
     Insert( s, e )
     { Left( s ) = L & Right( s ) = Prefix( e, R ) };
Op9: { not Null(s) & not EOList(s) & L = Left( s ) & R = Right(s) & R1 = Rest(R)
}
     Replace( s, e )
     { Left( s ) = L & Right( s ) = Prefix( e, R1 ) };
Op10:{ not Null(s) & not EOList(s) & L = Left(s) & R = Right(s) & R1 = Rest(R) }
     Delete( s )
     { Left( s ) = L & Right( s ) = R1 }.
   После выполнения операции Destroy( s ) память, отведенная под список s,
освобождается, а значение переменной s становится неопределенным.
   После того, как задана функциональная спецификация, перейдем к рас-
смотрению особенностей реализации линейного списка на основе различных
базовых структур данных.


      1.3. Ссылочная реализация Л1–списка в динамической памяти

   Основная идея реализации Л1–списка ясна из рис. 1.7, а÷г. Список пред-
ставляется агрегатом из собственно цепочки звеньев списка и дополнительной
записи (формуляра списка) из трех полей ссылок на первый, текущий и пред-
шествующий текущему элементы. Содержимое списка и его текущее состоя-
ние полностью определяются этими (и только этими) переменными. Перемен-
ной, идентифицирующей список, является указатель на формуляр списка
(переменная s на рис.1.7,а÷г).
   Память под формуляр списка выделяется при выполнении операции
Create. Выполнение операции Insert приводит к размещению очередного эле-
мента списка в памяти, освободить которую можно, например, удалив этот
элемент с помощью операции Delete. При выполнении операции Empty осво-
бождается вся память, занятая под элементы списка, но сохраняется формуляр
списка. Выполнение операции Destroy равносильно выполнению операции
Empty и, кроме того, приводит к освобождению памяти, отведенной под фор-
муляр списка; значение идентифицирующей список переменной становится
при этом неопределенным.
     Особые состояния списка: Null – пустой список, BOList – начало списка и
EOList – конец списка, определяются как
Null              ↔ (Head = nil) & (PredCur = nil) & (Cur = nil);
BOList & not Null ↔ (Head = Cur ≠ nil) & (PredCur = nil);
EOList & not Null ↔ (Head ≠ nil) & (PredCur ≠ nil) & (Cur = nil) &
                       (PredCur^.link = nil)

                                       8