Справочное руководство по Ada 2012
H.3.2 Предикат Inspection_Point
Встречающаяся конструкция предиката Inspection_Point определяет набор объектов, значения которых должны быть доступны в момент(ах) выполнения программы, соответствующих положению предиката в единице компиляции. Цель такого предиката заключается в облегчении проверки кода.
Синтаксис
Форма предиката pragma Inspection_Point имеет следующий вид:
Правила допустимости
Предикат Inspection_Point разрешается там, где разрешены элемент_объявления или выражение. Каждое имя_объекта должно статически обозначать объявление объекта.
Статическая семантика
Точка инспекции — это момент в объектном коде, соответствующий появлению предиката Inspection_Point в единице компиляции. Объект является инспектируемым в точке инспекции, если соответствующий предикат Inspection_Point либо содержит аргумент, обозначающий этот объект, либо не содержит аргументов и объявление объекта видно в точке инспекции.
Динамическая семантика
Выполнение предиката Inspection_Point не оказывает никакого эффекта.
Требования к реализации
Достижение точки инспекции является внешним взаимодействием по отношению к значениям инспектируемых объектов в этой точке (см. 1.1.3).
Требования к документации
Для каждой точки инспекции реализация должна определить отображение между каждым инспектируемым объектом и аппаратными ресурсами (такими как ячейки памяти или регистры), из которых можно получить значение объекта.
ПРИМЕЧАНИЯ
7 Реализация не допускает выполнения «удаления мёртвых присваиваний» для последнего присваивания переменной перед точкой, где эта переменная инспектируема. Таким образом, точка инспекции имеет эффект неявного чтения каждого из её инспектируемых объектов.
8 Точки инспекции полезны для поддержания соответствия между состоянием программы в терминах исходного кода и состоянием машины во время выполнения программы. Утверждения о значениях объектов программы могут проверяться в терминах машины в точках инспекции. Объектный код между точками инспекции может обрабатываться автоматизированными инструментами для механической проверки программ.
9 Определение отображения от объектов исходной программы к аппаратным ресурсам разрешается в виде аннотированного списка объектов, в удобочитаемой или обработываемой инструментами форме.
