Semantic Spec Compilation (SSC): взгляд на компиляцию человеко-ориентированных Markdown-спецификаций

Страницы:  1

Ответить
 

Professor Seleznov


Современная разработка программного обеспечения по-прежнему сталкивается с устойчивым разрывом между тем, как человек описывает намерение системы, и тем, как это намерение затем становится машинно-исполняемой логикой. Требования, проектные решения, ограничения, бизнес-правила и примеры ожидаемого поведения чаще всего существуют отдельно от исходного кода. Даже при достаточно дисциплинированном процессе разработки документация со временем может терять связь с реализацией, тогда как код остаётся исполняемым, но не всегда выражает предметный смысл системы в явном и проверяемом виде.
Классическим ответом на эту проблему стали формальные методы и формальные языки спецификаций. Они позволяют описывать систему строго, проверяемо и пригодно для анализа. Однако такая строгость требует от разработчика специальной подготовки и готовности работать в заранее заданной формальной системе. В повседневной инженерной практике значительная часть знания о системе сначала фиксируется не в коде, а в текстовых требованиях, заметках, таблицах, примерах, обсуждениях и проектных пояснениях. Перевод этого материала в формальный язык требует отдельного усилия и потому далеко не всегда становится частью реального рабочего процесса.
Другой ответ связан с развитием больших языковых моделей. Они сделали практически значимым сценарий, при котором код может быть получен непосредственно из естественно-языкового описания. Такой подход полезен как средство поддержки разработчика, ускорения прототипирования и получения черновых реализаций. Но как основа компиляции такой сценарий остаётся слабым. Модель действительно может сгенерировать рабочий код, однако связь между исходной спецификацией и полученным результатом часто остаётся нестрогой, её трудно воспроизвести, проверить и объяснить как последовательный переход от требования к реализации.
Классическая технология разработки трансляторов языков программирования показывает, что надёжный переход от исходного описания к исполняемому результату обычно строится через последовательные стадии анализа, промежуточного представления, проверок и генерации целевого артефакта. Однако такая технология обычно предполагает, что исходный язык уже является формальным или хотя бы имеет заранее заданную грамматику. В рассматриваемой задаче Markdown не является языком программирования, а используется как носитель спецификационного смысла. Поэтому перед формальной трансляцией требуется дополнительный слой семантического разрешения, нормализации и проверки определённости.
В настоящей работе предлагается промежуточная позиция. Markdown рассматривается как человеко-ориентированная среда записи спецификационного смысла. Разработчик описывает в нём сущности, ограничения, инварианты, правила, состояния и примеры. Система, в свою очередь, не компилирует сырой текст напрямую, а извлекает из него каноническую спецификацию, проверяет её и только затем передаёт в детерминированный нижний слой компиляции. Иными словами, объектом компиляции является не Markdown как последовательность строк, а достаточно определённый смысл, извлечённый из Markdown-документа и приведённый к проверяемой форме.
Постановка проблемы и границы рассматриваемой задачи
Проблема, рассматриваемая в данной работе, возникает на пересечении трёх ограничений современной разработки программного обеспечения. Первое связано с традиционным кодом, второе – с формальными спецификациями, третье – с прямой генерацией кода из естественного языка. Каждое из этих направлений решает часть задачи, но ни одно из них не закрывает её полностью.
В традиционных языках программирования исполнимость достигается за счёт высокой операционной определённости. Код точно задаёт последовательность вычислений, условия, ветвления, вызовы и возвращаемые значения. Однако такая определённость не равна полноте предметного описания. Существенные элементы знания о системе часто остаются за пределами исполняемой части. К ним относятся бизнес-правила, обоснования принятых решений, ограничения предметной области, допустимые состояния, примеры корректного поведения и внешние условия. Они могут быть записаны в документации, комментариях, задачах трекера или оставаться в неформальных договорённостях команды. В результате код является основным носителем исполнения, но не всегда остаётся полным носителем смысла.
Формальные языки спецификаций предлагают другой путь. Они позволяют описывать систему строго и проверяемо, выявлять противоречия, анализировать состояния и доказывать свойства. Однако такая строгость достигается ценой высокого порога входа. Разработчик должен не только знать предметную область, но и уметь выражать её в терминах выбранной формальной системы. Для многих инженерных команд это оказывается слишком тяжёлым требованием, особенно на ранних стадиях проектирования, когда логика ещё уточняется, а требования существуют в форме естественного языка, списков, таблиц и примеров.
Прямой переход от естественного языка к коду сохраняет удобство входа, но переносит ключевое решение в вероятностный слой. Если в исходном описании есть неполнота или неоднозначность, модель может заполнить её правдоподобной догадкой. Для обычного прототипирования это может быть приемлемо. Однако для компилятора спецификаций такой подход опасен, поскольку отсутствующее предметное решение фактически заменяется предположением системы. Следовательно, требуется архитектура, в которой вариативность естественного языка допускается на входе, но не переносится в нижний слой исполнения. Свободное описание должно быть преобразовано в проверяемую модель, а исполняемый результат должен строиться только из той части смысла, которая стала достаточно определённой.
Предлагаемый подход не ставит задачу универсальной компиляции любого естественно-языкового текста в корректную программу. Такое утверждение было бы слишком широким. Произвольное текстовое намерение может не содержать ни правил поведения, ни критериев корректности, ни типов данных, ни допустимых состояний, ни алгоритмических деталей. Например, фраза «система должна оптимально распределять заказы между исполнителями» сама по себе не задаёт функцию оптимизации, набор ограничений, допустимые эвристики и критерии качества. Такая запись может быть началом постановки задачи, но не является достаточной спецификацией для безопасной компиляции.
Предметом настоящей работы является более ограниченный, но инженерно значимый класс Markdown-документов. Речь идёт о спецификациях, в которых поведение системы может быть выражено через распознаваемые смысловые опоры. К таким опорам относятся сущности, поля, типы, ограничения, инварианты, предусловия, постусловия, переходы состояний, правила принятия решений, вычислительные правила и проверяемые примеры. Такой документ может сохранять свободную форму письма, но должен содержать достаточно информации для построения нормализованной модели. Если в спецификации не определён порог «крупного платежа», не задан критерий «активного пользователя» или не описан источник внешней проверки, система не должна придумывать недостающий смысл. Она должна остановить компиляцию и указать, какое уточнение необходимо.
Предлагаемый подход
Под семантической компиляцией спецификаций (Semantic Spec Compilation, SSC) в данной работе понимается архитектурный подход к преобразованию человеко-ориентированной Markdown-спецификации в исполняемую логику через промежуточную каноническую модель. Это не компиляция Markdown как синтаксиса и не прямая генерация кода из естественного языка. Речь идёт о многоступенчатом процессе извлечения, нормализации, проверки и последующего детерминированного преобразования спецификационного смысла.
SSC не заменяет классическую теорию трансляторов, а переносит её принципы на слабоструктурированные спецификации, где перед формальной трансляцией требуется семантическое разрешение, нормализация и проверка определённости. В классическом трансляторе входной слой (frontend) работает с исходным языком, заданным грамматикой, и строит внутренние представления, пригодные для анализа и генерации кода. В предлагаемом подходе роль входного слоя расширяется. Он должен не только выделить структуру документа, но и установить, какие элементы смысла являются достаточно определёнными, какие выведены из контекста, а какие остаются неоднозначными или конфликтующими.
Markdown в этой схеме выступает исходным артефактом, удобным для человека. Разработчик описывает в нём намерения, ограничения, правила, состояния, примеры и ожидаемое поведение системы. Однако сам Markdown не является исполняемым кодом и не передаётся напрямую в нижний компиляционный слой. Между текстом и целевым артефактом располагается каноническая модель, в которой извлечённый смысл представлен в проверяемой и машинно-обрабатываемой форме.
Обобщённая модель процесса, представленная в нотации, близкой к Event Storming, показана на рисунке 1.
pic
Рисунок 1 – Event Storming-модель процесса SSC
На первой стадии Markdown-документ считывается как человеко-ориентированный артефакт. Система сохраняет исходный текст и технический контекст документа. В этот контекст входят путь к файлу, хеш содержимого, структура заголовков и блоков, а также позиции фрагментов, из которых были извлечены элементы спецификации. Эти сведения нужны для трассировки, то есть для возможности показать, из какого места исходного текста было получено конкретное правило, поле, ограничение или пример.
Далее формируется первично извлечённая спецификация (Extracted Spec). Это черновое структурированное представление того, что система смогла обнаружить в Markdown-документе. На этом этапе выделяются кандидаты на сущности, поля, типы данных, ограничения, правила поведения, примеры, зависимости и внешние проверки. Такая модель ещё не считается корректной спецификацией. Она может содержать повторы, разные названия одного и того же понятия, неполные элементы, неоднозначные формулировки или потенциальные противоречия.
Следующая стадия – связанная спецификация (Resolved Spec). Здесь первично извлечённые элементы сопоставляются друг с другом и приводятся к более согласованному виду. Система связывает разные упоминания одной сущности, сопоставляет правила с нужными полями и примерами, разрешает ссылки, устраняет расхождения в названиях и формирует более цельную модель предметной области.
На практике проблема возникает не только при извлечении отдельных сущностей из текста. Гораздо важнее понять, не описывает ли спецификация одну и ту же сущность разными словами. Такое встречается довольно часто (например, в одном фрагменте разработчик использует слово «платёж», а в другом – техническое имя Payment). Эти элементы можно связать между собой, но не по одному лишь сходству названий. Для такого связывания нужны основания, совпадающие атрибуты, одинаковые правила обработки или одна и та же роль в описываемом процессе. Если таких оснований нет, соответствие не должно считаться установленным фактом. В модели оно должно оставаться неопределённым.
Затем оценивается, насколько надёжно был интерпретирован каждый элемент спецификации. Здесь важно различать несколько случаев. Одни элементы явно заданы в тексте. Другие можно восстановить из контекста. Третьи остаются неоднозначными. Наконец, часть элементов может прямо противоречить остальной спецификации. Например, правило «сумма платежа должна быть больше нуля» достаточно определённо, из него ясно, какое ограничение нужно проверить. Иначе работает фраза «крупный платёж требует проверки». Пока не указано, какая сумма считается крупной, такое правило нельзя превратить в точную логику. Если же в примере используется валюта USD, хотя ранее допустимой названа только RUB, это уже не неоднозначность, а конфликт, который должен быть отдельно зафиксирован.
После такой проверки формируется отчёт валидации. Его задача – показать, можно ли использовать полученную модель для дальнейшей компиляции. В отчёте проверяются полнота описания, согласованность правил и примеров, корректность типов, наличие всех упомянутых сущностей, допустимость переходов состояний и достаточность информации для построения реализации. Если обнаружены блокирующие проблемы – например, отсутствующие определения, противоречивые правила или неоднозначности, влияющие на поведение системы, – компиляцию нужно остановить. Важно, что такая остановка не является сбоем. В предлагаемом подходе это нормальный результат, система не должна достраивать смысл там, где сама спецификация его не задаёт.
Если блокирующих проблем нет, из канонической модели выделяется компилируемая спецификация. Это уже не исходный Markdown-документ и не весь набор извлечённых фрагментов, а только проверенная часть модели, достаточно полная, определённая и непротиворечивая. Именно она передаётся в нижний компиляционный слой. После этой границы система больше не должна обращаться к исходному Markdown, чтобы вероятностно «додумывать» недостающие элементы.
На нижнем уровне выполняется lowering, то есть понижение уровня представления. Компилируемая спецификация преобразуется в промежуточное представление – IR (Intermediate Representation). На этом этапе свободный естественный текст уже исключён из обработки. Дальше система работает не с авторскими формулировками, а со структурированной моделью. Ограничения представлены как проверки, правила поведения – как условные переходы или функции, переходы состояний – как проверяемая логика состояний, примеры – как тестовые случаи или проверочные сценарии. После построения промежуточного представления выполняется его проверка. На этом этапе оцениваются корректность типов, допустимость операций, согласованность переходов управления и соответствие требованиям выбранного нижнего компиляционного механизма, или backend. Затем генератор результата, или emitter, формирует целевой артефакт. Им может быть консольная программа, библиотека, программный интерфейс приложения (Application Programming Interface, API) или иной поддерживаемый результат.
Выбор целевого артефакта не должен относиться к уровню Markdown. Markdown описывает предметную логику, а форма исполнения выбирается отдельно на нижнем уровне. Одна и та же компилируемая спецификация может быть преобразована в разные целевые формы, если соответствующие генераторы результата это поддерживают.
Markdown-спецификация и пример записи
Если Markdown рассматривается как спецификационная среда, от разработчика требуется не имитация программирования в текстовой форме, а фиксация предметного смысла. В центре внимания находятся не инструкции для машины, а сущности предметной области, ограничения, правила поведения и ожидаемые результаты.
При этом Markdown не должен превращаться в скрытый предметно-ориентированный язык (Domain-Specific Language, DSL) с жёстким набором обязательных конструкций. Его ценность состоит в том, что разработчик может писать в привычной инженерной форме, используя текст, списки, таблицы, примеры, пояснения и псевдокод. Однако свобода формы не означает произвольности содержания. Чтобы спецификация могла быть скомпилирована, она должна содержать смысловые опоры, достаточные для построения нормализованной модели.
К таким опорам относятся назначение модуля, описание сущностей, их свойства, ограничения, инварианты, правила поведения, предусловия, постусловия, зависимости и примеры входных и выходных ситуаций. Особенно важны примеры, поскольку они связывают словесное правило с наблюдаемым поведением. Пример человеко-ориентированной записи приведён в листинге 1.
Листинг 1 – Пример человеко-ориентированной Markdown-спецификации
```markdown
# Согласование платежей по договору
Нужен модуль согласования платежей для организации.
Сумма платежа должна быть положительной.
Валюта на текущем этапе – только RUB.
## Платёж
- сумма: decimal
- валюта: string
- статус: создан | подтверждён | отклонён
Инварианты:
- сумма > 0
- после подтверждения сумма не изменяется
## Согласование платежа
Если сумма меньше 100 000 руб., платёж согласуется автоматически.
Если сумма 100 000 руб. и выше, требуется подтверждение бухгалтером.
Примеры:
- 35 000 RUB -> подтверждён
- 150 000 RUB без подтверждения бухгалтера -> создан
- 150 000 RUB с подтверждением бухгалтера -> подтверждён
```
Такой фрагмент не заставляет автора заранее переводить каждое утверждение в формальный синтаксис. Разработчик всё ещё пишет на естественном языке, но в тексте уже есть опорные элементы, с которыми может работать система (сущность Payment, поля amount, currency, status, ограничение amount > 0, правило согласования и проверочные примеры). Иначе обстоит дело с документом, где есть только общее намерение – без условий, ограничений и примеров. Такой текст может быть полезен как постановка задачи, но его недостаточно, чтобы безопасно выполнить семантическую компиляцию.
Работа с неопределённостью и каноническая модель
В предлагаемом подходе исходная спецификация сначала остаётся человеческим описанием, а не формальной программой. Следовательно, система неизбежно сталкивается с вариативностью формулировок, неполнотой и смысловой неоднозначностью. Работа с неопределённостью не является дополнительной функцией архитектуры. Она определяет границу между допустимым извлечением смысла и недопустимым домысливанием.
Необходимо различать вариативность формулировки и смысловую неоднозначность. Вариативность возникает тогда, когда одно и то же правило выражено разными словами, но сохраняет один и тот же смысл. Например, утверждения «сумма должна быть положительной», amount > 0 и «нельзя передавать ноль и отрицательные значения» могут быть приведены к одному ограничению. Смысловая неоднозначность возникает в другом случае. Если текст говорит «крупный платёж требует проверки», но не определяет критерий крупного платежа, система не имеет достаточного основания для построения исполняемого правила. Здесь проблема не в форме выражения, а в отсутствии необходимого предметного решения.
Для управляемой работы с неопределённостью каждый извлечённый элемент должен получать явный статус. Такой статус относится не ко всему документу, а к конкретному элементу модели. Это может быть поле, правило, ограничение, пример, переход состояния или внешняя зависимость. Базовые статусы приведены в таблице 1.
Таблица 1 – Статусы определённости элементов канонической модели
Статус Смысл статуса Пример Действие системы
явно определённый (deterministic) элемент явно задан в тексте «сумма платежа должна быть больше 0» допускается к валидации и дальнейшей компиляции
выведенный (derived) элемент выведен из контекста из примеров следует порог согласования требует подтверждения на этапе валидации
неоднозначный (ambiguous) элемент допускает несколько интерпретаций «крупный платёж» без порога блокирует компиляцию соответствующей части
конфликтующий (conflicting) разные фрагменты противоречат друг другу текст разрешает только RUB, пример содержит USD блокирует компиляцию до устранения конфликта

Элементы со статусами ambiguous и conflicting нельзя передавать в нижний компиляционный слой как установленные факты. Они должны оставаться в отчёте валидации как признаки неопределённости или противоречия. Элементы со статусом derived можно использовать осторожно, только если их подтверждают другие части спецификации – примеры, инварианты, явные ссылки или согласованные правила. Каждый статус должен быть объяснимым. Для элемента необходимо хранить ссылку на исходный фрагмент Markdown, основание присвоения статуса и, если требуется, связанные фрагменты, из которых возник вывод или конфликт.
Каноническая модель выступает центральной границей между свободным описанием и строгим машинным представлением. Она не заменяет Markdown как пользовательскую форму записи и не превращается в новый язык, который разработчик обязан писать вручную. Её задача состоит в том, чтобы привести извлечённый смысл к единой структуре. В этой структуре должны быть представлены сущности, поля, типы, ограничения, правила, переходы состояний, примеры, зависимости, статусы определённости и ссылки на исходные фрагменты документа.
Если в архитектуре используется агент или большая языковая модель, их роль должна быть ограничена верхним семантическим слоем. Модель может помогать выделять кандидаты на сущности, правила, ограничения, примеры, зависимости и возможные неоднозначности. Однако она не должна рассматриваться как компилятор, генератор финального кода или окончательный источник корректности. Результат её работы должен быть представлен в структурированной форме и затем пройти обычные стадии связывания, оценки определённости и валидации. При неизменной компилируемой спецификации повторная сборка не должна зависеть от повторного вероятностного ответа модели.
Место подхода среди аналогов и научная новизна
Предлагаемая концепция не возникает в полном отрыве от существующих исследований. Прежде всего она соотносится с технологией разработки трансляторов, где переход от исходного текста к исполняемому результату обычно организуется через анализ, внутренние представления, проверки и генерацию целевого кода [1]. Однако SSC переносит эти принципы на иной тип входа. В качестве такого входа выступает не формальный язык программирования, а слабоструктурированная спецификация, в которой до построения промежуточного представления необходимо разрешить смысловую неполноту и неоднозначность.
Кроме того, подход находится на пересечении нескольких смежных направлений, каждое из которых затрагивает отдельную часть рассматриваемой задачи. Исследования преобразования естественного языка в формальные спецификации показывают, что текстовое описание может служить исходным материалом для построения строгой модели [2]. Работы по исполняемой документации демонстрируют возможность рассматривать документационные формы не только как пояснение к системе, но и как источник последующего исполнения [3]. Подходы, подобные Doc2Spec, развивают идею синтеза формальных спецификаций из естественного языка через промежуточные грамматические и структурные ограничения [4].
Практические системы класса Cucumber/Gherkin показывают, что текстовые сценарии могут быть встроены в инженерный процесс как исполняемые спецификации, хотя для связывания текста с кодом обычно требуются заранее написанные шаговые определения [5]. Формальные языки TLA+ и Alloy демонстрируют, каким может быть строгое спецификационное ядро, пригодное для проверки свойств и анализа состояний [6], [7]. Нейро-символьные системы, в частности Jigsaw, показывают важность последующей обработки и анализа результата, полученного от большой языковой модели, а не безусловного доверия её прямому выводу [8]. Литературное программирование исторически связывает текст и программу, но исходит прежде всего из того, что код уже присутствует внутри документа [9]. Современные обзоры работ по формализации требований с применением больших языковых моделей подтверждают, что область активно развивается, но пока не сводится к единому устоявшемуся подходу [10]. Сравнительная позиция предлагаемого подхода показана в таблице 2.
Таблица 2 – Сравнение Semantic Spec Compilation со смежными подходами и классической трансляторной схемой
Подход Вход Промежуточная модель Работа с неопределённостью Итоговый результат
Технология разработки трансляторов формальный язык внутренние представления компилятора обычно не требуется целевой код или программа
Литературное программирование текст с включённым кодом не является обязательной не рассматривается код, связанный с документом
Cucumber/ Gherkin текстовые сценарии по заданным правилам частично ограниченная тестовые сценарии
TLA+/ Alloy формальная спецификация формальная модель устраняется на уровне записи анализ модели
Прямая генерация кода LLM естественный язык обычно отсутствует обычно не фиксируется явно программный код
Естественный язык → формальная спецификация естественный язык формальная спецификация частичная формальная модель
Semantic Spec Compilation слабоструктурированный Markdown каноническая модель явная оценка определённости исполняемый артефакт

Из этого сопоставления следует, что отдельные элементы предлагаемой архитектуры уже представлены в смежных направлениях. Новизна работы не должна формулироваться как утверждение, что каждый компонент является новым сам по себе. Существенным является их объединение в единую архитектурную схему. В неё входят свободный, но смыслово-дисциплинированный Markdown, семантическое извлечение, каноническая модель с трассировкой и статусами определённости, детерминированная валидация и нижний компиляционный слой, формирующий исполняемый артефакт только из проверенной модели.
В этой связи важно не называть SSC обычным компилятором Markdown. Такая формулировка была бы неточной, поскольку Markdown в предлагаемой архитектуре не является формальным исходным языком. Более корректно рассматривать SSC как расширение трансляторной схемы на область спецификаций, где до классических стадий анализа и генерации требуется отдельный этап установления достаточного смысла. Отличие состоит не только в формате входа, но и в обязанности системы работать с неполнотой, неоднозначностью и конфликтами, которые в обычном языке программирования устраняются уже на уровне грамматики и синтаксической дисциплины.
Первый элемент новизны состоит в использовании Markdown как первичного человеко-ориентированного входа без превращения его в жёсткий предметно-ориентированный язык. Второй элемент связан с обязательной канонической моделью, которая отделяет свободную форму человеческого описания от строгой формы, пригодной для проверки и компиляции. Третий элемент состоит в явной работе с неопределённостью. Система должна не скрывать неоднозначность за вероятностными догадками, а фиксировать её как часть модели. Четвёртый элемент связан с разделением недетерминированного верхнего слоя и детерминированного нижнего слоя. Пятый элемент относится к целевой исполняемости. Одна и та же проверенная спецификация может быть выведена в разные формы исполнения без изменения предметной семантики.
Метод проверки и план экспериментов
Поскольку работа носит архитектурно-исследовательский характер, её ключевые утверждения должны быть сформулированы как проверяемые гипотезы. Проверка должна оценивать не только способность системы получить исполняемый результат, но и качество промежуточного перехода. К таким показателям относятся полнота извлечения, обнаружение неоднозначностей, воспроизводимость, корректность поведения и стоимость человеческого уточнения.
Проверку подхода целесообразно строить вокруг нескольких вопросов. Прежде всего нужно определить, можно ли для ограниченного класса Markdown-спецификаций, содержащих сущности, ограничения, правила, состояния и примеры, извлекать каноническую модель с измеримой полнотой и точностью без перевода входного документа в жёсткий язык. Отдельно следует проверить, повышает ли фиксируемая каноническая модель воспроизводимость результата по сравнению с прямым переходом от естественного языка к коду. Ещё один важный вопрос связан с примерами. Предполагается, что их наличие снижает число неоднозначных интерпретаций и повышает поведенческую корректность результата. Также необходимо оценить, действительно ли явная стадия определения статуса элементов снижает риск небезопасной компиляции. Наконец, трассировка неопределённых и конфликтующих элементов должна показать, помогает ли она уменьшить объём ручных уточнений со стороны разработчика.
Для проверки предлагается сформировать корпус спецификаций трёх типов. В него должны входить строго структурированные Markdown-документы, более свободные инженерные описания, а также шумные либо намеренно неполные документы. Содержательно корпус должен охватывать вычислительные правила, конечные автоматы состояний, простые рабочие процессы и сценарии валидации. Такое разнообразие необходимо для проверки того, насколько устойчиво архитектура работает на различных типах предметной логики.
Сравнение должно включать как внешние базовые варианты, так и абляционные версии самой архитектуры. Внешними вариантами могут быть прямая генерация кода из естественного языка, подход с жёстко заданными разделами и вариант на основе контролируемого естественного языка. Абляционные варианты должны исключать отдельные компоненты предлагаемого конвейера, например стадию оценки определённости или валидацию на основе примеров. Это позволит оценить не только общий результат, но и вклад конкретных архитектурных решений. Основные метрики оценки представлены в таблице 3.
Таблица 3 – Метрики оценки предлагаемой архитектуры
Группа метрик Что оценивается Пример показателя
извлечение смысла насколько полно и точно построена каноническая модель точность и полнота извлечения сущностей, правил, ограничений и примеров
неопределённость насколько корректно обнаружены неоднозначные и конфликтующие элементы точность и полнота выявления ambiguous/conflicting элементов
безопасность компиляции насколько система избегает небезопасного допуска доля ложных допусков и ложных отказов
поведенческая корректность соответствует ли итоговый артефакт примерам и независимым тестам доля успешно пройденных тестов
воспроизводимость стабилен ли результат при неизменной спецификации и версиях инструментов совпадение Compilable Spec, IR и поведения артефакта
объяснимость можно ли связать элементы модели с исходным Markdown полнота трассировки
стоимость уточнения сколько усилий требуется для исправления спецификации число итераций, объём правок и время исправления

На уровне раннего прототипа подход можно считать подтверждённым, если система демонстрирует более высокую воспроизводимость по сравнению с прямой генерацией кода, корректно останавливает компиляцию при неоднозначных или конфликтующих спецификациях, сохраняет трассировку к исходному Markdown и стабильно проходит тесты, построенные на основе примеров из спецификации.
Ограничения и угрозы валидности
Предлагаемый подход не снимает все проблемы, которые возникают при переходе от свободного текстового описания к исполняемой логике. Его задача скромнее, не компилировать любой произвольный текст, а дать практический способ связать человеческую спецификацию с воспроизводимым исполнением. Поэтому от разработчика всё равно требуется достаточно ясно описывать сущности, ограничения, правила и примеры. Без этих опор система не сможет построить устойчивую каноническую модель.
Отдельное ограничение связано с качеством самой канонической модели. Даже если смысл Markdown-документа извлечён корректно, этого ещё недостаточно. Внутренняя модель должна уметь точно представить сущности, правила, ограничения и связи между ними. Иначе ошибка может появиться уже не при чтении текста, а на следующем шаге – при преобразовании извлечённого смысла в исполняемый результат.
Важную роль здесь играет валидатор. Он должен не просто пропускать корректные спецификации, но и останавливать те случаи, где смысл остаётся неполным, противоречивым или недостаточно определённым для безопасной компиляции. При этом отказ должен быть объяснимым. Разработчик должен видеть, какой элемент спецификации вызвал проблему и почему система не может продолжить обработку.
К угрозам внутренней валидности относится зависимость результата от конкретной реализации верхнего семантического слоя. Поведение системы может существенно меняться в зависимости от выбранной модели, способа извлечения, структуры запроса и параметров генерации. Поэтому при экспериментальной проверке необходимо отделять свойства архитектуры от свойств частного прототипа.
К угрозам внешней валидности относится риск слишком искусственного корпуса. Если экспериментальные документы будут написаны в стиле, заранее удобном для системы, результаты могут оказаться завышенными. Отдельно следует учитывать риск ложной новизны. Поскольку отдельные элементы предлагаемого подхода уже присутствуют в смежных направлениях, новизну необходимо обосновывать не через отдельные компоненты, а через их целостную архитектурную комбинацию.
Инженерные сценарии отказа также должны рассматриваться явно. Система может создать элемент канонической модели без достаточного основания в исходном тексте, не обнаружить скрытый конфликт между правилами и примерами, ошибочно перевести выведенный элемент в статус явно определённого, использовать устаревший кэш или породить различия в артефактах из-за разных версий инструментов сборки. Для снижения этих рисков необходимы трассировка, хеширование исходного документа, фиксация версии схемы канонической модели и фиксация версий нижнего компиляционного механизма.
ЗАКЛЮЧЕНИЕ
В данной работе предложена концепция семантической компиляции спецификаций, в рамках которой Markdown рассматривается как первичный человеко-ориентированный носитель спецификационного смысла, а исполняемая логика возникает не как прямой результат вероятностной генерации, а как итог последовательного построения, нормализации, проверки и компиляции канонической модели. Ключевой вывод работы состоит в следующем, компилировать следует не сам Markdown-текст, а только тот смысл, который удалось извлечь, проверить и привести к достаточно определённой форме.
Предлагаемая архитектура занимает промежуточное положение между строгими формальными языками спецификаций, технологией разработки трансляторов и прямой генерацией кода из естественного языка. В отличие от формальных языков и классических трансляторов, она работает с человеко-ориентированным входом и допускает вариативность Markdown-документов. В отличие от второй, она не передаёт вероятностной модели право окончательного решения о корректности. В этой схеме неоднозначность не скрывается, а явно маркируется. Компиляция допускается только после строгой валидации. Нижний слой работает с проверенной моделью и остаётся детерминированным.
При этом область применимости подхода должна пониматься ограниченно. Речь не идёт об автоматической компиляции произвольного текста или о синтезе любых алгоритмов из неполного намерения. Наиболее естественная область раннего применения – правила, ограничения, контракты, вычислительные условия, простые рабочие процессы, конечные автоматы состояний и спецификации, снабжённые проверяемыми примерами. В таких случаях Markdown может выступать не просто документацией, а исходным материалом для построения воспроизводимой исполняемой логики.
Дальнейшая проверка концепции требует экспериментальной реализации, корпуса спецификаций, эталонной разметки и сравнения с базовыми подходами. Ключевыми критериями успеха должны быть не только способность системы что-либо скомпилировать, но и её способность корректно различать определённые, неоднозначные и конфликтующие фрагменты, сохранять трассировку к исходному Markdown и воспроизводимо строить целевой артефакт из валидированной модели.

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

  • Aho A. V. Compilers: Principles, Techniques, and Tools [Текст] / A. V. Aho, M. S. Lam, R. Sethi, J. D. Ullman. – 2nd ed. – Boston : Pearson/Addison Wesley, 2006. – 1040 p.
  • Hahn C., Schmitt F., Tillman J. J., Metzger N., Siber J., Finkbeiner B. Formal Specifications from Natural Language [Электронный ресурс]. arXiv:2206.01962. URL: https://arxiv.org/abs/2206.01962 (дата обращения: 18.04.2026).
  • Tegeler T., Beelman S., Schürmann J., Smyth S., Teumert S., Steffen B. Executable Documentation: From Documentation Languages to Purpose-Specific Languages [Электронный ресурс]. ISoLA 2022. URL: https://link.springer.com/chapter/10.1007/978-3-031-19756-7\_10 (дата обращения: 18.04.2026).
  • Xia S., He M., Jia H., Song L. Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction [Электронный ресурс]. arXiv:2602.04892. URL: https://arxiv.org/abs/2602.04892 (дата обращения: 18.04.2026).
  • Cucumber Documentation [Электронный ресурс]. URL: https://cucumber.io/docs/ (дата обращения: 18.04.2026).
  • Lamport L. TLA+ Home Page [Электронный ресурс]. URL: https://lamport.azurewebsites.net/tla/tla.html (дата обращения: 18.04.2026).
  • Alloy Tools [Электронный ресурс]. URL: https://alloytools.org/ (дата обращения: 18.04.2026).
  • Jain N., Vaidyanath S., Iyer A., Natarajan N., Parthasarathy S., Rajamani S., Sharma R. Jigsaw: Large Language Models meet Program Synthesis [Электронный ресурс]. arXiv:2112.02969. URL: https://arxiv.org/abs/2112.02969 (дата обращения: 18.04.2026).
  • Knuth D. E. Literate Programming [Электронный ресурс] // The Computer Journal. 1984. Vol. 27, no. 2. P. 97–111. URL: https://academic.oup.com/comjnl/article/27/2/97/343244 (дата обращения: 18.04.2026).
  • Beg A., O'Donoghue D., Monahan R. A Short Survey on Formalising Software Requirements using Large Language Models [Электронный ресурс]. arXiv:2506.11874. URL: https://arxiv.org/abs/2506.11874 (дата обращения: 18.04.2026).
-Источник
 
Loading...
Error