Preview

Russian Technological Journal

Расширенный поиск

Эквивалентность схем программ на основе алгебраического подхода к заданию семантики языков программирования

https://doi.org/10.32362/2500-316X-2022-10-1-18-27

Полный текст:

Аннотация

Цели. Статья посвящена вопросам эквивалентности схем программ. В соответствии с работами А.А. Ляпунова и Ю.И. Янова – основоположников данной теории, под схемой программы понимается ее модель, в которой осуществляется абстрагирование от содержательных значений операторов и выражений. При этом неизменной остается структура программы, включающая символические обозначения операторов и выражений при сохранении последовательности их выполнения. Представленная в статье модель языка программирования содержит основные конструкции последовательных языков и является ядром имеющихся языков последовательного программирования. Цель работы – разработка эффективного алгоритма исследования вопросов эквивалентности (неэквивалентности) схем программ последовательных языков программирования.
Методы. Используется алгебраический подход к заданию семантики языков программирования для исследования вопросов эквивалентности схем программ.
Результаты. Предложен новый алгебраический подход к заданию формальной семантики языков последовательного программирования – процессная семантика. Процессная семантика задается посредством сопоставления программам (схемам программ) множества вычислительных последовательностей. Под вычислительной последовательностью понимается последовательность выполнения действий (команд и тестов) программы. На введенной семантической области (множестве вычислительных последовательностей) определены операции конкатенации двух видов (тест-команда и команда-команда) и операция объединения, свойства которых заданы системами аксиом. Доказана конечность представления семантических значений в виде систем рекурсивных уравнений. Предложен алгоритм доказательства эквивалентности (неэквивалентности) систем рекурсивных уравнений, характеризующих семантические значения для пары схем программ, откуда вытекает эквивалентность (неэквивалентности) программ в сильном смысле.
Выводы. Показана эффективность применения предложенного алгоритма для доказательства эквивалентности схем последовательных программ, в которых отсутствует побочный эффект при вычислении выражений, т.е. последовательное вычисление выражения более, чем один раз, ничего не меняет. В статье приведен демонстрационный пример доказательства эквивалентности схем программ двумя методами: известным методом индукции фиксированной точки де Баккера – Скотта и предложенным в статье методом. Сравнение приведенных методов свидетельствует не только об эффективности нового метода, но и его существенной простоте, что было подтверждено на практике при выполнении соответствующих заданий студентами специальности «Прикладная математика и информатика» Национального исследовательского университета МЭИ в процессе изучения дисциплины «Семантика языков программирования».

Об авторе

Ю. П. Кораблин
НИУ МЭИ
Россия

Кораблин Юрий Прокофьевич, д.т.н., профессор, профессор кафедры прикладной математики и искусственного интеллекта Института информационных и вычислительных технологий
Scopus Author ID 6603265252 

111250, Россия, Москва, Красноказарменная ул., д. 14



Список литературы

1. Кораблин Ю.П., Куликова Н.Л., Шипов А.А. Программы как минимальные фиксированные точки: теоретические и прикладные аспекты. Cloud of Science. 2020;7(3):535−550.

2. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург; 2010. 610 с. ISBN 978-5-9775-0404-1

3. Кораблин Ю.П., Кучугуров И.В. Процессная семантика языков распределенного программирования. Программные продукты и системы. 2011;4(96):57−64.

4. Кораблин Ю.П. Семантические методы анализа программ. М.: Изд-во МЭИ; 2019. 68 с. ISBN 978-5-7046-2173-7

5. Floyd R.W. Assigning Meanings to Programs. In: Colburn T.R., Fetzer J.H., Rankin T.L. (Eds.). Program Verification. Studies in Cognitive Systems. Dordrecht: Springer; 1993. V. 14. P. 65−81. https://doi.org/10.1007/978-94-011-1793-7_4

6. Hoare C.A.R., Wirth N. An axiomatic definition of the programming language PASCAL. Acta Informatica. 1973;2(4):335−355. https://doi.org/10.1007/BF00289504

7. Stoy J.E. Denotational semantics: The Scott-Strachey approach to programming language theory. Cambridge: The MIT Press Series in Computer Science; 1985. 414 p.

8. Алагич С., Арбиб M. Проектирование корректных структурированных программ: пер. с англ. M.: Радио и связь; 1984. 264 с.

9. de Bakker J. Mathematical Theory of Program Correctness. Prentice Hall International; 1980. 505 p.

10. Захаров В.А. Моделирование и анализ поведения последовательных реагирующих программ. Труды Института системного программирования РАН. 2015:27(2):221−250. https://doi.org/10.15514/ISPRAS2015-27(2)-13

11. Захаров В.А., Подымов В.В. Применение алгоритмов проверки эквивалентности для оптимизации программ. Труды Института системного программирования РАН. 2015;27(4):145−174. https://doi.org/10.15514/ISPRAS-2015-27(4)-8

12. Захаров В.А., Жайлауова Ш.Р. О задаче минимизации последовательных программ. Моделирование и анализ информационных систем. 2017;24(7):415−433. https://doi.org/10.18255/1818-1015-2017-4-415-433

13. Молчанов А.Э. Разрешимость проблемы эквивалентных преобразований в классе примитивных схем программ. Труды Института системного программирования РАН. 2015;27(2):173−188. https://doi.org/10.15514/ISPRAS-2015-27(2)-11

14. Кораблин Ю.П., Шипов А.А. Верификация моделей систем на базе эквациональной характеристики формул CTL. Программные продукты и системы. 2019;32(4):547−555. http://dx.doi.org/10.15827/0236-235X.128.547-555


  • Предложен алгебраический метод, задающий процессную семантику программ. Семантика сопоставляет программам в качестве семантических значений множество вычислительных последовательностей или путей выполнения программы.
  • Доказана возможность представления семантических значений схем программ в виде конечных систем рекурсивных уравнений.
  • Предложен эффективный алгоритм анализа эквивалентности/неэквивалентности полученных систем рекурсивных уравнений.

Рецензия

Для цитирования:


Кораблин Ю.П. Эквивалентность схем программ на основе алгебраического подхода к заданию семантики языков программирования. Russian Technological Journal. 2022;10(1):18-27. https://doi.org/10.32362/2500-316X-2022-10-1-18-27

For citation:


Korablin Y.P. Equivalence of the schemes of programs based on the algebraic approach to setting the semantics of programming languages. Russian Technological Journal. 2022;10(1):18-27. https://doi.org/10.32362/2500-316X-2022-10-1-18-27

Просмотров: 78


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2782-3210 (Print)
ISSN 2500-316X (Online)