5.8. Object Oriented Programming and Liskov Substitution Principle

SPARK supports safe Object Oriented Programming by checking behavioral subtyping between parent types and derived types, a.k.a. Liskov Substitution Principle: every overriding operation of the derived type should behave so that it can be substituted for the corresponding overridden operation of the parent type anywhere.

5.8.1. Class-Wide Subprogram Contracts

[Ada 2012]

Specific Subprogram Contracts are required on operations of tagged types, so that GNATprove can check Liskov Substitution Principle on every overriding operation:

  • The class-wide precondition introduced by aspect Pre'Class is similar to the normal precondition.

  • The class-wide postcondition introduced by aspect Post'Class is similar to the normal postcondition.

Although these contracts are defined in Ada, they have a stricter meaning in SPARK for checking Liskov Substitution Principle:

  • The class-wide precondition of an overriding operation should be weaker (more permissive) than the class-wide precondition of the corresponding overridden operation.

  • The class-wide postcondition of an overriding operation should be stronger (more restrictive) than the class-wide postcondition of the corresponding overridden operation.

For example, suppose that the Logging unit introduced in Ghost Packages defines a tagged type Log_Type for logs, with corresponding operations:

 1package Logging with
 2  SPARK_Mode
 3is
 4   Max_Count : constant := 10_000;
 5
 6   type Log_Count is range 0 .. Max_Count;
 7
 8   type Log_Type is tagged private;
 9
10   function Log_Size (Log : Log_Type) return Log_Count;
11
12   procedure Init_Log (Log : out Log_Type) with
13     Post'Class => Log.Log_Size = 0;
14
15   procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
16     Pre'Class  => Log.Log_Size < Max_Count,
17     Post'Class => Log.Log_Size = Log.Log_Size'Old + 1;
18
19private
20
21   subtype Log_Index is Log_Count range 1 .. Max_Count;
22   type Integer_Array is array (Log_Index) of Integer;
23
24   type Log_Type is tagged record
25      Log_Data : Integer_Array;
26      Log_Size : Log_Count;
27   end record;
28
29   function Log_Size (Log : Log_Type) return Log_Count is (Log.Log_Size);
30
31end Logging;

and that this type is derived in Range_Logging.Log_Type which additionally keeps track of the minimum and maximum values in the log, so that they can be accessed in constant time:

 1with Logging; use type Logging.Log_Count;
 2
 3package Range_Logging with
 4  SPARK_Mode
 5is
 6   type Log_Type is new Logging.Log_Type with private;
 7
 8   not overriding
 9   function Log_Min (Log : Log_Type) return Integer;
10
11   not overriding
12   function Log_Max (Log : Log_Type) return Integer;
13
14   overriding
15   procedure Init_Log (Log : out Log_Type) with
16     Post'Class => Log.Log_Size = 0 and
17                   Log.Log_Min = Integer'Last and
18                   Log.Log_Max = Integer'First;
19
20   overriding
21   procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
22     Pre'Class  => Log.Log_Size < Logging.Max_Count,
23     Post'Class => Log.Log_Size = Log.Log_Size'Old + 1 and
24                   Log.Log_Min = Integer'Min (Log.Log_Min'Old, Incr) and
25                   Log.Log_Max = Integer'Max (Log.Log_Max'Old, Incr);
26
27private
28
29   type Log_Type is new Logging.Log_Type with record
30     Min_Entry : Integer;
31     Max_Entry : Integer;
32   end record;
33
34   function Log_Min (Log : Log_Type) return Integer is (Log.Min_Entry);
35   function Log_Max (Log : Log_Type) return Integer is (Log.Max_Entry);
36
37end Range_Logging;

GNATprove proves that the contracts on Logging.Append_To_Log and its overriding Range_Logging.Append_To_Log respect the Liskov Substitution Principle:

range_logging.ads:9:13: info: implicit aspect Always_Terminates on "Log_Min" has been proved, subprogram will terminate
range_logging.ads:12:13: info: implicit aspect Always_Terminates on "Log_Max" has been proved, subprogram will terminate
range_logging.ads:16:20: info: class-wide postcondition is stronger than overridden one
range_logging.ads:22:20: info: class-wide precondition is weaker than overridden one
range_logging.ads:23:20: info: class-wide postcondition is stronger than overridden one
logging.ads:10:13: info: implicit aspect Always_Terminates on "Log_Size" has been proved, subprogram will terminate

Units Logging and Range_Logging need not be implemented, or available, or in SPARK. It is sufficient that the specification of Logging and Range_Logging are in SPARK for this checking. Here, the postcondition of Range_Logging.Append_To_Log is strictly stronger than the postcondition of Logging.Append_To_Log, as it also specifies the new expected value of the minimum and maximum values. The preconditions of both procedures are exactly the same, which is the most common case, but in other cases it might be useful to be more permissive in the overriding operation’s precondition. For example, Range_Logging.Append_To_Log could allocate dynamically additional memory for storing an unbounded number of events, instead of being limited to Max_Count events like Logging.Append_To_Log, in which case its precondition would be simply True (the default precondition).

A derived type may inherit both from a parent type and from one or more interfaces, which only provide abstract operations and no components. GNATprove checks Liskov Substitution Principle on every overriding operation, both when the overridden operation is inherited from the parent type and when it is inherited from an interface.

GNATprove separately checks that a subprogram implements its class-wide contract, like for a specific contract.

5.8.2. Mixing Class-Wide and Specific Subprogram Contracts

[Ada 2012]

It is possible to specify both a specific contract and a class-wide contract on a subprogram, in order to use a more precise contract (the specific one) for non-dispatching calls and a contract compatible with the Liskov Substitution Principle (the class-wide contract) for dispatching calls. In that case, GNATprove checks that:

  • The specific precondition is weaker (more permissive) than the class-wide precondition.

  • The specific postcondition is stronger (more restrictive) than the class-wide postcondition.

For example, Logging.Append_To_Log could set a boolean flag Special_Value_Logged when some Special_Value is appended to the log, and express this property in its specific postcondition so that it is available for analyzing non-dispatching calls to the procedure:

procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
  Pre'Class  => Log.Log_Size < Max_Count,
  Post'Class => Log.Log_Size = Log.Log_Size'Old + 1,
  Post       => Log.Log_Size = Log.Log_Size'Old + 1 and
                (if Incr = Special_Value then Special_Value_Logged = True);

This additional postcondition would play no role in dispatching calls, thus it is not involved in checking the Liskov Substitution Principle. Note that the absence of specific precondition on procedure Append_To_Log does not mean that the default precondition of True is used: as a class-wide precondition is specified on procedure Append_To_Log, it is also used as specific precondition. Similarly, if a procedure has a class-wide contract and a specific precondition, but no specific postcondition, then the class-wide postcondition is also used as specific postcondition.

When both a specific contract and a class-wide contract are specified on a subprogram, GNATprove only checks that the subprogram implements its specific (more precise) contract.

5.8.3. Dispatching Calls and Controlling Operands

[Ada 2012]

In a dispatching call, the controlling operand is the parameter of class-wide type whose dynamic type determinates the actual subprogram called. The dynamic type of this controlling operand may be any type derived from the specific type corresponding to the class-wide type of the parameter (the specific type is T when the class-wide type is T'Class). Thus, in general it is not possible to know in advance which subprograms may be called in a dispatching call, when separately analyzing a unit.

In SPARK, there is no need to know all possible subprograms called in order to analyze a dispatching call, which makes it possible for GNATprove to perform this analysis without knowledge of the whole program. As SPARK enforces Liskov Substitution Principle, the class-wide contract of an overriding operation is always less restrictive than the class-wide contract of the corresponding overridden operation. Thus, GNATprove uses the class-wide contract of the operation for the specific type of controlling operand to analyze a dispatching call.

For example, suppose a global variable The_Log of class-wide type defines the log that should be used in the program:

The_Log : Logging.Log_Type'Class := ...

The call to Append_To_Log in procedure Add_To_Total may dynamically call either Logging.Append_To_Log or Range_Logging.Append_To_Log:

procedure Add_To_Total (Incr : in Integer) is
begin
   Total := Total + Incr;
   The_Log.Append_To_Log (Incr);
end Add_To_Total;

Because GNATprove separately checks Liskov Substitution Principle for procedure Append_To_Log, it can use the class-wide contract of Logging.Append_To_Log for analyzing procedure Add_To_Total.

5.8.4. Dynamic Types and Invisible Components

[SPARK]

The Data Initialization Policy in SPARK applies specially to objects of tagged type. In general, the dynamic type of an object of tagged type may be different from its static type, hence the object may have invisible components, that are only revealed when the object is converted to a class-wide type.

For objects of tagged type, modes on parameters and data dependency contracts have a different meaning depending on the object’s static type:

  • For objects of a specific (not class-wide) tagged type, the constraints described in Data Initialization Policy apply to the visible components of the object only.

  • For objects of a class-wide type, the constraints described in Data Initialization Policy apply to all components of the object, including invisible ones.

GNATprove checks during flow analysis that no uninitialized data is read in the program, and that the specified data dependencies and flow dependencies are respected in the implementation, based on the semantics above for objects of tagged type. For example, it detects no issues during flow analysis on procedure Use_Logging which initializes parameter Log and then updates it:

1with Logging; use Logging;
2
3procedure Use_Logging (Log : out Log_Type) with
4  SPARK_Mode
5is
6begin
7   Log.Init_Log;
8   Log.Append_To_Log (1);
9end Use_Logging;

If parameter Log is of dynamic type Logging.Log_Type, then the call to Init_Log initializes all components of Log as expected, and the call to Append_To_Log can safely read those. If parameter Log is of dynamic type Range_Logging.Log_Type, then the call to Init_Log only initializes those components of Log that come from the parent type Logging.Log_Type, but since the call to Append_To_Log only read those, then there is no read of uninitialized data. This is in contrast with what occurs in procedure Use_Logging_Classwide:

1with Logging; use Logging;
2
3procedure Use_Logging_Classwide (Log : out Log_Type'Class) with
4  SPARK_Mode
5is
6begin
7   Log_Type (Log).Init_Log;
8   Log.Append_To_Log (2);
9end Use_Logging_Classwide;

on which GNATprove issues a check message during flow analysis:


use_logging_classwide.adb:8:04: high: extension of "Log" is not initialized
    8 |   Log.Append_To_Log (2);

Indeed, the call to Init_Log (a non-dispatching call to Logging.Init_Log due to the conversion on its parameter) only initializes those components of Log that come from the parent type Logging.Log_Type, but the call to Append_To_Log may read other components from Range_Logging.Log_Type which may not be initialized.

A consequence of these rules for data initialization policy is that a parameter of a specific tagged type cannot be converted to a class-wide type, for example for a dispatching call. A special aspect Extensions_Visible is defined in SPARK to allow this case. When Extensions_Visible is specified on a subprogram, the data initialization policy for the subprogram parameters of a specific tagged type requires that the constraints described in Data Initialization Policy apply to all components of the object, as if the parameter was of a class-wide type. This allows converting this object to a class-wide type.