Ваш .md-файл — не спецификация: формальный анализ находит пробелы в требованиях
.md File is not a specification: Using formal analysis to find requirements gaps
Автор показывает на примере приложения для записи в салон, как формальный анализ с помощью Dynamic Logic и инструмента FizzBee выявляет неоднозначности и пробелы в требованиях, записанных даже в нотации EARS. Модель проверки обнаруживает нарушение инварианта: если стилист меняет расписание после бронирования, старая запись остаётся. Рассматриваются три варианта решения — блокировка, каскадная отмена или ручное урегулирование, — и подчёркивается, что выбор остаётся за продуктом.
Инварианты нельзя протестировать. Можно тестировать только предусловия и постусловия. Инварианты должны быть обоснованы на основе этих тестируемых предусловий и постусловий.
- ActionHank
Ок, то есть предлагаемое решение здесь — определить спецификацию на том, что по сути является кодом для другой LLM, чтобы она потом интерпретировала его в другой код?
Не уверен, что это делает что-то большее, чем скилл grillme, а потом тыканье агента, чтобы он сделал работу.
- jackdaniels4me
Сегодня большинство кодинг-агентов поддерживают spec-driven development (или plan mode).
Обычно они фиксируют требования, дизайн и план реализации в Markdown-файлах. Но действительно ли этот Markdown-файл — спецификация?
В этой статье рассматривается, как формальный анализ может выявить пробелы в требованиях, которые легко упустить.