Version 1.2 of ai12s/ai12-0273-1.txt

Unformatted version of ai12s/ai12-0273-1.txt version 1.2
Other versions for file ai12s/ai12-0273-1.txt

!standard 12.6(8.9/5)          18-04-09 AI12-0273-1/00
!class Amendment 18-04-09
!status Hold by Letter Ballot (10-0-1) - 18-05-07
!status work item 18-04-09
!status received 18-04-05
!priority Very_Low
!difficulty Medium
!subject Contract matching for formal subprograms
!summary
** TBD.
!problem
Ada has a strong "contract model" for generic units, which makes it possible to reason about generic bodies without knowing anything about the properties of the actual types.
This model is fairly weak for formal subprograms, where even the subtypes of the subprogram profile are ignored. This can make it hard to reason in generic bodies. AI12-0272-1 partially mitigated this problem by allowing Pre/Post for generic formal subprograms.
However, those are purely dynamic checks. This introduces a "tripping hazard", where a mismatch between the formal and actual subprogram can cause Assertion_Error failures much later (on calls to the formal subprogram).
Typically, we leave problems like this to static checking tools. However, most static analysis programs treat generics as macros and takee no advantage of the Ada contract model. Thus it falls to Ada to provide a solution.
!proposal
This proposal assumes that AI12-0272-1 has been incorporated into Ada.
We add an aspect Match_Contract for generic formal subprograms. When this is True, additional matching rules are applied to the actual subprogram:
* the profile of the actual subprogram must subtype conform to that of the
formal subprogram;
* the precondition of the actual subprogram must be *weaker* than the
precondition of the formal subprogram;
* the postcondition of the actual subprogram must be *stronger* than the
postcondition of the formal subprogram.
We could use various mechanisms to determine whether the preconditions/ postconditions are weaker or stronger.
A particularly simple one that would work for most real-world usages is: (1) For each precondition of a subprogram, take all of the precondition expressions that apply to the subprogram, combining them appropriately (usually with "or" or "and"); giving expression PrAll. (2) Split the large PrAll expression into a set of subexpressions SPr that are combined by top-level "or" or "or else". Do this recursively until all of the top-level of each subexpression is not "or" or "or else". (3) If any of the subexpressions in the set SPr are the constant "True", then replace the entire set SPr with the empty set. Discard any subexpressions in SPr that are constant "False". (4) Then, for each subexpression in the set SPr for the actual subprogram, there must be a conforming subexpression in the set SPr for the formal subprogram. [Careful: the reverse doesn't need to be true!] If this is True, then the precondition of the actual is weaker than the precondition of the formal.
A similar set of operations is performed for the postcondition check:
(5) For each postcondition of a subprogram, take all of the postcondition expressions that apply to the subprogram, combining them appropriately (usually with "and"); giving expression PoAll. (6) Split the large PoAll expression into a set of subexpressions SPo that are combined by top-level "and" or "and then". Do this recursively until all of the top-level of each subexpressions is not "and" or "and then". (7) If any of the subexpressions in the set SPo are the constant "False", then replace the entire set SPo with the empty set. Discard any subexpressions in SPo that are constant "True". (8) Then, for each subexpression in the set SPo for the formal subprogram, there must be a conforming subexpression in the set SPo for the actual subprogram. If this is True, then the postcondition of the actual is stronger than the postcondition of the formal.
Here, "full conformance" is enhanced as always to treat corresponding parameters of the two subprograms to "conform". (Otherwise, nothing would match.)
We could also go a bit further and allow conformance to allow swapping of operands to "and" and "or" (and other predefined operators other than "-" and "/"??) This latter extension isn't particularly important.
This set of rules allows any exact matching Pre or Post, trivially weaker/stronger Pre/Post (especially "True"), and additional cases that are likely through inheritance. It doesn't apply the full possibilities of synbolic logic, but that seems out of bounds for the Ada language.
!wording
** TBD.
!discussion
Note that sometimes we want to be as liberal as possible with generic parameters; matching is easier for predicate functions (for one example) if one doesn't need to exactly match all of the subtypes. The weaker matching makes a generic more generally applicable.
However, if the programmer doesn't want that applicability and want a proper match, there isn't any way to get it currently.
One could imagine having a similar mechanism for 'Access for access-to-subprogram types. Again, whether detailed matching is desired depends on the programmer and what other tools they plan to use. If matching is defined for generics, we could use essentially the same wording for 'Access. (Note that 'Access does use subtype conformance by default, so it isn't quite so loose as generic formal subprograms -- but there is no contract matching.)
** TBD.
!ASIS
[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

****************************************************************


Questions? Ask the ACAA Technical Agent