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:

 1package Logging_No_Dispatch 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 private;
 9
10   function Log_Size (Log : Log_Type) return Log_Count;
11
12   procedure Init_Log (Log : out Log_Type) with
13     Post => Log_Size (Log) = 0;
14
15   procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
16     Pre  => Log_Size (Log) < Max_Count,
17     Post => Log_Size (Log) = Log_Size (Log)'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_No_Dispatch;

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

 1package Geometry with
 2  SPARK_Mode
 3is
 4   type Shape is tagged record
 5      Pos_X, Pos_Y : Float;
 6   end record;
 7
 8   function Valid (S : Shape) return Boolean is
 9     (S.Pos_X in -100.0 .. 100.0 and S.Pos_Y in -100.0 .. 100.0);
10
11   procedure Operate (S : in out Shape) with
12     Pre'Class => Valid (S);
13
14   procedure Set_Default (S : in out Shape) with
15     Post'Class => Valid (S);
16
17   procedure Set_Default_Repeat (S : in out Shape) with
18     Post'Class => Valid (S);
19
20   procedure Set_Default_No_Post (S : in out Shape);
21
22   type Rectangle is new Shape with record
23      Len_X, Len_Y : Float;
24   end record;
25
26   function Valid (S : Rectangle) return Boolean is
27     (Valid (Shape (S)) and S.Len_X in 0.0 .. 10.0 and S.Len_Y in 0.0 .. 10.0);
28
29   procedure Operate (S : in out Rectangle);
30
31   procedure Set_Default (S : in out Rectangle);
32
33   procedure Set_Default_Repeat (S : in out Rectangle) with
34     Post'Class => Valid (S);
35
36   procedure Set_Default_No_Post (S : in out Rectangle) with
37     Post'Class => Valid (S);
38
39end 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:

 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:8:13

 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:26:13

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

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

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

 1with Geometry; use Geometry;
 2
 3procedure Use_Geometry (S : in out Shape'Class) with
 4  SPARK_Mode
 5is
 6begin
 7   S.Set_Default;
 8   S.Operate;
 9
10   S.Set_Default_Repeat;
11   S.Operate;
12
13   S.Set_Default_No_Post;
14   S.Operate;
15end Use_Geometry;

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

 info: precondition proved
--> use_geometry.adb:8:05

 info: precondition proved
--> use_geometry.adb:11:05

 medium: precondition might fail
--> use_geometry.adb:14:05
   14 |       S.Operate;
      |       ~^~~~~~~~
      + possible fix: call at line 13 should mention S (for argument S) in a postcondition
   13 |       S.Set_Default_No_Post;
      |        ^
 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:9:13

 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:31:13

 info: class-wide postcondition is stronger than overridden one
--> geometry.ads:44:20

 info: class-wide postcondition is stronger than overridden one
--> geometry.ads:49:20

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:

 1with Geometry; use Geometry;
 2
 3procedure More_Use_Geometry (S1, S2, S3, S4 : in out Shape'Class) with
 4  SPARK_Mode,
 5  Pre => S1.Valid
 6is
 7begin
 8   S1.Operate;
 9
10   if S2.Valid then
11      S2.Operate;
12   end if;
13
14   S3.Set_Default;
15   S3.Operate;
16
17   S4.Operate;
18end 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:

 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:9:13

 info: implicit aspect Always_Terminates on "Valid" has been proved, subprogram will terminate
--> geometry.ads:31:13

 info: class-wide postcondition is stronger than overridden one
--> geometry.ads:43:20

 info: class-wide postcondition is stronger than overridden one
--> geometry.ads:47:20
 info: precondition proved
--> more_use_geometry.adb:8:06

 info: precondition proved
--> more_use_geometry.adb:11:09

 info: precondition proved
--> more_use_geometry.adb:15:06

 medium: precondition might fail
--> more_use_geometry.adb:17:06
   17 |       S4.Operate;
      |       ~~^~~~~~~~
      + possible fix: precondition of subprogram at line 3 should mention S4
    3 |    procedure More_Use_Geometry (S1, S2, S3, S4 : in out Shape'Class) with
      |    ^