[RFC] OOP - Dispatching

[QuentinOchem]

This RFC contains specific elements about the new dispatching syntax and semantics, coming from the overall OOP discussion.

[clairedross]

Very interesting. Do we really want to set the mode by default though ? This does not seem very user friendly to me.

[QuentinOchem]

Very interesting. Do we really want to set the mode by default though ? This does not seem very user friendly to me.

Not for Ada users compiling in legacy mode, we don't want to change the semantics implicitly. For people that adopt the new version of the language, yes. This does perform what people expect from dispatching, and does remove a known Ada vulnerability.

[clairedross]

As discussed live with Quentin, I am worried dispatching everywhere might remove the possibility to support OOP in SPARK. Basically, SPARK support of OOP is already quite rudimentary. It does not support many design patterns, because basically, when it proves something, it tries to prove it for all possible derived types with all possible overriding primitives. So what you can do is (1) prove subprograms using dispatching for all possible derived types using the provided classwide contracts (2) prove specific subprograms where the tag is known for the object. These two usages are made possible by the specific handling of calls to primitive operations in classwide contracts in Ada. They are considered as dispatching calls on dispatching calls, which allows to handle (1), but when proving the contract itself, they call the function of the specific type (which changes when they are inherited) so SPARK can prove (2). Here is an example:

package P with SPARK_Mode is
   pragma Elaborate_Body;

   type Root is abstract tagged null record;
   function Is_Init (R : Root) return Boolean is abstract;
   function Is_Processed (R : Root) return Boolean is abstract;
   procedure Init (R : out Root) is abstract with
     Post'Class => Is_Init (R);
   procedure Process (R : in out Root) is abstract with
     Pre'Class  => Is_Init (R),
     Post'Class => Is_Processed (R);
   procedure Go (R : out Root) with
     Extensions_Visible,
     Post'Class => Is_Processed (Root'Class (R));

   type Child is new Root with record
      F : Integer;
   end record;
   function Is_Init (R : Child) return Boolean is (R.F >= 1);
   function Is_Processed (R : Child) return Boolean is  (R.F >= 0);
   procedure Init (R : out Child);
   procedure Process (R : in out Child);
end P;

package body P with SPARK_Mode is

   procedure Go (R : out Root) is
   begin
      Init (Root'Class (R));
      Process (Root'Class (R));
   end Go;

   procedure Init (R : out Child) is
   begin
      R.F := 1;
   end Init;

   procedure Process (R : in out Child) is
   begin
      R.F := R.F - 1;
   end Process;

end P;

The procedure Go can be proved because calls in the contracts of Init and Process are considered to be dispatching and the procedures Init and Process can be proved because they see the specific versions. Note that I wrote Go as a primitive here, just so we can see the explicit redispatch, but it would make more sense to use a parameter of type Root'Class as it is probably not meant to be overridden.

As I think I demonstrated, the special handling in classwide contracts is crucial for provability of OOP in SPARK. Arguably, the support of OOP in SPARK is already not that great, but I think it might still be worthwhile to try and salvage what we have. Requiring the use of "old" OOP for SPARK would still be possible of course, but it might make the gap between Ada and SPARK wider while we have been trying for years to reduce it.

[sttaft]

The approach that existing Ada takes where dispatching only occurs when parameters are of a class-wide type, gives the programmer control of where and when the level of indirection and dynamism of dispatching is used. A dispatching call is a more challenging thing to test and prove things about than a statically-bound call, so it should be a conscious choice.

Historically, Ada's approach was developed in response to concerns expressed by organizations (like Microsoft) who were supporting large, heavily object-oriented libraries (such as Microsoft Foundation Classes). They found that any use of dispatching calls from one primitive of a type to another created complex coupling. This coupling meant that if some but not all primitives were inherited by a derived type (subclass), then the details of the inter-primitive calls made by the inherited primitives, that might normally be considered private to the implementation of the type, become visible. That is, the user would be relying on an undocumented internal re-dispatch, from say an inherited "Print_Line" operation to an overridden "Print" primitive. Once users figure out these inter-primitive calls, they never want to see them change on new versions of the library, an expectation which could make maintenance quite difficult.

We recognized that such inter-primitive re-dispatching calls need to be documented, and hence should not be the default. For a case like Print_Line, in Ada the simplest solution is to have Print_Line take a class-wide parameter in the first place, which it then uses to dispatch to Print and New_Line, if that is the desired semantics. Print_Line then becomes a "class-wide operation" rather than a primitive, eliminating the potential confusion and the dangers of partial inheritance.

[manthonyaiello]

Let’s build on Claire’s comment above to make sure the proposed change to always dispatch won’t break not only SPARK, but potentially any Ada that uses postconditions on classes.

We’ll change Claire’s code as follows, and assume that this RFC has been implemented (i.e., we always dispatch, i.e., the ‘self’ parameter is always converted to a classwide).

package P with SPARK_Mode is
   pragma Elaborate_Body;

   type Root is abstract tagged null record;
   function Is_Init (Self : Root) return Boolean is abstract;
   procedure Init (Self : out Root) is abstract with
     Post => Self.Is_Init;

   type Child is new Root with record
      F : Integer;
   end record;
   function Is_Init (Self : Child) return Boolean is (Self.F >= 1);
   procedure Init (Self : out Child);

   type Grandchild is new Child with record
      G : Integer;
   end record;
   function Is_Init (Self : Grandchild) return Boolean is (Self'Super.Is_Init and Self.G >= 2);
   procedure Init (Self : out Grandchild);
end P;

package body P with SPARK_Mode is

   procedure Init (Self : out Child) is
   begin
      Self.F := 1;
   end Init;

   procedure Init (Self : out Grandchild) is
   begin
      Self'Super.Init;  -- This line results in a failed postcondition
      Self.G := 2;
   end Init;
end P;

The problem arises at the call to Self’Super.Init; in Grandchild. At the conclusion of Child.Init, the postcondition is evaluated and Is_Init is called. However, since we always dispatch and since Grandchild overrides Is_Init, we will call Grandchild.Is_Init at this point - which will be false, so the postcondition will fail.

It’s potentially problematic in general to call a superclass method that may call an overridden method - but there are ways to protect against it when needed (final, static, etc.). Here the way out of the box is not clear:

• we don’t want to mark Init as final
• we don’t want the call to Is_Init to be never-dispatching, because used outside of the postcondition, the dispatching behavior is likely to be expected.

Perhaps the solution is to make the postcondition on Root.Init specify non-dispatching?

   procedure Init (Self : out Root) is abstract with
     Post => Self.Is_Init'Static;  -- (or some other syntax)

[QuentinOchem]

Thanks for documenting the case @manthonyaiello

We had a live review with Claire on this, and indeed the idea is to provide a specific syntax. SPARK behavior is not only to have a static call on the parent Is_Init, it's also to replace it when inherited by the overridden version, if any. Initial wording suggested 'Specific as an attribute, which matches the SPARK denomination of that capability.