Абстрактные типы данных и частичная корректность программ тема диссертации и автореферата по ВАК РФ 01.01.10, кандидат физико-математических наук Менц, Хельмут

• Менц, Хельмут
• кандидат физико-математических наук
• 1984

Оглавление диссертации кандидат физико-математических наук Менц, Хельмут

ВВЕДЕНИЕ. .V.V.

ГЛАВА. I. Последовательности операций и Дерево вызовов

ГЛАВА 2. Вопрос о динамической допустимости операции 23 ГЛА.ВА. 3. Вопрос о частичной корректности программ

ГЛАВА. 4. Языковая реализация клетки

ГЛАВА. 5. Реализация алгоритма верификации . ШО

ГЛАВА. 6. Возможные дальнейшие работы

Введение диссертации (часть автореферата) на тему «Абстрактные типы данных и частичная корректность программ»

В последнее время в развитии программирования все большую роль играют усилия, направленные на повышение надежности программирования. В частности, становятся все важнее попытки повысить надежность программирования путем предоставления новых средств и форм описания данных (см., например [б] , [l9] , [23] , [24] , [28] , [Зб] , [45] ).Это вызвано, по крайней мере, следующими двумя причинами: 1. Становится все яснее, что "данные являются основным делом программ" [з?] в том смысле, что структура данных оказывает большое влияние на структуру обрабатывающих их программ.2. Однако, имеющиеся в традиционных языках программирования, как например ФОРТРАН, АЛГ0Л60, 1Ш/1, КОБОЛ и ПАСКАЛЬ, средства описания данных не дают возможность достаточно адекватно описать использующиеся и возникающие в реальных процессах данные.Из цели повышения надежности программирования при этом следует, что стоит задача создания таких средств описания данных, которые позволяли бы: 1. выражать в программе свойства реальных данных формально и по возможности полностью и естественным образом, 2, сосредоточить описание свойств определенного класса данных и допустимых способов реализации этих свойств в одном месте программы.Можно считать, что первым шагом для достижения- этой цели являлось введение различных конструкций класса (например " class " в СИМУЛА-67, "cluster" в CLU.), которые предоставляют возможность включить в описание данных рядом с описанием класса объектов и описания определенных для этих данных операций, то есть, описания процедур и функций, реализующих определенные над этими объектами операции. Но классы не позволяют объявить в явном виде соотношения между их операциями, взаимные зависимости этих операций. (например условия, при которых выполнение какой-то операции разрешено). Для них такие соотношения надо описать внутри определений самих операций, так что описание каждой операции выполняет две функции: 1. описываются действия, которые выполняет эта операция и 2. определяются условия, в которых разрешено выполнение этих действий, Необходимость описания условий применимости операций часто следует из того, что данные нельзя рассматривать как статистические, не подлежащие во время вьшолнения программы никаким (кроме модификации их значений) изменениям объекты.Данные программы обычно являются отражением реально существующих данных, как например картотекой рабочих какого-то завода или описания состояния автоматического станка во время изготовления какого-то изделия.Но реальные данные часто развиваются. Для описания состояния автоматического станка например развитие данных может выражаться в том, что в определенных состояниях, станка разрешены только такие операции, которые соответствуют разрешенным в данный момент процессам дальнейшей обработки изделия.Желательно, чтобы развитие реальных данных отражалось как можно точнее в данных программы. Есть притом надежда, что возможность, явно описать в определении данных условия для применения определенных для них операций, повысит наглядность этого описания и облегчает их использование. Кроме того можно надеяться, что такая возможность приведет к тому, что программист при определении данных лучше обдумывает вопросы соотношений между операциями.Явное описание условий применимости отдельных операций данных кроме того дает возможность проверки того, что эти условия соблюдаются программами, обрабатывающими эти данные. Такие (и похожие) соображения привели к возникновению понятия абстрактных типов данных. Мы, следуя Б, Лисков и Циллес [37] , под абстрактным типом данных понимаем группу взаимосвязанных функций или операций, выполнимых над определенным классом объектов, которая удовлетворяет тем условием, что поведение этих объектов можно наблюдать лишь с помощью применения операций.Под конкретным объектом какого-то абстрактного типа данных понимаем отдельный объект из указанного в определении абстрактного типа класса объектов, рассматриваемый вместе с определенными для него операциями и взаимосвязями между ними. При этом в дальнейшем всегда считается, что все эти операции выполняются над объектом, то есть, что результатом выполнения какой-то операции для какого-то объекта является тот же объект, но может быть с модифицированным значением.В последние годы были разработаны самые различные методы для описания взаимосвязей между операциями абстрактного типа данных.Следуя опять Б. Дисков и Циллес их можно разбивать в 5 групп: 1) Использование фиксированного круга формальных объектов (например использование графов [l9] ), 2) Использование подходящих, но произвольных формальных средств (например, можно использовать понятия теории множеств и разрешать определение и использование самых различных операций над множествами), 3) Использование модели машин состояния (" state motokitaevrtoole I "» смотри например [45] ), 4) Использование неявных определений с помощью аксиом (см. [24] , [52] , [53] ), 5) Использование неявных определений с помощью алгебраических соотношений (см. [2l] , [40] , [49] ).Предоставление, языковых средств для описания и верификации абстрактных типов данных является одной из.главных целей разработки языка программирования АL РН А R D (см. [59] ). Разработанные до сих пор средства описания и верификации абстрактных типов данных пригодны и полезны для обширного круга проблем. При их практическом применении в широких масштабах однако появляется следующее затруднение: Если попытаться выбрать средства формального описания так, чтобы их практическое применение не слишком затруднялось, чтобы получающееся описание осталось понятным для широкого круга программис'тов,'то как правило не удается провести полную формализацию описания. В МОделе машин состояния, например, часть свойств абстрактных типов данных обычно придется описать неформально.А если, с другой стороны, сосредоточить все внимание на предос-5тавление средств, позволяющих получить полное формальное описание абстрактного типа данных, то использующие эти средства описания обычно становятся такими абстрактными и сложными, что с ними могут справляться лишь опытные математики. Но такую высокую математическую культуру вряд ли можно ожидать(по крайней мере сегодня и в ближайшее время) от практического программиста.Кроме того оказывается, что автоматическая верификация программ до сих пор очень неэффективна. В. Турский например оценивает, что объем работы, необходимой ДЕ Я доказательства свойств какой-то программы на сегодняшнем уровне по меньшей мере на порядок величины больше, чем объем работы, затраченной на написание этой программы [б] .Из сказанного можно сделать вывод, что в области формализации описаний данных для достижения результатов, которые могли бы найти практическое применение уже сегодня и в ближайшем будущем, надо поставить себе не сразу цель полной формализации и верификации всех свойств данных, а надо попытаться приблизиться к этой цели шаг за шагом.Целью данной работы поэтому является выбор первого на этом пути шага, обоснование осмысленности этого выбора и опытная реализация выбранного шага.В первой главе работы в качестве первого шага предлагается фиксация в описании абстрактного типа данных всех последовательностей применений операций этого абстрактного типа данных, не приводящих к противоречиям со свойствами реальных данных, описанных в постановке задачи. Предлагается способ описания множества этих последовательностей.Во второй главе работы доказывается принципиальная возможность, решить во время выполнения какой-то программы вопрос.о том, разрешено ли в данный момент выполнение данной операции.В третьей главе показывается, при каких условиях возможна верификация программы относительно возникновения при произвольном ее выполнении вызова операции, не разрешенного в данном месте программы, В четвертой главе вводится расширение языка ПАСКАЛЬ, позволяющее использовать в этом языке введенные в первой главе средства опи-6сания Бзашюсвязей между операциятли данных.Пятая глава содержит краткое описание опытной реализации алгоритгла верификацш!» В шестой главе указьшаются некоторые возможности дальнейшего развития представленных идей.^ !•' Последовательность операций и дерево вызовов Попытаемся определить такие взаишсвязи между операциями данных, которые можно было бы формально описать и которые отражали бы важные свойства реальных данных в форме, понятной и естественной для практического програмлиста.Последовательность вызовов А * [ ] , не содержащая ни одного элемента, назовем пустой.2) Говорим, что последовательность вызовов операций абстрактного типа данных допустима для этого абстрактного типа данных (или допускается этим абстрактным типом данных), если этот абстрактный тип данных содержит хотя бы один объект, для которого все указанные в ней операции можно вызвать в порядке, заданном этой последовательностью, не нарушая при этом никакие из наложенных на операции взаимосвязей очередности. В противном случае говорим, что последовательность вызовов операций недопустима для этого абстрактного типа данных.или что она не допускается этим абстрактным типом данных.3) Все допустимые последовательности вызовов какого-то абстрактного типа данных образуют множество допустимых последовательностей вызовов этого абстрактного типа данных.Рассмотрим пример: Пример I : Требуется обрабатывать последовательный.набор данных, записи которого могут иметь типы TI, Т2 или ТЗ. Тип записи указан в ее первой позиции.Набор данных имеет следующую структуру: 1) Набор начинается неизвестным числом записей типа Т2, за группой которых обязательно следует одна запись типа TI.2) После первой группы записей следует неизвестное количество записей типа TI или Т2.3) Набор данных заканчивается записью типа ТЗ.

5) Говорим, что какая-то программа PROGi обрабатывает какой-то объект DATA абстрактного типа данных AftT , если тот определен (достзшен) для PR.06« и если в ней вызываются для DATA какие-то из определенных для Аьт операций. Рассмотрим теперь выполнение программы PROG» , обрабатывающей объект DATA абстрактного типа А&т . Этому выполнению программы соответствует конкретная последовательность вызовов операций - Ю для ЭАТА . Можно определить следующее понятие: Определение I. S: Говорим, что встречающийся при выполнении PRO6 вызов операции для объекта Л)АТА типа А ВТ динамически допускается в данный момент, или что он динамически допускается, если последовательность вызовов, получающаяся присоединением имени вызывающей операции к последовательности, образованной из имен уже выполненных для DATA операций, является начальной частью какой-то из допустимых последовательностей вызовов А в т . .Вернемся еще раз к рассмотрению программы PRos . Она по предположению без параллельной обработки. С другой стороны мы не ввели никаких средств для описания зависимостей между операциями различных абстрактных типов данных и даже различных объектов одного и того же абстрактного типа данных. Это означает, что мы считаем, что допустимости вызовов операций для различных объектов абстрактных типов данных не зависят друг от друга. Далее известно, что для каждой блоксхемы с одним входом и одним выходом и произвольной управляющей структзфы существует программа, образованная с использованием в качестве управляющих структур одних конструкций последовательности, разветвления и итерации, которая производит те же вычисления как и исходная блоксхема (см. [35] ). Поэтому мы в дальнейшем позволим себе считать, что все рассматривающиеся программы не содержат других управляющих конструкций кроме поюледовательности, разветвления и итерации,' Исходя из всего выше сказанного можно определить: Определение 1.4: 1) Последовательность, образованная из имен операций, вызывающихся при выполнении какой-то программы PR Об» для обрабатывающегося в ней объекта ВАТА абстрактного типа данных назовем последовательностью вызовов операций для DATA , соответствующей этому выполнению PR оft .2) Под псевдоуспешным выполнением программы PROS понимаем любое ее выполнение, которое а) кончится через конечное время и при котором -IIб) не возникают ошибки, препятствующие продолжению действий, предписанных текстом программы.3) Пусть в программе PR.OG> обрабатывается объект D A T A абстрактного типа данных Айт . Говорим тогда, что программа PROGi частично корректна относительно объекта DATA , если для DATA ни при каком псевдоуспешном ее выполнении не ьюгут возникатаь^^допустимые для А6Т последовательности вызовов.* 4) Говорим, что программа PRoft частично корректна, если она частично корректна относительно всех обрабатывающихся в ней объектов абстрактных типов данных.Из сказанного выше следует, что для достижения нашей цели надо найти способ для описания множества допустимых последовательностей вызовов абстрактного типа данных. При этом описание должно быть устроено так, чтобы для любой конкретной последовательности вызовов можно было определить, является ли она начальной частью какой-то из принадлежащих этому множеству последовательностей или нет.Если это удается, можно будет описать абстрактный тип данных определением Г) класса объектов, 2) множества операций, определенных над этим классом объектов и 3) множества допустимых последовательностей вызовов операций.Ясно, что описание множества допустимых последовательностей вызовов перечислением его элементов в общем случае не возможно. Поэтому надо искать другой способ описания, который удовлетворял бы нашим требованиям и был бы применим для описания множества допустимых последовательностей вызовов хотя бы для случаев, имеющих большое практическое значение.Все последовательности вызовов операций для объекта DATA , соответствующие псевдоуспешным выполнениям программы PROG. , можно построить по общей схеме, непосредственно получающейся из программы. Для этого вычеркиваются из программы все конструкции, не содержащие вызовы операций выбранного объекта D A T A И все условия в конструкциях разветвления и итерации. Таким образом получается схема, описывающая построение всех последовательностей вызовов операций исключительно конструкциями последовательности, разветвления и итерации.Факт, что последовательности вызовов операций, соответствзпющие какой-то программе, можно описать исключительно конструкциями последовательности, разветвления и итерации, приводит к мысли, что может оказаться возможным и целесообразным описать в определениях абстрактных типов данных множества допустимых для них последовательностей вызовов таким же способом. Этот способ описания множества допустимых последовательностей вызовов операций назовем описанием его путем задания схемы построения множества.Есть еще и другие поводы, приводящие к идее о целесообразности описания взаимосвязей между операциями данных, заданием схемы построения множества допустимых последовательностей вызовов операций.М.А. Джексон в своей книге "Принципы проектирования программ" [28] убедительно показывает, какое большое влияние структзфа данных оказывает на структуру обрабатывающих эти данные программ.При этом структура данных - это для Джексона не только структура объектов, служащих для хранения значений этих данных (как например массив или файл). Для него структура данных определяется главным образом взаимосвязями между отдельными процессами обработки данных, возможными последовательностями этих процессов. Он разработал средства, служащие одновременно для описания так понимаемой структуры данных и для описания структуры обрабатывающих эти данные программ. Кроме того Джексон в своей книге убедительно демонстрирует пригодность этих средств для описания данных и программ для решения обширного круга практических задач. Этими средствами как раз и являются конструкции последовательности, разветвления и итерации.Джексон убеждает читателей своей книги в том, что программы можно считать хорошо структурированными только тогда, когда их структура соответствует структуре (в понимании Джексона) обрабатывающихся в них данных и что такой метод стрзгктурирования программ в особенности облегчает их понимание и модификацию. Он демонстрирует методологию программирования, с помощью которой можно добиться достижения хорошей, структуры программ, получая при этом высокую степень згверенности в их правильности. Эта методология нашла уже довольно широкое распространение, в особенности для решения экономических и промышленных задач.Все это, вместе с тем, что понимание структуры данных Джексоном согласуется с нашей целью описания множества допустимых последовательностей вызовов абстрактного типа данных и служит еще раз подтверждением идеи возможности и целесообразности такого описания. Сверх этого результаты Джексона усиливают наши надежды на то, что наш подход к решению вопроса динамической допустимости вызова операций и к проверке частичной корректности программ является целесообразным. Итак, надо найти конкретный способ для описания схемы построения множества допустимых последовательностей вызовов абстрактного типа данных. Используем для этого (в модифицированной для наших целей форме) средства, разработанные Джексоном для описания структуры программ и данных.Это означает, что мы используем в качестве схемы построения множества допустимых последовательностей вызовов непосредственное описание общей струтстуры всех принадлежащих множеству последовательностей с помощью дерева, нетерминальные вершины которого соответствуют конструкциям последовательности, разветвления или итерации, а терминальные вершины - вызовам операций или поддеревьев данного дерева.Такое дерево в дальнейшем назовем деревом вызовов абстрактного типа данных.Допуская неточность, мы кроме того часто будем говорить о вершинах деревьев вызовов, как о конструкциях последовательности, разветвления, итерации, вызова поддерева и вызова операции, если этим вершинам соответствуют эти конструкции.Итак, ограничиваемся в дальнейшем рассмотрением множеств допустимых последовательностей вызовов, построение которых описывается каким-то деревом вызовов. Назовем эти множества множествами последовательностей вызовов, допускающихся деревом вызовов. Они определяются рекурсивно с помощью вершин этого дерева: Множество последовательностей вызовов, допускающихся деревом вызовов - это множество последовательностей вызовов, допускающихся корнем этого дерева.Множество последовательностей вызовов, допускающихся любым поддеревом какого-то дерева вызовов - это множество последовательностей вызовов, допускающихся корнем подцерева, т.е. вершиной доминирующей над этим поддеревом.Описываем теперь структзгру дерева вызовов вместе с правилами образования множеств последовательностей вызовов, допускающихся отдельными составными элементами этих деревьев.Следуя опять Джексону, для описания дерева вызовов при этом используем два варианта нотации, а именно: 1) Вербальную нотацию и 2) Нотацию с помощью диаграммы.Синтаксис средств вербальной нотации опишем формально, используя для этого предлагаемую Н. Виртом форму [58] , а средства описания с помощью диаграммы демонстрируем на примерах.Дерево вызовов абстрактного типа данных строится из элементов двух, типов, из вызовов и составных элементов дерева: элемент__дерева_вызовов = вызов ) составной_элемент_дерева__ __вызовов. составной_элемент_дерева_вызовов = Гимя_подцерева ":"] (последовательность 1 разветвление 1 итерация).Составные элементы дерева вызовов - это нетерминальные вершины дерева. Имя подцерева - это произвольное имя в понимании того языка программирования, на котором описывается абстрактный тип данных.Оно обозначает все подцерево корнем которого данная вершина является. Смысл остальных понятий объясняется ниже. вызов = вызов_операции \ вызов__поддерева.Вызовы - это терминальные вершины дерева. вызов_операции = имя_операции | " skip ".Уточнение понятия имени операции зависит от языка программирова-15ния, на котором описывается абстрактный тип данных.Множество последовательностей вызовов, допускающихся вершиной, являющейся вызовом операции, содержит единственная последовательность. Если вызов операции не равен " skip ", то эта последовательность в свою очередь состоит из единственного элемента, а именно из имени вызванной, операции. Если вызов операции равен " skip ", то последовательность должна быть пустая.Пример: Здесь и в остальных примерах дяя иллюстрации построения дерева вызовов используем операции, определенные Д Е Я данных из примера (I). Множество последовательностей, допускающихся утсазанными в примерах деревьями, обозначим через ^, Вербальная нотация: Раост^ Диаграмма: |pROCTi[ Тогда имеем: t » ^[РЯОСТ^]^ Определяем: вызов_поддерева = "ьиЬ " имя__подцерева.Множество последовательностей вызовов, допускающихся вершиной, являющейся вызовом поддерева, есть множество последовательностей вызовов, допускающихся вершиной, доминирующей над вызванным поддеревом, то есть над поддеревом, имя которого,з^азано в вызове.Рекурсивность вызовов поддеревьев допускается.Название "вызов поддерева" выбрано потоглу, что описанное правило эквивалентно получению дерева вызовов, в котором вместо вызова поддерева вставлена копия вызванного поддерева. При этом считаем, что до первой замены какого-то вызова вызванным поддеревом сняты копии ото всех поддеревьев, которые.где-то вызываются, и что эти копии сохраняются в неизменном виде. От этих первоначальных копий в дальнейшем и снимаются все те копии, которые вставляются в дерево вместо соответствующих вызовов поддеревьев.Множество последовательностей вызовов, допускающихся вершиной, являющейся конструкцией последовательности, получается конкатенацией всех множеств последовательностей вызовов, допускающихся элементами этой конструкции последовательности. Порядок конкатенации множеств определяется порядком следования соответствующих им элементов в последовательности.Пример: Вербальная нотация: SB а : &щ ркрстг ] REAPF еп&сс^ Диаграмма: Тогда имеем: ^ * {[PROCTI, REA4)F]J Определяем: разветвление = "seU(;t " ветвь [^"^г. " ветвь en. ье.1 . ветвь = элемент_дерева_вызовов.Множество последовательностей вызовов, допускающихся вершиной, являющейся разветвлением, получается объединением всех множеств последовательностей вызовов, допускающихся ветвями этого разветвления.Пример: Вербальная нотация: S£L: select PROLTA ОГ^ PROCJX enstl Диаграмма: Sit: btUcii [рЛОСТ-! 1 PROCTJ.Тогда имеем: ^ * {дР^остл}^ [РЯОСТХ]^ Определяем: итерация = *Ч te.r " тело__итерации "enittr ", тело итерации = элемент_дерева_вызовов.Пусть 61 - множество последовательностей вызовов, допускающихся телом итерации. Тогда множество последовательностей вызовов, допускающихся вершиной, являющейся итерацией, получается объединением множества, содержащего лишь пустую последовательность вызовов, со множествами 01 , QL^Oi , 0(.^OL&6t и т.д.Определение 1.5: , Вербальную нотацию дерева вызовов в дальнейшем назовем схемой вызовов, а нотацию с помощью диаграмм - диаграммой вызовов.Пример: Описанными средствами нельзя задавать множество И ] [PUSH] Jpi*SH,PUSH],...^ i:?ubH,.--,?asH] ^ n для конечного, но заранее не фиксированного п Можно лишь описать соответствующее бесконечное множество: [[], [PWbH],[Pu^ H,PuSH],..., [PUSH,...,PUSH],...^ п Такое снижение точности описания множеств допустимых последовательностей вызовов было предпринято с целью упрощения деревьев вызовов и в особенности облегчения решения вопросов динамической допустимости операции и частичной корректности программы. Мы считаем, что такое снижение точности может (по крайней мере в рамках данной работы) быть оправдано упрощением работы с описанными средствами и результирующим повышением эффективности верификации.Определение 1.6: Абстрактные типы данных, для которых взаимосвязи между их операциями описываются с помощью деревьев вызовов назовем клетками, а объекты этих типов - клетками данных, Итак, мы определили способ описания множеств допустимых последовательностей вызовов абстрактных типов данных, но мы пока не показали, что этот способ описания так выбран, что с его помощью можно 1) всегда решить вопрос о динамической допустимости операции и 2) показать частичную корректность программы.Займемся этими вопросами в следующих главах, —23— 2;' Вопрос о динагдической допустишсти операции Рассмотрим вопрос о динамической допусттюсти вызова операции для какой-то клетки данных в программе без параллельной обработки;^ Для 'х-аких программ вопрос о динаЕтческой допустишсти вызова операции сводится (как уже отмечено выше) к вопросу о том, является ли последовательность, получающаяся присоединением текущего вызова операции к последовательности уже выполненных для клетки данных операций, начальной частью какой-то допустимой последовательности вызовов типа этой клетки'данных.Говорим в частности, что цепочка вызовов допускается (не допускается) какой-то клеткой, если ею допускается (не допускается) соответствующая цепочке последовательность вызовов.Определение 2.2: Пусть дана клетка АВТ с диаграмглой вызовов. Построим по этой диаграьше вызовов разметку для непомеченного дерева Т, имещего ту же структуру что и она по следующим правилам: (1) Все нетерминальные вершины Т снабжаются метками, о(Зразованными конкатенацией имени поддерева, соответствующего вершине диаграммы, удлиненного суффиксом ^ или (если соответствующая вершина не имеет имени) пустой цепочки е с цепочкой символов bi^ , SELECT ИЛИ ITEK , в зависимости от того, является ли вершина диаграммы конструкцией последовательности, разветвления или итерации.Полз^енное таким образом помеченное дерево назовем деревом вызова ТЯд для клетки А. Пример: д|:5Еа 24Определение. 2,3; Пусть вершина какого-то дерева вызовов ТКд имеет метку А ^ В, Говорим об этой вершине, что ей соответствует конструкция последовательности, разветвления или итерации, вызов операции или вызов поддерева, если цепочка В равна sE(k , SELECT , ITER. , е или su.b соответственно.П)^получится из дерева Т1^д следующим образом: (Г) РТд содержит одно (и только одно) правило для каждой нетерминальной вершины дерева. (2) Правило, соответствующее какой-то нетерминальной вершине строится, исходя из метки этой вершины и из меток всех исходящих из нее дуг.Пусть символ поддерева, в метке вершины есть V , а метки дуг, выходящих из этой вершины W^ ^ Wj., ... , W^ t . (а) Если вершине соответствует последовательность, то получим правило; V -> W,, wi ... Wn где порядок следования меток VV^,WV,.-.WKX соответствует определенной вершиной последовательности. (б) Если вершине соответствует разветвление, то получим правило: (с) Если вершине соответствует итерация, то получим правило: (где е обозначает пустуто цепочку).

Заключение диссертации по теме «Математическое обеспечение вычислительных машин и систем», Менц, Хельмут

Заключение

Главная цель данной работы состояла в исследовании возможности разработки новых языковых средств для (хотя бы частичной) верификации программ, применение которых стало бы возможным для рядового программиста, использующего метод структурного программирования. Исходным пунктом прежде всего служил метод структурного программирования Джексона.

В работе достигнуты следующие главные результаты:

1) Введен новый способ определения абстрактных типов данных.

В этих типах, которые мы назвали клетками, вместе с указанием определенных для них операций указывается и множество допустимых последовательностей вызовов этих операций. Для описания множества допустимых последовательностей вызовов операций введено дерево вызовов операций.

2) Доказано, что с помощью дерева вызовов операций во время выполнения какой-то программы всегда можно решить вопрос о том, разрешено ли в данный момент выполнение данной операции.

3) Введено понятие частичной, корректности программы относительно какой-то. клетки данных, обрабатывающейся в этой программе и найдено достаточное условие этой частичной корректности.

4) Определено расширение языка программирования ПАСКАЛЬ, дающее возможность для определения клеток и проверки частичной корректности программ, написанных на этом расширении.

5") Реализованы алгоритм генерации внутреннего представления деревьев вызовов, исходя из их описания в виде схем вызовов и алгоритм проверки соответствия дерева вызовов программы дереву вызовов клетки данных. Реализация алгоритмов позволяет проверить частичную корректность программ относительно клеток данных, если только заданы схема вызовов программы и схема вызовов клетки данных.

Кроме того в работе указан общий подход к разработке программ для автоматической генерации деревьев вызовов программ и намечены первые идеи для использования деревьев вызовов для описания клеток данных, позволяющих их параллельную обработку.

Список литературы диссертационного исследования кандидат физико-математических наук Менц, Хельмут, 1984 год

1. Ахо А., Ульман Дж.: Теория синтаксического анализа, перевода и компиляции, т. I. Мир, М., 1978

2. Вирт Н.: Язык программирования Паскаль. Пересмотренное сообщение. Алгоритмы и организация решения экономических задач, выпуск 9. Статистика, М., 1977, стр.52-86

3. Гинзбург С.: Математическая теория контекстно-свободных языков. Мир, М., 1970

4. Дал У.И., Мюрхауг Б., Нюгорд К.: СИМУЛА-67. Универсальный язык программирования. Мир, М., 1969

5. Дал У.И., Дейкстра Э., Хоор К.: Структурное программирование. Мир, М., 1975'

6. Дейкстра Э.: Дисциплина программирования. Мир, М., 1978

7. Майерс Г.: Надежность программного обеспечения. Мир, М., 1980

8. ТурскийВ.: Методология программирования. Мир, М., 1981"

9. Харари Ф.: Теория графов. Мир, М., 1973

10. Кщенко Е.Л., Касаткина И.В.: Современные методы доказательства правильности программ. -Кибернетика, 1980, $ 6, стр.37-62

11. B£r, D.: Deduktive Prograrnmverifikation. Möglichkeitenund Probleme. Rechentechnik/Datenverarbeitung, 2. Beiheft 1976, S. 11 23

12. Bothe, K.: A Generalized Abstract Data Type Concept.

13. Humboldt-Universität zu Berlin, Preprint ITr. 3 (ITeue Folge), Berlin 1980

14. Brinch-Hansen, P.: Concurrent Pascal. A programming languagefor operating system design. Information Science Technical Report ITr. 10, April 1974

15. Campell, R. H.; Habermann, A. IT.: The specification of processsynchronization by path expressions. Lecture ITotes in Computer Science, vol. 16, Springer, Heidelberg 1974, pp. 69 - 102

16. Campell, R. H.; Kolstad, R. B.: An overview of Path Pascal'sdesign. ACM sigplaij Notices, vol. 15, ITr. 9 (Sept. 1980) pp. 13 - 14

17. Cowan, D^ D.; Graham, J. XI*; Welch, J. W.; Luc en a, C. J.P.:

18. A data-directed approach to program construction. Software-Practice and Experience, vol. 10, ITr. 5 (Kay 1930), pp. 355 - 372

19. Dijkstra, E. V,'.: The humble programmer. Comm. ACH, vol. 15,1.r. 10 (ITov. 1972), pp. 859 866

20. Dijkstra, E. XI.: Formal techniques and sizeable programs.1.cture llotes in Computer Science, vol. 14, Springer, Heidelberg .1976

21. Early, J.: Towards an understanding of data structures.

22. Comm. ACII, vol. 14, ITr. 10 (Oct. 1971), pp. 617 627

23. Endres, A.: Analyse und Verifikation von Programmen.

24. Systematische Verfahren und Untersuchungen zur Erstellung fehlerfreier Software. -R. Oldenbourg Verlag, München Wien, 1979

25. Guttag, J.U.; Horowitz, E.; Musser, D. R.: The design ofdata type specifications. Current trends in Programming Methodology, vol. IV (editor: Yeh, R.T.), Prentice Hall, Englewood Cliffs, 1978, pp. 60 - 79

26. Liskov, B.: Data access and program correctness.

27. ACS! SI GPL All Notices, vol. 10, Hr. 7 (July 1975), pp. 16 17

28. Liskov, 3.; Zilles, S.: An introduction to formal specifications of data abstractions. Current trends in Programming Methodology, vol. I (editor: Yell, R.T.), Prentice Hall, Englewood Cliffs, 1977, pp. 1 - 32

29. Liskov, B.; Snyder, A.; Atkinson, R.; Schaffort, C.:

30. Abstraction mechanisms in CLU. Comm. ACM, vol. 20, ITr. 8 (Aug. 1977), pp. 564 - 576

31. London, K. L.: Perspectives on program verification.

32. Current trends in Programming Methodology, vol. II (editor: Yell, R.T.), Prentice Hall, Englewood Cliffs, 1977, pp. 151 172

33. Uajster, II. E.: Limits of the "algebraic" specification ofabstract data types. ~ ACM SIGPLAIT Hotices, vol. 12, Hr. 10 (Oct. 1977), pp. 37 42

34. Manna, Z.; Yfaldinger, R. : The logic of computer programming.

35. EE Transactions on Software Engineering, vol. SE-4, Hr. 3 (1978)

36. IToonan, R. E.: Structured programming and formal specification.

37. University of Maryland, Technical Report TR-372, April 1975

38. Hordstrüm, B.: Programming with abstract data types.

39. University of UineS (Sweden), Report UMIIIF-63-78

40. Parnas,D. L.: On the criteria to be used in decomposing - — systems into moduls. - Com. ACI.I, vol. 15,

41. Hr. 12 (Dec. 1972), pp. 1053 1058

42. Paraas,D. L. : A technique for software module specificationwith examples. ~ Comm. ACI.I, vol. 15, Hr. 5 (Kay 1975), pp. 330 336

43. Parnas,D. L.; Shore, J. E. ; Y/eiss, D.: Abstract types defined----------------------as classes of variables. ACI.I SIGPLAIT Hotices,vol. 11 (1976), Special issue: Proceedings of Conference on Data, pp. 149 154

44. Guttag, J. 5 U.: Botes on Type abstraction. Lecture Hot esin Computer Science, ITr. 69, Springer, Heidelberg, 1979

45. Hoare, С.Л.Н.: Proof of correctness of data representations. ~

46. Acta Informatics, vol. 1, Hr. 4 (1972), pp. 271 281

47. Hoare, C.A.R.: Hints on Programming Language Design.

48. Stanford HELIO AIH-224, October 1973

49. Horning, J. J.ï Some desirable properties of data abstractionfacilities. АСЫ SIGPLAIT Iïotices, vol. 11 (1976), Special issue: Proceedings of Conference on Data, pp. 60 - 62

50. Igarashi, S.; London, R.L. ; Luckham, D.C.: Automatic Program

51. Verification I: A logical basis and its implementation. ~ Acta Informática, vol. 4, pp. 145 182 (1975)

52. Jackson, 1!. A.: Principles of program design.

53. Academic Press, London, 1975

54. Jackson, II. A.: Constructive methods of program design.1.cture Ilotes in Computer Science, ÏTr. 44, Springer, Heidelberg, 1976, pp. 236 262

55. Jackson, II. A.; Information systems: Modelling, sequencingand transformations. Proceedings 3rd International Conference on Software Engineering, May 10-12, 1978. Atlanta, Georgia, USA, pp. 72 - 81

56. Jones, A.K.; Liskov, Б.Н.: A language extension for expressing;constraints on data access. Comm. ACI.l, vol. 21 , Hr. 5 (May 1978), pp. 353 - 367

57. Kamin, S.: Some definitions for algebraic data typespecifications. ACM' SIGPLAIT ITotices, vol. 14, Hr. 3 (March 1979), pp. 28 - 37

58. Kolstad, R. В.; Campell, R. H.: Path Pascal user manual.

59. ACM SIGPLAIT notices, vol. 15, Hr. 9 (Sept. 1980), pp. 15 24

60. Knuth, D. E.: Structured programming with goto statements.

61. Current trends in Programming Methodology, vol. 1 (editor: Yeh, R.T.), Prentice Hall, Englev/ood Cliffs, 1977, pp. 140 194

62. Lingner, R.C.; Mills, H.D.: On the development of largereliable programs, Current trends in Progranmiing Methodology, vol. I (editor: Yeh,R.T. Prentice Hall, Englewood Cliffs, 1977, pp. 120 - 139

63. Reference manual for the Ada programming language. Proposedstandard document. United States Department of Defense, July 198049. Reichel50. Rice, II.51)1. Shaw, II.

64. H. ; Rupbach, U. L. ; Kaphengst, Ii.: Initiale algebraische Spezifikation von Datentypen, parametri-sierte Datentypen und Algorithmen. -Wissenschaftliche Informationen und Berichte 15« V2B R0B0TR0ÏT ZFT, Dresden, 19S0

65. Recursion and Iteration. Comm. ACI.1, vol. 8,

66. Hr. 2 (Febr. 1965), pp. 114 115

67. Research directions in abstract data structures.

68. SIGPLAIT ITotices, vol. 11 (1916), Special issue: Proceedings of Conference on Data, pp. 66 6352)

69. Spitzen, J.; Wegbreit, В.: The verification and synthesis ofdata structures. Acta Informatics, vol. 4 (1975), PP. 127 - 14453. Standish.1. T.54. S toy an, II.:55. Tanenbaum, A56. ïïirth, IT.:57. Wirt h, IT.:58. Wirt h, IT.:

70. A.: Data structures An axiomatic approach. -Current trends in Programming methodology, vol. IV (editor: Yeh, R.T.), Prentice Hall, Englewoocl Cliffs, 1978, pp. 30 - 60

71. S. : In defense of program testing or correctness proof considered harmful. ACII SIGPLAIT ITotices, vol. 11, ITr. 5 (Hay 1976), pp. 64 - 68

72. On the design of programming languages. -Information Processing 74, pp. 386 3931.odula: A language for modular multiprogramming. Software- Practice and Experience, vol. 7, ITr. 1 (1977), pp. 3-35

73. What can we do about the unecessary diversity of notation for syntactic definitions? -Coram. ACI.I, vol. 20, ITr. 11 (ITov. 1977), pp. 822 823

74. Wulf, XI. A,; London, R.L. ; Shaw, I.i. : An introduction to theconstruction and verification of Alpliard programs. IEEE Transactions on Software Engineering, vol. SE-2, ITr. 4 (Dec. 1976), pp. 253 - 265fUL