ADA - предварительное условие «класса

Question

Я пытаюсь скомпилировать этот код:

function valid(a:Toto'Class; t: Titi) return Boolean with Pre'Class => fonction(a); 

ВНСТ говорит„аспект „pre'class“ может быть указан только для примитивной работы с тегами частного“

Я думаю, это из-за Toto'Class, но как я могу заставить его работать?

Answer 1

Целью Pre'Class и Post'Class, я считаю, является указание предварительных условий, которые применяются, даже если переопределенная подпрограмма.

package Pack1 is 
    type Base_Type is tagged record ... end record; 
    procedure Operation (Obj : Base_Type) with Pre'Class => [condition]; 
end Pack1; 

Что это означает, что если условие выполнено, то Operation допускается, даже если производные типы накладывают другие условия. Предположим, что процедура использует эту операцию на Base_Type'Class объекта:

procedure Something_Else (Obj : Base_Type'Class) is 
begin 
    -- check to make sure the condition is true 
    Obj.Operation; 
end Something_Else; 

Something_Else не знает, что фактический тип Obj есть. Но все же можно быть уверенным, что если условие Pre'Class равно true, то может быть выполнено Operation (то есть оно удовлетворяет предварительным условиям). Если условие было всего Pre => [condition], то не могло быть гарантировано, что это сработает, потому что фактический тип Obj может быть производным, а Operation может быть переопределен для этого производного типа с более ограничительным условием и условием переопределения Operation будет проверен (после того как звонок будет отправит на переопределение Operation). С Pre'Class оба условия проверяются, и операция разрешена, если любое условие истинно (таким образом, производный тип может сделать вещи менее ограничительными). Но важно то, что Something_Else полагается на контракт, что если условие Pre'Class истинно, то допустимо Operation.

Однако ничто из этого не имеет значения, если Operation не может быть отменено. В вашем примере, поскольку параметр Valid равен Toto'Class, и поскольку (я предполагаю) Titi не является помеченным типом, Valid не является примитивной операцией и, следовательно, не является операцией диспетчеризации.

procedure Another_Procedure (Obj : Toto'Class; T : Titi) is 
begin 
    if Obj.Valid(T) then 
     ... 
    end if; 
end Another_Procedure; 

Когда Another_Procedure называет Valid, он всегда будет вызывать Valid, что вы написали; он никогда не отправит другому Valid, независимо от того, какой тип Obj на самом деле есть. Valid не является отправкой. Из-за этого нет смысла ставить на него класс. Поэтому язык запрещает это.

Примечание: В простом случае, когда имеется только тип основания и производного типа, не цепь типов, Pre'Class означает, что операция может быть выполнена, если условие или любое предварительное условие на производного типа преуспевает. Post'Class означает, что подпрограмма соответствует условию, если условие и выполнено в любом постусловии на производном типе.