Почтовые условия и ограниченные в выходных параметрах - PullRequest
0 голосов
/ 20 сентября 2018

Как указать, что ограниченный выходной параметр не изменяется при вызове подпрограммы по условию post?Рассмотрим следующий код:

with Ada.Text_IO;

procedure Main is

   package C is

      type Printer is tagged limited private;

      procedure Print
        (P : in out Printer;
         B : Integer);

   private

      type Printer is tagged limited record
         A : Integer := 0;
      end record;

   end C;

   package body C is

      procedure Print
        (P : in out Printer;
         B : Integer) is
      begin
         if B >= 0 then
            P.A := B;
         end if;
         Ada.Text_IO.Put_Line (P.A'Image);
      end Print;

   end C;

   P : C.Printer;
begin
   P.Print (-1);
end Main;

Когда в качестве входных данных для подпрограммы «Печать» указано отрицательное число, внутреннее состояние экземпляров принтера остается неизменным во время вызова подпрограммы.Каков наилучший способ указать это?Попытка выполнить следующее приводит к сообщению об ошибке «атрибут« Старый »не может применяться к ограниченным объектам»:

procedure Print
    (P : in out Printer;
     B : Integer) with
    Post => (if B < 0 then P'Old = P);

Может ли решение быть найдено в агрегатах дельты в стандарте Ada 2020?

ПРАВКА: Это может быть сложный вопрос, учитывая, что ограниченные типы по определению не имеют оператора равенства.

1 Ответ

0 голосов
/ 21 сентября 2018

С 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;

Это позволяет достичь почти того, что вы хотели, но я сомневаюсь, что это стоит того из-за бремени обслуживания.

...