Ada Programming/Attributes/'Result

Description

Within a postcondition expression for F, denotes the return object of the function call for which the postcondition expression is evaluated.

Within a postcondition expression for F, denotes the return object of the function call for which the postcondition expression is evaluated. The type of this attribute is that of the result subtype of the function or access-to-function type except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result; in those cases the type of the attribute is described above as part of the Name Resolution Rules for Post'Class.

Example

F’Result return X