Детальная информация

Представлена реализация двух расширений реляционного программирования, полезных при разработке интерпретаторов: табличной мемоизации и конструктивного отрицания. Мемоизация позволяет эффективно обходить пространство состояний интерпретатора, а отрицание – проверять, что заданное состояние интерпретатора недостижимо. Полезность данных расширений продемонстрирована на примере интерпретатора для многопоточного императивного языка программирования.

These interpreters can execute a program, check that the program satisfies a set of constraints or generate a program that has specified properties. In order to take advantages of the relational interpreter, the developer needs to define the semantics of the programming language as a relation. In this work, we present an implementation of two useful extensions of relational programming: tabling and constructive negation. Tabling helps to traverse the state space of the interpreter efficiently. Constructive negation allows to check that some state of the interpreter is unreachable. We show how this extensioncan be used on an example of a relational interpreter for a concurrent imperative programming language.

Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление = St. Petersburg state polytechnical university journal. Computer science. Telecommunications and control systems: научное издание. Т. 11, № 2. — Электрон. текстовые дан. (1 файл : 12,5 Мб). — Санкт-Петербург: Изд-во Политехн. ун-та, 2018. — Загл. с титул. экрана. — Электронная версия печатной публикации. — Свободный доступ из сети Интернет (чтение, печать, копирование). — Текстовый документ. — Adobe Acrobat Reader 7.0. — <URL:http://elib.spbstu.ru/dl/2/j18-376.pdf>.