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¶
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'Classis similar to the normal precondition.
The class-wide postcondition introduced by aspect
Post'Classis 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
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
Range_Logging.Append_To_Log respect the Liskov Substitution
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
Range_Logging need not be implemented, or available,
or in SPARK. It is sufficient that the specification of
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¶
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.
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¶
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
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
Append_To_Log, it can use the class-wide contract of
Logging.Append_To_Log for analyzing procedure
5.8.4. Dynamic Types and Invisible Components¶
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
Use_Logging which initializes parameter
Log and then updates
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;
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
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
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 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
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