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 2012, 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
package Logging with
  SPARK_Mode
is
   Max_Count : constant := 10_000;

   type Log_Count is range 0 .. Max_Count;

   type Log_Type is tagged private;

   function Log_Size (Log : Log_Type) return Log_Count;

   procedure Init_Log (Log : out Log_Type) with
     Post'Class => Log.Log_Size = 0;

   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;

private

   subtype Log_Index is Log_Count range 1 .. Max_Count;
   type Integer_Array is array (Log_Index) of Integer;

   type Log_Type is tagged record
      Log_Data : Integer_Array;
      Log_Size : Log_Count;
   end record;

   function Log_Size (Log : Log_Type) return Log_Count is (Log.Log_Size);

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
with Logging; use type Logging.Log_Count;

package Range_Logging with
  SPARK_Mode
is
   type Log_Type is new Logging.Log_Type with private;

   not overriding
   function Log_Min (Log : Log_Type) return Integer;

   not overriding
   function Log_Max (Log : Log_Type) return Integer;

   overriding
   procedure Init_Log (Log : out Log_Type) with
     Post'Class => Log.Log_Size = 0 and
                   Log.Log_Min = Integer'Last and
                   Log.Log_Max = Integer'First;

   overriding
   procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
     Pre'Class  => Log.Log_Size < Logging.Max_Count,
     Post'Class => Log.Log_Size = Log.Log_Size'Old + 1 and
                   Log.Log_Min = Integer'Min (Log.Log_Min'Old, Incr) and
                   Log.Log_Max = Integer'Max (Log.Log_Max'Old, Incr);

private

   type Log_Type is new Logging.Log_Type with record
     Min_Entry : Integer;
     Max_Entry : Integer;
   end record;

   function Log_Min (Log : Log_Type) return Integer is (Log.Min_Entry);
   function Log_Max (Log : Log_Type) return Integer is (Log.Max_Entry);

end 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: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

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:

1
2
3
4
5
6
7
8
9
with Logging; use Logging;

procedure Use_Logging (Log : out Log_Type) with
  SPARK_Mode
is
begin
   Log.Init_Log;
   Log.Append_To_Log (1);
end 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:

1
2
3
4
5
6
7
8
9
with Logging; use Logging;

procedure Use_Logging_Classwide (Log : out Log_Type'Class) with
  SPARK_Mode
is
begin
   Log_Type (Log).Init_Log;
   Log.Append_To_Log (2);
end Use_Logging_Classwide;

on which GNATprove issues an error during flow analysis:

use_logging_classwide.adb:3:34: info: initialization of "Log" proved
use_logging_classwide.adb:3:34: info: initialization of extension of "Log" proved
use_logging_classwide.adb:8:04: high: extension of "Log" is not initialized
use_logging_classwide.adb:8:04: info: initialization of "Log" proved

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.