Бабичев А.В. Распознавание и спецификация структур данных

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

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

В настоящей работе предлагается следующий подход к разрешению сложившийся тупиковой ситуации. Описывается формальный язык и две возможные интерпретации этого языка (две формальные теории, основанные на одном и том же языке): жесткая интерпретация и мягкая интерпретация одного и того же формального языка. При мягкой интерпретации можно осуществить проверку непротиворечивости, но язык обладает слабыми выразительными способностями (тем не менее, он при этом более выразителен, чем современные средства спецификации). А жесткая интерпретация хотя и порождает неразрешимую теорию (теорию с неразрешимой проблемой выполнимости), но обладает следующими ценными свойствами:

1. по любому описанию можно автоматически построить программу, которая допускает ровно те графы, которые соответствуют описанию;

2. выразительные возможности языка спецификаций при жесткой интерпретации довольно высоки (например, на нем можно совершенно точно описать, что такое двунаправленный список).

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

На рисунке 2 представлена схема информационных зависимостей между разделами.

Кратчайшая последовательность для освоения основного теоретического результата (раздел 4.3) помечена на рисунке жирными стрелками.

В главе 1 рассматривается три способа формального представления понятия "структура данных":

Три способа формального представления структур данных потребовались по следующим причинам. При распознавании структур данных (при использовании формализма итерационных и объектно-ориентированных автоматов в главах 3 и 4) используется формализм функциональных схем. В то же время для спецификации типов даных используется более приближенный к реальным структурам данных конечно-автоматный формализм (исключением является описываемый в разделе 2.1 язык спецификации итерационных типов, который использует формализм функциональных схем). Именно из-за того, что распознавание происходит на уровне схем, а спецификация – на уровне автоматов, в разделе 1.2 так много внимания уделено вопросу перевода с автоматного уровня на схемный.

То, что потребовалось два разных конечно-автоматных представления, связано с тем, что конечные автоматы используются в дальнейшем не только в формальном языке спецификации (глава 2), но и как элементы области интерпретации этого языка. При этом использование раскрашенных автоматов в качестве элементов области интерпретации приводит к созданию жесткой теории (жесткой интерпретации языка спецификаций). В то же время использование раскрашенных автоматов Мура в качестве элементов области интерпретации приводит к созданию языка, в котором проблема непротиворечивости спецификации разрешима...

Об авторе

Кандидат технических наук, старший научный сотрудник. В 1976 г. закончил МИИТ по специальности "прикладная математика". С тех пор работает в Институте проблем управления РАН. Кандидатская диссертация (1982) посвящена вопросам организации беспереборного синтаксического анализа контекстно-свободных языков.

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

В настоящее время занимается вопросами создания логического языка спецификации технических конструкций.

В качестве разработчика участвовал в крупных проектах по созданию компиляторов (Fortran77, Pascal, С/С++ , Prolog), систем тестирования/верификации, систем моделирования и систем резервного копирования данных.