High-integrity object-oriented programming with Ada - Part 3

Ada 2012 Features
The example below illustrates these Ada 2012 features. The type Table is a tagged type serving as the root of an inheritance hierarchy, corresponding to a fixed-length data structure with operations Insert and Remove. Inserting the same element multiple times is allowed; removing an element removes all occurrences of the element. The Table type can be extended to provide a variety of representations, with corresponding implementations of Insert and Remove. The example shows a specific derived type, Nonduplicated_Table, which maintains the invariant that no element occurs more than once. For simplicity, elements in the table are integer values in the range zero through one million. In practice the example would be expressed as a generic package to make it more reusable—Element_Type would then be a formal type parameter.

package Tables is

  Max_Length : constant Integer := 100;
  type Element_Type is range 0 .. 1_000_000; -- New integer type

  subtype Length_Range is Integer range 0 .. Max_Length;
  subtype Index_Range  is Integer range 1 .. Max_Length;

  type Table is tagged private;

  procedure Insert (T : in out Table;
                    E : in Element_Type) with
    Pre'Class  => Allows_Insert (T, E),
    Post'Class =>
      ( Length (T) >= Length (T'Old) ) and
      ( Is_In (T, E ) and
      ( for all J in 1 .. Length (T'Old) => Is_In (T, Element_At (T'Old, J)) ));

  procedure Remove (T : in out Table; E : in Element_Type) with
    Pre'Class  => Allows_Remove (T, E),
    Post'Class =>
     ( Length (T) < Length (T'Old) ) and
     ( not Is_In (T, E) ) and
     ( for all J in 1 .. Length (T) => Is_In (T'Old, Element_At (T, J) ));
    -- Postcondition implies that all occurrences of E are removed from T

  function Length (T : Table) return Length_Range;

  function Element_At (T : Table; I : Index_Range) return Element_Type with
    Pre'Class => I <= Length (T);

  function Is_In (T : Table; E : Element_Type) return Boolean;

  function Allows_Insert (T : Table; E : Element_Type) return Boolean
    is ( Length (T) < Max_Length ); -- Ada 2012 expression function

  function Allows_Remove (T : Table; E : Element_Type ) return Boolean
    is ( Is_In (T, E) );            -- Ada 2012 expression function

private
  type Element_Array is array (1..Max_Length) of Element_Type;
  type Table is tagged record
     Length : Length_Range := 0;
     Data   : Element_Array;
  end record;
end Tables;


package Tables.Nonduplicated is

  type Nonduplicated_Table is new Table with private
  with
    Invariant'Class => -- No two elements equal
      ( for all J in 1 .. Length (Nonduplicated_Table) - 1 =>
         ( for all K in J+1 .. Length (Nonduplicated_Table) =>
            ( Element_At (Nonduplicated_Table, J) /=
              Element_At (Nonduplicated_Table, K)) ));


  overriding
  procedure Insert (T : in out Nonduplicated_Table; E : in Element_Type);

  overriding
  function Allows_Insert (T : Nonduplicated_Table;
                          E : Element_Type) return Boolean
     is (Tables.Allows_Insert (Table(T), E) and not Is_In (T, E));

  overriding
  procedure Remove (T : in out Nonduplicated_Table; E : in Element_Type);

  -- Allows_Remove is inherited from Tables
private
  type Nonduplicated_Table is new Table with null record;
end Tables.Nonduplicated;

The LSP-inspired rule against strengthening a precondition presents a paradox. Since inheritance as specialization generally constrains the value space of the original class, the subclass’s operations would typically impose stronger preconditions than the superclass’s. In the example shown, Insert(T, E) for a Nonduplicated_Table T requires that E is not already present in T, but this condition is not needed by Insert for the parent class Table. A solution is to express the precondition as a dynamically dispatching Boolean function—here Allows_Insert —that is appropriately adapted (in fact strengthened) by Nonduplicated_Table. Since the program’s interface to checking the precondition is the same for both parent type and derived type, despite differing implementation, it may be argued that LSP is preserved.

The precondition for the Remove operation is the same for Table and for Nonduplicating_Table and is captured by the Allows_Remove function.

The post condition can be expressed more specifically than the preconditions, to reflect the basic semantics of insertion and removal. The type invariant is an implicit post condition for each operation, and-ed with the inherited post condition.

The notation Pre'Class and Post'Class for the various pre- and post conditions aspects indicates that these are to be inherited by descendant types (which may add further conditions).