Руководство по Ada (Ada 2022)

H.3.2 Предикат Inspection_Point

Встречаемость предиката Inspection_Point определяет набор объектов, значения которых должны быть доступны в момент(ах) выполнения программы, соответствующих положению предиката в единице компиляции. Цель такого предиката — облегчить проверку кода.

Синтаксис

Форма предиката Inspection_Point такова:

pragma Inspection_Point[(имя_объекта_имя {, имя_объекта_имя})];

Правила допустимости

Предикат Inspection_Point разрешается там, где разрешается элемент_объявления или выражение. Каждое имя_объекта должно статически обозначать объявление объекта.

Статическая семантика

Точка проверки — это точка в объектном коде, соответствующая появлению предиката Inspection_Point в единице компиляции. Объект является проверяемым в точке проверки, если соответствующий предикат Inspection_Point содержит аргумент, обозначающий этот объект, или не содержит аргументов, а объявление объекта видимо в точке проверки.

Динамическая семантика

Выполнение предиката Inspection_Point не оказывает никакого эффекта.

Требования к реализации

Достижение точки проверки — это внешнее взаимодействие по отношению к значениям проверяемых объектов в этой точке (см. 1.1.3).

Требования к документации

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

ПРИМЕЧАНИЕ 1 Поскольку достижение точки проверки считается внешним взаимодействием по отношению к значениям проверяемых переменных, реализация не может выполнить «удаление мёртвых записей» последнего присваивания такой переменной перед точкой проверки. Таким образом, точка проверки имеет эффект неявного считывания каждого из своих проверяемых объектов.

ПРИМЕЧАНИЕ 2 Точки проверки полезны для поддержания соответствия между состоянием программы в терминах исходного кода и состоянием машины во время выполнения программы. Утверждения о значениях объектов программы могут быть проверены в машинных терминах в точках проверки. Объектный код между точками проверки может обрабатываться автоматизированными инструментами для механической проверки программ.

ПРИМЕЧАНИЕ 3 Определение отображения от объектов программы на машинные ресурсы может быть представлено в виде аннотированного списка объектов в удобочитаемой или обрабатываемой инструментами форме.