CODEWITHSUNDEEP
ada
user2302725
user2302725

Reputation: 473

ADA - precondition in 'class

I'm trying to compile this code :

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

GNAT says "aspect "pre'class" can only be specified for a primitive operation of a tagged private"

I guess it's because of the Toto'Class but how could I make it work ?

Upvotes: 0

Views: 329

Answers (1)

ajb
ajb

Reputation: 31689

The purpose of Pre'Class and Post'Class, I believe, is to specify preconditions that apply even when a subprogram is overridden.

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

What this means is that if the condition is met, then Operation is allowed, even if derived types impose other conditions. Suppose a procedure uses this operation on a Base_Type'Class object:

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

Something_Else doesn't know what the actual type of Obj is. But it can still be assured that if the Pre'Class condition is true, then Operation can be performed (i.e. it satisfies the preconditions). If the condition were just Pre => [condition], it could not be assured that this would work, because Obj's actual type could be a derived type, and Operation could be overridden for that derived type with a more restrictive condition, and the condition on the overriding Operation would be the one that is checked (since the call would dispatch to the overriding Operation). With Pre'Class, both conditions are checked, and the operation is allowable if either condition is true (thus a derived type can make things less restrictive). But the important thing is that Something_Else is relying on the contract that, if the Pre'Class condition is true, then Operation is allowable.

However, none of this matters if Operation can't be overridden. In your example, since Valid's parameter is Toto'Class, and since (I assume) Titi is not a tagged type, Valid is not a primitive operation and therefore is not a dispatching operation. 

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

When Another_Procedure calls Valid, it will always call the Valid that you wrote; it will never dispatch to a different Valid, no matter what type Obj actually is. Valid is not a dispatching function. Because of that, there's no point in putting a class-wide precondition on it. So the language disallows it.

Note: In a simple case where there is just a base type and a derived type, not a chain of types, Pre'Class means that an operation can be performed if the condition or any precondition on the derived type succeeds. Post'Class means that a subprogram meets the condition if the condition and any postcondition on the derived type succeed.

Upvotes: 3

Related Questions