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.