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