Version 1.3 of ai12s/ai12-0014-1.txt

Unformatted version of ai12s/ai12-0014-1.txt version 1.3
Other versions for file ai12s/ai12-0014-1.txt

!standard 6.1.1(0/3)          11-12-21 AI12-0014-1/01
!class Amendment 11-12-21
!status No Action (8-0-1) 15-06-28
!status work item 11-12-21
!status received 11-11-11
!priority Low
!difficulty Medium
!subject Postconditions on subprogram bodies
It makes sense to include preconditions and postconditions in a body of a subprogram, using information that is not to be visible to clients (such as objects declared in the package body).
A body precondition can easily be modeled with an assert pragma, but a body postcondition cannot because of the 'Old and 'Result attributes and the possibility of multiple exits from a subprogram.
It is best to keep contract things conceptually separated from other proof aids, as the contract things are intended to be visible to callers and other kinds of assertions are not. Thus, we don't want to call these things "postconditions". Therefore, we are proposing to allow aspects Assert_on_Entry and Assert_on_Exit on subprogram bodies, and allow the 'Old and 'Result attributes in the latter. The aspects would be evaluated as described and always belong to the actual subprogram body invoked (they're never inherited into a new body).
** TBD.
As noted in the proposal, Assert_on_Exit is intended to be evaluated for any normal exit (not when an exception is raised, there is a separate proposal for exception contracts that include exception postconditions).
!ACATS test
** TBD.

Editor's note: The original e-mail thread that spawned this AI can be found in AI05-0267-1.
The subjects are intertwined with the topics addressed in that AI and there is no sensible
way to separate them.


Questions? Ask the ACAA Technical Agent