ПРОГРАММИРОВАНИЕ, 2009, Ml, с. 50-60
■ ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
ОПЕРАЦИОННО-ОНТОЛОГИЧЕСКИЙ ПОДХОД К ФОРМАЛЬНОЙ СПЕЦИФИКАЦИИ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ*
© 2009 г. И. С. Ануреев
Институт систем информатики СО РАН 630090 Новосибирск, пр. Лаврентьева, 6 E-mail: anureev@iis.nsk.su Поступила в редакцию 21.04.2008 г.
Создание формальных спецификаций языков программирования - актульная задача теории и практики программирования. В работе представлен операционно-онтологический подход к формальной спецификации языков программирования. Он включает формализм для задания операционно-онтологической семантики языков программирования - онтологические системы переходов, язык описания онтологических систем переходов OTSL и методологию применения языка OTSL к разработке формальных спецификаций языков программирования.
1. ВВЕДЕНИЕ
Самый распространенный способ получения информации о семантике языков программирования - спецификации на естественном языке. Особенностью таких спецификаций является использование неявной системы понятий и категорий (концептуального окружения), которое позволяет сделать спецификации обозримыми и емкими в смысловом аспекте за счет перенесения части смысла на уровень терминов и обозначений, требуя при этом от читателя в процессе чтения спецификаций распознавания и адекватного понимания смысла понятий и категорий, входящих в концептуальное окружение.
Однако такие спецификации могут быть двусмысленными и неполными как из-за их естественно-языковой природы, так и из-за неполного распознавания и/или неточной интерпретации концептуального окружения. Поэтому важное значение приобретает разработка формальных спецификаций языков программирования, которые обеспечивали бы математическую строгость описаний и унифицированный
*Это исследование частично поддержано грантами РФФИ 06-01-00464-а и 08-01-00899-а.
формат для концептуального окружения, позволяющий явно определять, какие понятия и категории входят в концептуальную систему, и фиксировать их смысл.
Если провести анализ неформальных спецификаций, описывающих динамическую семантику языков программирования, то практически во всех таких спецификациях в основе лежит некий пошаговый абстрактный вычислитель (абстрактная машина), который оперирует явно или неявно терминами состояния и перехода из состояния в состояние. Такой подход к описанию семантики называется операционным, а сама семантика - операционной семантикой. Более того, сложные взаимосвязи на уровне статической семантики в современных языках программирования требуют использования операционных (алгоритмических) описаний уже на этом уровне.
С учетом сказанного, можно сделать вывод, что операционная семантика является наиболее естественным кандидатом на роль универсальной формальной спецификации языков программирования. Еще один факт, подтверждающий этот вывод, состоит в том, что число языков, для которых (или их существенных подмножеств) имеется формальная операционная
семантика, превалирует над числом языков, семантика которых основана на других подходах (денотационный, аксиоматический и т. д.).
Операционная семантика обычно использует известный универсальный формализм - системы переходов. Общий метод применения систем переходов к разработке формальной семантики языков программирования - метод структурной операционной семантики - был предложен Гордоном Плоткином в его работе [1].
Этот формализм обеспечивает математическую строгость описания языка программирования. Однако он не решает проблему моделирования его (языка) концептуального окружения.
Логико-алгебраический подход к решению этой проблемы был предложен Юрием Гуреви-чем. Он основывается на машинах абстрактных состоянии [2,3]- обобщении систем переходов за счет использования в качестве состояний произвольных алгебр. Выбор подходящей алгебры при спецификации языка программирования позволяет в какой-то степени решать проблему моделирования концептуального окружения этого языка.
Наш подход к решению этой проблемы основан на спецификации концептуального окружения с помощью онтологии. Мы представляем новый вид семантики - операционно-онтологи-ческую семантику, которая описывает в едином контексте онтологию языка программирования и его операционную семантику. Как формализм задания операционно-онтологической семантики мы используем онтологические системы переходов (далее ОТ-системы) - обобщение систем переходов за счет накладывания онтологической структуры на состояния систем переходов.
В работе представлены основные определения, связанные с ОТ-системами (раздел 3), основы языка описания ОТ-систем ОТЯГ (раздел 4) и методология применения ОТЯГ к формальной спецификации языков программирования (раздел 5). Соглашения и обозначения, используемые в работе, собраны в разделе 2.
2. СОГЛАШЕНИЯ И ОБОЗНАЧЕНИЯ
Условимся начинать обозначения множеств с прописной буквы, а их элементы обозначать также как множества, но начиная с заглавной
буквы и, возможно, добавляя индексы, штрихи и т. п. Например, re - множество отношений, Re, Re', Rei - конкретные отношения из re.
Пусть х —т- у, х —т-р у, х X у, bo, _L обозначают множество тотальных функций из х в у, множество частичных функций из х в у, декартово произведение множеств х и у, булевское множество {true, false} и неопределенное значение, соответственно.
Как обычно, х —т- у —т- z - сокращение для х (у z).
Пусть upd(f, (Ai,... , Ап), е) обозначает функцию f' такую, что
f'(Ai)...(An) = е
и f'(Bi)... (Bn) = f (Bi)... (Вга) в случае, если CBi. . , BJ ф (Ai,. . . , AJ.
Пусть X(Yi Zi,..., Yn Zn) обозначает результат замены в синтаксической конструкции X всех (свободных) вхождений Yi,... , Yn на синтаксические конструкции Z\,... , Zn, соответственно.
Пусть X [Y] q обозначает результат подстановки синтаксической конструкции Y в позицию q синтаксической конструкции X.
Условимся обрамлять сквозные примеры структурными скобками
ExW[текст примера]Ех, где N - номер примера.
3. ОНТОЛОГИЧЕСКИЕ СИСТЕМЫ ПЕРЕХОДОВ
В этом разделе определяется понятие ОТ-системы и вводится связанная с ним терминология.
3.1. Определение ОТ-систем
Онтологическая система переходов Ots включает:
1. Множество состояний st.
2. Множество переходов tr.
3. Функцию означивания переходов
TrVal G tr —т- st X st —т- bo.
Свойство TrVal (Tr) (St, St') (далее обозначаемое Tr(St, St')) означает, что имеется переход
с именем Тг из состояния St в состояние Б!;'. Пара состояний (Б!;, Б!;') называется экземпляром перехода Тг в состоянии БЪ, если Тг(31;, St/)• Множество экземпляров перехода Тг в состоянии St называется значением перехода Тг в состоянии Б!;. Дополнительно функция означивания переходов определяет, какие переходы возможны в текущем состоянии. Переход Тг возможен в состоянии БЪ, если его значение в состоянии St непусто.
4. Множество понятий со.
5. Множество отношений ге.
6. Множество объектов оЬ.
7. Функцию означивания понятий Со¥а1 вида st —т- со —т-р оЬ —т- Ьо. Значение (содержимое) Со (Б!;) понятия Со в состоянии St определяется как СоУаКЗ!;). Объект ОЬ называется экземпляром понятия Со в состоянии БЪ, если Со(31;)(0Ь). Дополнительно функция означивания определяет, какие понятия существуют в состоянии Б!;. Понятие Со существует в состоянии БЪ, если Со (Б!;) ф _1_. Понятия, существующие в состоянии БЪ, называются реальными понятиями в состоянии Б!;. Понятия, которые не существуют в состоянии БЪ, называются потенциальными понятиями в состоянии Б!;.
8. Функцию означивания отношений ИвУа!
вида st
ге
ob X ob —т- Ьо. Значение
1. Выделение функции означивания объектов 0Ь¥а1 вида st —> оЬ —>р оЬ. Эта функция задает семантику объектов. Значение 0Ь(31;) объекта ОЬ в состоянии St определяется как 0Ь¥а1 (3"Ь) (ОЬ). Дополнительно функция означивания объектов определяет, какие объекты существуют в текущем состоянии. Объект ОЬ существует в состоянии БЪ, если 0Ь(31;) ф _1_. Объекты, существующие в состоянии БЪ, называются реальными объектами в состоянии Б!;. Объекты, которые не существуют в состоянии БЪ, называются потенциальными объектами в состоянии Б!;.
2. Разбиение множества объектов оЬ на два непересекающихся множества - множество атомарных объектов аОЬ и множество составных объектов сОЬ. Атомарные объекты не имеют внутренней структуры. Их семантика задается внешними связями с другими атомарными объектами. Разбиение позволяет рассматривать сложные структуры как (составные) объекты. Таким образом, понятия, например, могут определяться на последовательностях объектов.
3. Выделение множества объектных ссылок оЬБ^ и функции означивания объектных ссылок 0Ы1е:С¥а1 вида
st —т- obRef
ob.
(содержимое) Re(St) отношения Re в состоянии St определяется как ReVal(St). Пара объектов (Ob, Ob') называется экземпляром отношения Re в состоянии St, если
Re(St)(Ob, Ob').
Дополнительно это семейство определяет, какие отношения существуют в состоянии St. Отношение Re существует в состоянии St, если Re(St) ф _L. Отношения, существующие в состоянии St, называются реальными отношениями в состоянии St. Отношения, которые не существуют в состоянии St, называются потенциальными отношениями в состоянии St.
3.2. Варианты ОТ-систем
Варианты ОТ-систем - это ОТ-системы с дополнительными характеризациями. Выделим характеризации ОТ-систем, образующие базис для построения вариантов ОТ-систем (различные комбинации характеризаций соответствуют различным вариантам ОТ-систем):
Значение 0Ы1е:1:(3^ объектной ссылки 0ЬЯе± в состоянии St определяется как 0Ы1е:1:¥а1(3^ (0ЬЯе±). Объектные ссылки используются, чтобы ссылаться на объекты.
4. Разбиение множества понятий со на два непересекающихся множества - множество атомарных понятий аСо и множество составных понятий сСо.
5. Выделение среди понятий множества предопределенных понятий ргеСо. Предопределенные понятия - это понятия с предопределенным значением. Предопределенные понятия являются реальными в любом состоянии.
6. Разбиение множества отношений ге на два непересекающихся множества - множество атомарных отношений aRe и множество составных отношений cRe.
7. Выделение с
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.