Formal proof of the semantic equivalence between the core of the AOP language AspectTalk and the OOP language smalltalk.pdf Язык аспектно-ориентированного программирования (АОП) AspectTalk [1] разработанс целью создания защищённых систем обработки информации. На нём могутбыть реализованы информационная система и политика её безопасности, а также осуществленаих интеграция с помощью соединительных модулей [2]. Основой этой технологииявляется возможность создания с помощью АОП дополнительных модулейи интеграции их с программой без изменения её исходного текста [3]. Согласно [4],всякий язык АОП L является надмножеством (расширением) некоторого языка программирования,не являющегося языком АОП и называемого далее ядром языка L.Ядро языка AspectTalk, по замыслу его автора, построено как язык объектно-ориентированногопрограммирования (ООП). В данной работе даётся формальное доказательствосемантической эквивалентности ядра языка АОП AspectTalk и языка ООПSmalltalk 80 [5]. Тем самым, в частности, формально доказывается, что ядро языкаAspectTalk является действительно языком ООП.Основными компонентами определения языка программирования являются егосинтаксис и семантика. Синтаксис задаётся с помощью формы Бэкуса-Наура (БНФ)или расширенной БНФ (РБНФ) [6]. Денотационное описание семантики (ДОС) [7] -один из способов формального описания семантики языков программирования, которыйсостоит в задании тройки объектов: 1) множеств, определяемых системой уравненийна моноиде слов в алфавите языка и называемых синтаксическими областями;2) совокупности множеств, являющихся непрерывными решётками и называемых множествамисемантических объектов, или доменами [8]; 3) множества функций, являющихсяотображениями из синтаксических областей в домены, называемого множествомсемантических отображений.В [9] семантическая эквивалентность языков программирования определена каккоммутативность диаграммы, в которой объектами являются множества синтаксическихобластей и множества доменов, а стрелками - гомоморфизмы между этими множествами.Аналогичным образом семантическая эквивалентность ядра языка АОПAspectTalk и языка Smalltalk доказана коммутативностью диаграммы на рис. 1, гдеA - ядро языка АОП AspectTalk, B -язык Smalltalk, SynX -множество синтаксическихобластей языка X , Semx -множество доменов языка X .Syn^ SynB41 2Рис. 1. Диаграмма семантической эквивалентности языков A и BГомоморфизымы 1 и 2 -это множества семантических отображений ДОС языковA и B соответственно. ДОС ядра языка AspectTalk построено на основе [10], ДОСязыка Smalltalk позаимствовано из работы [11]. Гомоморфизмы 3 и 4 определяютсяправилами трансляции одного языка в другой, 5 и 6 являются гомоморфизмами нанепрерывных решётках. Заметим, что в [9] в качестве языков A и B рассматриваютсявысокоуровневый язык программирования и машинный язык соответственно иставится вопрос о корректности трансляции одного в другой. Поскольку задача восстановленияисходного текста программы не всегда имеет решение, гомоморфизм 4отсутствует на диаграммах в [9].Доказательство семантической эквивалентности ядра языка AspectTalk и языкаSmalltalk позволяет использовать все принципы ООП, разработанные для Smalltalk,в программировании на AspectTalk. Более того, возможна автоматическая трансляцияпрограмм с языка Smalltalk в AspectTalk и обратно.

Скачать электронную версию публикации