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.