7.5. How to Write Object Oriented Contracts

Object Oriented Programming (OOP) may require the use of special Class-Wide Subprogram Contracts for dispatching subprograms, so that GNATprove can check Liskov Substitution Principle on every overriding subprogram.

7.5.1. Object Oriented Code Without Dispatching

In the special case where OOP is used without dispatching, it is possible to use the regular Subprogram Contracts instead of the special Class-Wide Subprogram Contracts.

For example, consider a variant of the Logging and Range_Logging units presented in Class-Wide Subprogram Contracts, where no dispatching is allowed. Then, it is possible to use regular preconditions and postconditions as contracts, provided Log_Type is publicly declared as an untagged private type in both units:

 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_No_Dispatch with
  SPARK_Mode
is
   Max_Count : constant := 10_000;

   type Log_Count is range 0 .. Max_Count;

   type Log_Type is private;

   function Log_Size (Log : Log_Type) return Log_Count;

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

   procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
     Pre  => Log_Size (Log) < Max_Count,
     Post => Log_Size (Log) = Log_Size (Log)'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_No_Dispatch;
 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
38
with Logging_No_Dispatch; use Logging_No_Dispatch;

package Range_Logging_No_Dispatch with
  SPARK_Mode
is
   type Log_Type is private;

   function Log_Size (Log : Log_Type) return Log_Count;

   function Log_Min (Log : Log_Type) return Integer;

   function Log_Max (Log : Log_Type) return Integer;

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

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

private

   type Log_Type is tagged record
     Log : Logging_No_Dispatch.Log_Type;
     Min_Entry : Integer;
     Max_Entry : Integer;
   end record;

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

   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_No_Dispatch;

7.5.2. Writing Contracts on Dispatching Subprograms

Whenever dispatching is used, the contract that applies in proof to a dispatching call is the class-wide contract, defined as the first one present in the following list:

  1. the class-wide precondition (resp. postcondition) attached to the subprogram
  2. or otherwise the class-wide precondition (resp. postcondition) being inherited by the subprogram from the subprogram it overrides
  3. or otherwise the default class-wide precondition (resp. postcondition) of True.

For abstract subprograms (on interfaces or regular tagged types), only a class-wide contract can be specified. For other dispatching subprograms, it is possible to specify both a regular contract and a class-wide contract. In such a case, GNATprove uses the regular contract to analyze static calls to the subprogram and the class-wide contract to analyze dispatching calls to the subprogram, and it checks that the specific contract is a refinement of the class-wide contract, as explained in Mixing Class-Wide and Specific Subprogram Contracts.

Let’s consider the various cases that may occur when overridding a subprogram:

 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
38
39
package Geometry with
  SPARK_Mode
is
   type Shape is tagged record
      Pos_X, Pos_Y : Float;
   end record;

   function Valid (S : Shape) return Boolean is
     (S.Pos_X in -100.0 .. 100.0 and S.Pos_Y in -100.0 .. 100.0);

   procedure Operate (S : in out Shape) with
     Pre'Class => Valid (S);

   procedure Set_Default (S : in out Shape) with
     Post'Class => Valid (S);

   procedure Set_Default_Repeat (S : in out Shape) with
     Post'Class => Valid (S);

   procedure Set_Default_No_Post (S : in out Shape);

   type Rectangle is new Shape with record
      Len_X, Len_Y : Float;
   end record;

   function Valid (S : Rectangle) return Boolean is
     (Valid (Shape (S)) and S.Len_X in 0.0 .. 10.0 and S.Len_Y in 0.0 .. 10.0);

   procedure Operate (S : in out Rectangle);

   procedure Set_Default (S : in out Rectangle);

   procedure Set_Default_Repeat (S : in out Rectangle) with
     Post'Class => Valid (S);

   procedure Set_Default_No_Post (S : in out Rectangle) with
     Post'Class => Valid (S);

end Geometry;

In package Geometry, a type Shape is derived in a type Rectangle. A function Shape.Valid defines what it is to be a valid shape. It is overridden by Rectangle.Valid which defines what it is to be a valid rectangle. Here, a valid rectangle is also a valid shape, but that need not be the case. Procedure Set_Default and its variants demonstrate the various configurations that can be found in practice:

  1. The overridden subprogram Shape.Set_Default defines a class-wide contract (here only a postcondition), which is inherited in the overriding subprogram Rectangle.Set_Default. By the semantics of Ada, the postcondition of Shape.Set_Default calls Shape.Valid, while the inherited postcondition of Rectangle.Set_Default calls Rectangle.Valid.
  2. Both the overridden subprogram Shape.Set_Default_Repeat and the overriding subprogram Rectangle.Set_Default_Repeat define a class-wide contract (here only a postcondition). Here, since the contract is simply repeated, this is equivalent to case 1 above of inheriting the contract: the postcondition of Shape.Set_Default_Repeat calls Shape.Valid, while the postcondition of Rectangle.Set_Default_Repeat calls Rectangle.Valid.
  3. Only the overriding subprogram Rectangle.Set_Default_No_Post defines a class-wide contract (here only a postcondition). The default class-wide postcondition of True is used for the overridden Shape.Set_Default_No_Post.

In case 1, the overriding subprogram satisfies Liskov Substitution Principle by construction, so GNATprove emits no check in that case. Note that this is not the same as saying that Shape.Set_Default and Rectangle.Set_Default have the same contract: here the two postconditions differ, as one calls Shape.Valid, while the other calls Rectangle.Valid.

In case 2, GNATprove checks that Liskov Substitution Principle is verified between the contracts of the overridden and the overriding subprograms. Here, it checks that the postcondition of Rectangle.Set_Default_Repeat is stronger than the postcondition of Shape.Set_Default_Repeat.

In case 3, GNATprove also checks that Liskov Substitution Principle is verified between the default contract of the overridden subprogram and the specified contract of the overriding subprograms. Here, only a postcondition is specified for Rectangle.Set_Default_No_Post, so it is indeed stronger than the default postcondition of Shape.Set_Default_No_Post.

Hence the results of GNATprove‘s analysis on this program:

geometry.ads:34:20: info: class-wide postcondition is stronger than overridden one
geometry.ads:37:20: info: class-wide postcondition is stronger than overridden one

Let’s consider now calls to these subprograms in procedure Use_Geometry:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
with Geometry; use Geometry;

procedure Use_Geometry (S : in out Shape'Class) with
  SPARK_Mode
is
begin
   S.Set_Default;
   S.Operate;

   S.Set_Default_Repeat;
   S.Operate;

   S.Set_Default_No_Post;
   S.Operate;
end Use_Geometry;

Here are the results of GNATprove‘s analysis on this program:

use_geometry.adb:8:05: info: precondition proved
use_geometry.adb:11:05: info: precondition proved
use_geometry.adb:14:05: medium: precondition might fail

Parameter S is of class-wide type Shape'Class, so it can be dynamically of both types Shape or Rectangle. All calls on S are dispatching. In this program, GNATprove needs to check that the precondition of the calls to Operate is satisfied. As procedures Shape.Set_Default and Shape.Set_Default_Repeat state precisely this condition in postcondition, the precondition to the calls to Operate that follow can be proved. As procedure Shape.Set_Default_No_Post has no postcondition, the precondition to the last call to Operate cannot be proved. Note that these proofs take into account both possible types of S, for example:

  • If S is dynamically a shape, then the call to Shape.Set_Default on line 7 ensures that Shape.Valid holds, which ensures that the precondition to the call to Shape.Operate is satisfied on line 8.
  • If S is dynamically a rectangle, then the call to Rectangle.Set_Default on line 7 ensures that Rectangle.Valid holds, which ensures that the precondition to the call to Rectangle.Operate is satisfied on line 8.

7.5.3. Writing Contracts on Subprograms with Class-wide Parameters

Subprograms with class-wide parameters are not in general dispatching subprograms, hence they are specified through regular Subprogram Contracts, not Class-Wide Subprogram Contracts. Inside the regular contract, calls on primitive subprograms of the class-wide parameters are dispatching though, like in the code. For example, consider procedure More_Use_Geometry which takes four class-wide parameters of type Shape'Class, which can all be dynamically of both types Shape or Rectangle:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
with Geometry; use Geometry;

procedure More_Use_Geometry (S1, S2, S3, S4 : in out Shape'Class) with
  SPARK_Mode,
  Pre => S1.Valid
is
begin
   S1.Operate;

   if S2.Valid then
      S2.Operate;
   end if;

   S3.Set_Default;
   S3.Operate;

   S4.Operate;
end More_Use_Geometry;

The precondition of More_Use_Geometry specifies that S1.Valid holds, which takes into account both possible types of S1:

  • If S1 is dynamically a shape, then the precondition specifies that Shape.Valid holds, which ensures that the precondition to the call to Shape.Operate is satisfied on line 8.
  • If S1 is dynamically a rectangle, then the precondition specifies that Rectangle.Valid holds, which ensures that the precondition to the call to Rectangle.Operate is satisfied on line 8.

Similarly, the test on S2.Valid on line 10 ensures that the precondition to the call to S2.Operate on line 11 is satisfied, and the call to S3.Set_Default on line 14 ensures through its postcondition that the precondition to the call to S3.Operate on line 15 is satisfied. But no precondition or test or call ensures that the precondition to the call to S4.Operate on line 17 is satisfied. Hence the results of GNATprove‘s analysis on this program:

more_use_geometry.adb:8:06: info: precondition proved
more_use_geometry.adb:11:09: info: precondition proved
more_use_geometry.adb:15:06: info: precondition proved
more_use_geometry.adb:17:06: medium: precondition might fail