Доказательства · 13 мин
Граф, Exact и границы доказательства
Что система действительно подтверждает, а что остаётся гипотезой агента.
Слово «связь» звучит одинаково и для найденного совпадения, и для вызова, подтверждённого структурным анализом. Для изменения кода это принципиально разные основания.
Доказательство должно сохранять происхождение: точный факт остаётся точным, а эвристика не повышается до факта из-за уверенной формулировки агента.
Exact фиксирует воспроизводимый факт
Exact — точный фрагмент или отношение, которое можно повторно получить из неизменяемого снимка. Класс exact_static означает подтверждённый статический факт кода, а exact_manifest — точный факт из структурированного манифеста.
Это уже не пересказ модели. Но сила факта ограничена его предметом: три локальных вызова не доказывают все возможные динамические пути выполнения.
Эвристика и динамика остаются отдельными классами
heuristic обозначает связь, полученную приближённым анализом. dynamic — ситуацию, где точная цель зависит от выполнения программы. Оба результата полезны как направление проверки, но их нельзя представлять как exact_static.
Пустой результат Exact также не доказывает отсутствие, если система не подтвердила полноту проверки. Формулировка должна быть «факт не найден в доступной области», а не «вызова нет».
Точный факт структурированного описания.
Подтверждённая статическая связь кода.
Полезная, но приближённая связь.
Цель определяется только при выполнении.
Проектный граф и библиотечный Exact нельзя смешивать
Для проекта LEM умеет показывать определение, вызывающие элементы, область влияния и поток вызовов в пределах доступного графа. В первой библиотечной демонстрации публичны list, search, symbol и точечный Exact.
Поэтому честная подпись звучит так: «в sdk/client.bsl подтверждены три локальных вызова». Формулировка «построен полный граф всех зависимостей библиотеки» сейчас недопустима.
Граница доказательства должна быть видна рядом с выводом
Не прячьте ограничения в подвале страницы. Укажите координату, класс факта, область анализа и неизвестное непосредственно рядом с рекомендацией. Так агент не сможет расширить узкий факт до общего обещания незаметно для читателя.
Три локальных вызова — не полный маршрут
В синтетическом client.bsl можно подтвердить три вызова из СоздатьОтправление. Запрос агенту: «Покажи три точные связи, файл и версию; отдельно перечисли связи, которых этот результат не доказывает». Правильный ответ сохраняет ровно три стрелки и не дорисовывает путь до внешнего сервиса по названию функции.
Если в рецепте упоминается модуль повторов, это полезная смысловая подсказка, но не четвёртый статический вызов. Для полного пути исполнения нужны проектный граф, динамические проверки и доступ к соответствующему коду; публичное демо их не предоставляет.
Три сплошные стрелки и две пунктирные
Из СоздатьОтправление Exact подтверждает три локальных вызова. Упоминание модуля повторов в рецепте показывает смысловую связь, но не статический вызов.
- Нарисовать три подтверждённые стрелки сплошной линией.
- Пунктиром отметить смысловые кандидаты.
- Подписать класс каждого ребра.
- Для пустого результата сохранить состояние «не доказано».
Имена относятся к синтетическому корпусу. Полный library graph, impact, flow и visualize не обещаются.
Что уже можно утверждать, а что нужно проверить
- Классы exact_static и exact_manifest обозначают точные факты.
- Q4 подтверждает ограниченный набор локальных вызовов.
- Динамические цели вызовов.
- Полноту графа за пределами доказанной области.
- Отсутствие связи при неполной проверке.