Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024)

Ссылки сюда (1) →

Короткая ссылка: 20240629R

Докладчик

Александр Дельман

Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.

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

Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; в дальнейшем в проект добавились результаты также нескольких курсовых работ.

Видео

on youtube

Презентация

Thesis

• https://github.com/OnionGrief/Chipollino

Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.

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

Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; в дальнейшем в проект добавились результаты также нескольких курсовых работ.

Основные требования, предъявляемые к разработке:

наглядность

— результаты преобразований должны быть представлены в понятной пользователю форме.

Для решения этой задачи в качестве базового представления сущностей был выбран язык LaTeX и библиотека «Tikz» для отрисовки автоматов. Эти средства наиболее выразительны, и из LaTeX-формата нетрудно извлечь более простые посредством упрощающих гомоморфизмов.

расширяемость

— интерфейс должен быть достаточно удобен для пополнения новыми функциями и типами автоматов или других представлений формальных языков. Для решения этой задачи конвертер был спроектирован таким образом, чтобы модули синтаксического разбора, проверки типов и логирования допускали обновления посредством автоматического порождения необходимого кода (исключая «рабский труд» по написанию шаблонного кода).

связность

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

Экосистема проекта

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

Сам конвертер написан на языках C++} (большая часть фронтенда и весь бэкенд) и Refal-5 (форматирующие скрипты для порождения \LaTeX-исходников). В связи с этим, отдельно стоит упомянуть экспериментальный проект Линтера для Refal-5, который служит цели улучшить дисциплину кода, ранее не контролировавшуюся никем, кроме самого разработчика, делающего коммиты, и находится на стадии встраивания в «CI» проекта.

Применение в исследованиях

Хотя изначально конвертер разрабатывался как чисто учебный проект, оказалось, что этот инструмент удобен и для теоретических исследований. В частности, посредством метода Verify удобно перепроверять утверждения на предмет неявных допущений, что показал анализ статьи , выявивший несколько неточностей в приведённых формулировках. Кроме того, методы анализа полугрупповых структур показали хорошую скорость и точность при выявлений «REDoS»-ситуаций в академических регулярных выражениях с перекрытиями в подвыражениях, для которых методы анализа, использующие самопересечения автоматов , работают слишком медленно, а фаззеры, — ненадёжно. Последним применением конвертера на данный момент стало исследование бисимуляций в конечных автоматах с памятью посредством аппроксимаций классическими конечными автоматами. Поставленная цель — сделать осязаемыми абстрактные концепции, используемые в современной теории формальных языков, — оказалась полезна не только для сдачи зачётов, но и для испытания новых гипотез.