Декларативный подход
Стиль записи, где программа — система правил и ограничений, описывающих нужный результат, без порядка шагов: сказано, что должно быть верно, а как этого добиться, решает движок. Так устроены ограничения и запросы в базе данных, правила вывода, описание желаемого состояния системы. Пример: «брони одной комнаты не пересекаются», «бронь не дольше 4 часов» в виде ограничений в базе. Простые декларативные записи проверяются по тексту точно, потому что их поведение видно из самой записи. На мощном декларативном языке это уже не так, и теорема Райса задевает его так же, как императивный код.
Где встречается: языки, валидаторы, движки
- SQL · запрос описывает, какие данные нужны, а база сама выбирает, как их достать. Ограничения CHECK, UNIQUE и EXCLUDE — правила, которые база держит при каждой записи.
- Kubernetes · описывают желаемое состояние: какие сервисы и сколько копий запустить. Контроллеры в петле сверки приводят систему к нему.
- JSON Schema · схема описывает форму данных, валидатор проверяет по ней каждый документ.
- Quint · а также TLA+ и Alloy: правила и инварианты системы записаны как утверждения, проверка моделей перебирает состояния.
- Z3 · ограничения на значения; решатель ищет значения, которые им удовлетворяют, или доказывает, что таких нет.
- Prolog · факты и правила вывода; движок сам ищет ответ на вопрос. Язык полный: на нём можно написать и вечный цикл.
- Datalog · урезанный Prolog для запросов к данным: любой запрос гарантированно заканчивается, поэтому ответ всегда точный.
Источник: Википедия: декларативное программирование
Подробнее: Где ставить проверку работы ИИ-агентаПетля сверки для спек: как в KubernetesЧем model checking отличается от тестовСпеки по агрегатам
Где встречается · 2
- Где ставить проверку работы ИИ-агента · Спеки и контекст
- Теорема Райса простыми словами · Спеки и контекст