С RM 6.1.1
Для каждого X'Old в включенном выражении постусловия константа неявно объявляется в начале подпрограммы или записи.Константа имеет тип X и инициализируется результатом вычисления X (как выражения) в точке объявления константы.Значение X'Old в выражении постусловия является значением этой константы;тип X'Old - это тип X. Эти неявные объявления констант встречаются в произвольном порядке.
AARM весьма явный:
'Old делает noсмысл для ограниченных типов, потому что его реализация включает в себя копирование.Возможно, в семантическом смысле можно разрешить сборку на месте, но это того не стоит.
Я не думаю, что дельта-агрегаты решат проблему, потому что я не понимаю, как это могло бы предотвратитьнеявная копия.
Однако, хотя вы не можете применить 'old
к ограниченному объекту, вы можете применить его к одному или нескольким из его неограниченных компонентов.
procedure Print
(P : in out Printer;
B : Integer) with Post => (if B < 0 then P.A'Old = P.A);
Конечно, в вашем примере компонент A является частным, поэтому это не будет работать и, как правило, нежелательно для публичных процедур.
Чтобы решить эту проблему, вы можете захотеть обернуть компонент в функцию получения и написать:
function Printer_Value (P : in Printer) return Integer;
procedure Print
(P : in out Printer;
B : Integer) with Post => (if B < 0 then P.Printer_Value'Old = P.Printer_Value);
private
function Printer_Value (P : in Printer) return Integer is (P.A);
, а затем настроить Printer_Value, чтобы вручную включать компоненты, которые должны проверяться на неизменность.Но это также не компилируется, потому что P.Printer_Value'Old
потенциально не оценено (когда B>=0
).AARM заявляет, что обычное решение - сделать P'Old.Printer_Value
, но это невозможно, потому что P ограничено.Поэтому, чтобы заставить его работать, мы должны оценить его безоговорочно:
procedure Print
(P : in out Printer;
B : Integer) with Post => P.Printer_Value'Old = P.Printer_Value or else B >= 0;
Это позволяет достичь почти того, что вы хотели, но я сомневаюсь, что это стоит того из-за бремени обслуживания.