oop-dispatching: Does 'Specialized have an effect without Default_Dispatching_Calls?

[ronan-d]

The example in the 'Specialized section of the RFC doesn't have pragma Default_Dispatching_Calls. I looks to me that 'Specialized has no effect in this situation so the pragma might just be missing.

@QuentinOchem, should the example have pragma Default_Dispatching_Calls (On);?

[QuentinOchem]

I don't think Default_Disatching_Calls should have an effect on 'Specialized at all - as 'Specialized is specifically to ensure some kind of static call regardless of the situation. We can make that explicit in the example (showing that the result is the same no matter what the pragma is)

[ronan-d]

Thanks, that clears things up. I still don't understand fully the role of 'Specialized. I think it would be useful to have an example with two similar class-wide postconditions, one with 'Specialized and one without that's inadequate. Do you know of such an example?

(Side note: I'm not sure if the Self'Super.Init; call in the example is correct, it looks to me that Super.Init (a.k.a. Root.Init) is abstract.)

[QuentinOchem]

Indeed, the example is wrong, Root.Init should not be abstract - it should be null. Will fix.

In that example, if you dispatch instead of calling statically 'Specialized, you will always dispatch to an Init function that can't be satisfied from the point of call of the overriden Init. As a matter of fact (@swbaird can you confirm?) I believe this is today the default behavior in GNAT. What we're doing here is to (1) call it with a name and (2) change default (without Specialized) to be dispatching to match the rest of the behavior.

This is an issue that was drilled down quite a lot in the context of SPARK, @clairedross may have more details.

[swbaird]

I have much the same reaction as @ronan-d . What problem is this feature intended to address? I think an example illustrating both the problem and how the problem is addressed by this feature is needed.

But @QuentinOchem I think the answer to your question is "yes, that is what the RM already requires". RM 6.1.1 (37) says "Any operations within a class-wide postcondition expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the postcondition bound to the corresponding operations of the type identified by the controlling tag of the call on S.[ This applies to both dispatching and non-dispatching calls on S.]" To see what that notional type wording is referring to, see preceding paragraph 7 (in the name resolution section).

[QuentinOchem]

So to put things in order - we need to solve two issues at one: (1) all calls (under default dispatching calls, which is going to be On by default on some code configuration) are dispatching by default, including in pre and post. This is to have consistency across the code. And (2) the feature highlighted in the RM is important - I'm assuming we're not discussing that this is important? So the solution that we found to address these is to keep the RM behavior available on request through the 'Specialized attribute, and have all calls otherwise dispatching.