Абстрактные типы данных и частичная корректность программ

• Автор: Менц, Хельмут
• Шифр специальности: 01.01.10
• Научная степень: Кандидатская
• Год защиты: 1984
• Место защиты: Москва
• Количество страниц: 140 c. : ил

С ОДЕРЖАНИЕ

ГЛАВА. I. Последовательности операции и Дерево вызовов
ГЛАВА 2. Вопрос о динамической допустимости операции
ГЛАВА 3. Вопрос о частичной корректности программ
ГЛАВА 4. Языковая реализация клетки
ГЛАВА 5. Реализация алгоритма верификации
ГЛАВА 6. Возможные дальнейшие работы
ЗАКЛЮЧЕНИЕ
ПРИЛОЖЕНИЕ № I
133 1
ПРИЛОЖЕНИЕ № 2 ... СШЕОК ЛИТЕРАТУРЫ
В последнее время в развитии программирования все большую роль играют усилия, направленные на повышение надежности программирования. В частности, становятся все важнее попытки повысить надежность программирования путем предоставления новых средств и форм описания данных (см., например [б] , [l9] , [23] , [24] , [28] ,
[36] , [45] ).
Это вызвано, по крайней мере, следующими двумя причинами:
1. Становится все яснее, что "данные являются основным делом программ" [37] в том смысле, что структура данных оказывает большое влияние на структуру обрабатывающих их программ.
2. Однако, имеющиеся в традиционных языках программирования,
как например ФОРТРАН, АЛГ0Л60, ПЛ/1, КОБОЛ и ПАСКАЛЬ, средства описания данных не дают возможность достаточно адекватно описать использующиеся и возникающие в реальных процессах данные.
Из цели повышения надежности программирования при этом следует, что стоит задача создания таких средств описания данных, которые позволяли бы:
1. выражать в программе свойства реальных данных формально и по возможности полностью и естественным образом,
2. сосредоточить описание свойств определенного класса данных и допустимых способов реализации этих свойств в одном месте программы.
Можно считать, что первым шагом для достижения этой цели являлось введение различных конструкций класса (например " class " в СИМУЛА-67, "cluster" в CLU.), которые предоставляют возможность включить в описание данных рядом с описанием класса объектов и описания определенных для этих данных операций, то есть, описания процедур и функций, реализующих определенные над этими объектами операции. Но классы не позволяют объявить в явном виде соотношения между их операциями, взаимные зависимости этих операций. (например условия, при которых выполнение какой-то операции разрешено). Для них такие соотношения надо описать внутри определений самих операций, так что описание каждой операции выполняет

две функции:
1. описываются действия, которые выполняет эта операция и
2. определяются условия, в которых разрешено выполнение этих действий.
Необходимость описания условий применимости операций часто следует из того, что данные нельзя рассматривать как статистические, не подлежащие во время выполнения программы никаким (кроме модификации их значений) изменениям объекты.
Данные программы обычно являются отражением реально существующих данных, как например картотекой рабочих какого-то завода или описания состояния автоматического станка во время изготовления какого-то изделия.
Но реальные данные часто развиваются. Для описания состояния автоматического станка например развитие данных может выражаться в том, что в определенных состояниях, станка разрешены только такие операции, которые соответствуют разрешенным в данный момент процессам дальнейшей обработки изделия.
Желательно, чтобы развитие реальных данных отражалось как можно точнее в данных программы. Есть притом надежда, что возможность, явно описать в определении данных условия для применения определенных для них операций, повысит наглядность этого описания и облегчает их использование. Кроме того можно надеяться, что такая возможность приведет к тому, что программист при определении данных лучше обдумывает вопросы соотношений между операциями.
Явное описание условий применимости отдельных операций данных кроме того дает возможность проверки того, что эти условия соблюдаются программами, обрабатывающими эти данные. Такие (и похожие) соображения привели к возникновению понятия абстрактных типов данных. Мы, следуя Б. Лисков и С. Циллес [37] , под абстрактным типом данных понимаем группу взаимосвязанных функций или операций, выполнимых над определенным классом объектов, которая удовлетворяет тем условием, что поведение этих объектов можно наблюдать лишь с помощью применения операций.
Под конкретным объектом какого-то абстрактного типа данных понимаем отдельный объект из указанного в определении абстрактного типа

1.2) Пусть утверждение доказано для последовательности из к путей.: Покажем справедливость утверждения для к И путей.
Имеем последовательность путей
[**** .СкЛ • * • Ока,ж-з. І аігк.і1[а1ід і
По предположении индукции тогда имеем, что существует вывод У, =?> со1Л уь оіл.х. , где у, - сокращенная метка уъ - сокращенная метка <4^., и иа & уг^ , ым , со,,», е 1ут>2т;)
Кроме того из условия знаем, что сокращенная метка аІІК равна уі и ~ вершина поддерева, над которым доминирует аііц . В силу того, что аЧк - нетерминальная веріина, по (І.Ї) пути [а4>к соответствует вывод
^ =Г> 0О^л V, .
Имеем: у, =*> со,(1 va слла =&■ Со,., Шіі1 у. шаЛ СЛ,Л ,
Если ПОЛОЖИМ £0Діі ЬО^, в С0Х «5
шл ,^е (2ТдОур‘)* ж значит V, зависит от V*
2) Обратно.
Пусть У, зависит от ух , т.е. имеется вывод
& (.ута у2Та Г). Покажем наличие последовательности путей индукцией по числу шагов вывода
2.1) Пусть в существует непосредственный вывод
V, =? 5 А V* ТОЛЬКО ВОЗМОЖНО, если В РТд имеется
правило у,-*^, что в свою очередь означает, что в Тй»'а есть дута из вершины «*, с сокращенной меткой vл в вершину С сокращенной меткой V* , Т.е. если В ТК'а шлее тс я путь [Ч(0+Л и <Хц- вершина поддерева, над которым доминирует .'