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

1.Create:        → L_list        Начать работу( создать пустой список )
2.Null:       L_list → Boolean   Список пуст?
3.Emply:      L_list → L_list    Сделать список пустым
4.GoBOL:      L_list → L_list    Встать в начало списка (сделать текущим
                                 первый элемент, тогда пройденная часть
                                 списка пуста)
5.EOList:     L_list → Boolean   Конец списка (непройденная часть списка
                                 пуста)?
6.GoNext:     L_list → L_list    Перейти к следующему элементу; если те-
                                 кущим был последний, то новое состояние
                                 списка – EOList; отказ: в состояниях Null,
                                 EOList
7.GetEl:      L_list → El        Получить текущий элемент; отказ: в состоя-
                                 ниях Null, EOList
8.Insert:     L_list × El →      Добавить элемент перед текущим ( в состоя-
              L_list             нии EOList добавить элемент в конец спи-
                                 ска),сделать текущим новый элемент
9.Replace:    L_list × El →      Заменить текущий элемент; отказ: в состоя-
              L_list             ниях Null, EOList
10.Delete:    L_list → L_list    Удалить текущий элемент, следующий сде-
                                 лать текущим; отказ: в состояниях Null,
                                 EOList
11.Destroy: L-list →             Закончить работу

                  Рис.1.6. Функциональная спецификация Л1-списка

    Пусть Left( s ) – последовательность, соответствующая пройденной части
списка s, Right( s ) – непройденной его части, начиная с текущего элемента, а
Seq( s ) – всему списку в целом. Cостояние BOList (начало списка) будем фик-
сировать, когда текущим элементом является первый элемент списка, т.е.
Left( s ) = ∆, Right( s ) = Seq( s ). Состояние EOList (конец списка) фиксируется,
когда Left( s ) = Seq( s ) и Right( s ) = ∆. Текущий элемент при этом не опреде-
лен, а операция Insert имеет особый смысл (добавить элемент в конец списка).
    Семантика операций 1,2,3,5 ясна из рис.1.6. Для остальных базовых опера-
ций зададим их семантику в виде свойств (троек Хоара) {Pred} Op {Post}, где
Pred – предусловие, Оp – операция, Post – постусловие. Используем обозна-
чения: s, s0 – списки типа L_list; L, R, R1 – последовательности; e – переменная
типа El.
Op4: { s0 = s }
       GoBOL( s )
       { Left( s ) = ∆ & Right( s ) = Seq( s0 ) } ;
Op6: { not Null( s ) & not EOList( s ) & L = Left( s ) & R = Right( s ) }
        GoNext( s )
       { Left( s ) = L*First( R ) & Right( s ) = Rest( R ) } ;

                                        7