Use Class-wide Pre/Post Contracts (OOP06)

Level \(\rightarrow\) Required

Category

Safety:: \(\checkmark\)
Cyber:: \(\checkmark\)

Goal

Maintainability:: \(\checkmark\)
Reliability:: \(\checkmark\)
Portability:
Performance:
Security:: \(\checkmark\)

Remediation \(\rightarrow\) Low

Verification Method \(\rightarrow\) GNATcheck rule: Specific_Pre_Post (builtin rule)

Reference

[AdaOOP2016] section 6.1.4

SPARK User's Guide, section 7.5.2

Description

For primitive operations of tagged types, use only class-wide pre/post contracts, if any.

The class-wide form of precondition and postcondition expresses conditions that are intended to apply to any version of the subprogram. Therefore, when a subprogram is derived as part of inheritance, only the class-wide form of those contracts is inherited from the parent subprogram, if any are defined. As a result, it only makes sense to use the class-wide form in this situation.

(The same semantics and recommendation applies to type invariants.)

Note: this approach will be required for OOP07 (Ensure Local Type Consistency).

Applicable Vulnerability within ISO TR 24772-2

6.42 Violations of the Liskov substitution principle or the contract model [BLP]

Applicable Common Weakness Enumeration

N/A

Noncompliant Code Example

   type Root_T is tagged null record;
   procedure Set_Name (X    : Root_T;
                       Name : String)
     with Pre => Name'length > 0;
   function Get_Name (X : Root_T) return String
     with Post => Get_Name'result'length > 0;

Compliant Code Example

   type Root_T is tagged null record;
   procedure Set_Name (X    : Root_T;
                       Name : String)
     with Pre'class => Name'length > 0;
   function Get_Name (X : Root_T) return String
     with Post'class => Get_Name'result'length > 0;

Notes

N/A