guideline

The implementation of the dispatching operations of each type in a derivation class rooted in a tagged type T should conform to the expected semantics of the corresponding dispatching operations of the class-wide type T'Class.

The key point of both of the alternatives in the following example is that it must be possible to use the
class-wide type Transaction.Object'Class polymorphically without having to study the implementations of each of the types derived from the root type Transaction.Object. In addition, new transactions can be added to the derivation class without invalidating the existing transaction processing code. These are the important practical consequences of the design rule captured in the guideline:

with Database;
package Transaction is

   type Object (Data : access Database.Object'Class) is abstract tagged limited
      record
         Has_Executed : Boolean := False;
      end record;

   function Is_Valid (T : Object) return Boolean;
   -- checks that Has_Executed is False

   procedure Execute (T : in out Object);
   -- sets Has_Executed to True

   Is_Not_Valid : exception;

end Transaction;

The precondition of Execute(T) for all T in Transaction.Object'Class is that Is_Valid(T) is True. The postcondition is the T.Has_Executed = True. This model is trivially satisfied by the root type Transaction.Object.

Consider the following derived type:

with Transaction;
with Personnel;
package Pay_Transaction is
   type Object is new Transaction.Object with
      record
         Employee     : Personnel.Name;
         Hours_Worked : Personnel.Time;
      end record;
   function Is_Valid (T : Object) return Boolean;
   -- checks that Employee is a valid name, Hours_Worked is a valid
   -- amount of work time and Has_Executed = False
   procedure Has_Executed (T : in out Object);
   -- computes the pay earned by the Employee for the given Hours_Worked
   -- and updates this in the database T.Data, then sets Has_Executed to True
end Pay_Transaction;

The precondition for the specific operation Pay_Transaction.Execute(T) is that Pay_Transaction.Is_Valid(T) is True, which is the same precondition as for the dispatching operation Execute on the class-wide type. (The actual validity check is different, but the statement of the "precondition" is the same.) The postcondition for Pay_Transaction.Execute(T) includes T.Has_Executed = True but also includes the appropriate condition on T.Data for computation of pay.

The class-wide transaction type can then be properly used as follows:

type Transaction_Reference is access all Transaction.Object'Class;
type Transaction_List is array (Positive range <>) of Transaction_Reference;
procedure Process (Action : in Transaction_List) is
begin
   for I in Action'Range loop
   -- Note that calls to Is_Valid and Execute are dispatching
      if Transaction.Is_Valid(Action(I).all) then
         -- the precondition for Execute is satisfied
         Transaction.Execute(Action(I).all);
         -- the postcondition Action(I).Has_Executed = True is
         -- guaranteed to be satisfied (as well as any stronger conditions
         -- depending on the specific value of Action(I))
      else
         -- deal with the error
         ...
      end if;
   end loop;
end Process;

If you had not defined the operation Is_Valid on transactions, then the validity condition for pay computation (valid name and hours worked) would have to directly become the precondition for Pay_Transaction.Execute. But this would be a "stronger" precondition than that on the class-wide dispatching operation, violating the guideline. As a result of this violation, there would be no way to guarantee the precondition of a dispatching call to Execute, leading to unexpected failures.

An alternative resolution to this problem is to define an exception to be raised by an Execute operation when the transaction is not valid. This behavior becomes part of the semantic model for the class-wide type: the precondition for Execute(T) becomes simply True (i.e., always valid), but the postcondition becomes "either" the exception is not raised and Has_Executed = True "or" the exception is raised and Has_Executed = False. The implementations of Execute in all derived transaction types would then need to satisfy the new postcondition. It is important that the "same" exception be raised by "all" implementations because this is part of the expected semantic model of the class-wide type.

With the alternative approach, the above processing loop becomes:

procedure Process (Action : in Transaction_List) is
begin

   for I in Action'Range loop

    Process_A_Transaction:
      begin

         -- there is no precondition for Execute
         Transaction.Execute (Action(I).all);
         -- since no exception was raised, the postcondition
         -- Action(I).Has_Executed = True is guaranteed (as well as
         -- any stronger condition depending on the specific value of
         -- Action(I))

      exception
         when Transaction.Is_Not_Valid =>
            -- the exception was raised, so Action(I).Has_Executed = False

            -- deal with the error
            ...

      end Process_A_Transaction;

   end loop;

end Process;

rationale