Version 1.5 of ai12s/ai12-0041-1.txt

Unformatted version of ai12s/ai12-0041-1.txt version 1.5
Other versions for file ai12s/ai12-0041-1.txt

!standard 7.3.2(1/3)          14-11-18 AI12-0041-1/03
!standard 7.3.2(3/3)
!class binding interpretation 14-10-19
!status Corrigendum 2015 14-11-17
!status WG9 Approved 15-06-26
!status ARG Approved 6-0-2 14-10-19
!status promising 11-0-0 13-11-16
!status work item 12-11-29
!status received 12-09-27
!priority Medium
!difficulty Easy
!subject Type_Invariant'Class for interface types
!summary
Allow specifying Type_Invariant'Class for interface types.
!question
Type_Invariant is used on a private type to define constraints on the implementation. As such, they are particularly useful when derivation is used as a means to interact with a component. The developer of a component can use a combination of Post'Class and Type_Invariant'Class to ensure that the contracts are correctly fulfilled by the client.
One very common pattern to provide these interactions between components is to use interfaces, which are much more flexible than abstract tagged types. Unfortunately, Type_Invariant'Class cannot be specified on an interface, thus limiting the capability in this context. In particular, the invariant will allow one to express the relation between primitives and / or the type and its environment.
!recommendation
Allow Type_Invariant'Class on interfaces. When a type implements one or several interfaces, its inherited type invariant would then be the conjunction of all ancestor Type_Invariant'Class.
!wording
7.3.2 Type Invariants
Modify 7.3.2(1/3):
For a private type{,}[ or] private extension,{ or interface,} the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Modify 7.3.2(3/3):
Type_Invariant'Class This aspect shall be specified by an expression, called an invariant expression. Type_Invariant'Class may be specified on a private_type_declaration{,}[ or] a private_extension_declaration{, or a full_type_declaration for an interface type}.
!discussion
The existing Dynamic Semantics that describes invariant checks works perfectly for interfaces; it does not need any changes.
Note that an abstract null record is very similar to an interface. We could allow them with no other changes. We didn't do this as it doesn't seem to add much to the language, and allowing components would cause problems (see next paragraph).
A bigger alternative would be to allow invariants on most non-private types. This idea was rejected during the development of Ada 2012 as it would allow invariants to be violated almost anywhere, rather than only within the defining package. (The protection offered by invariants is not quite complete, but it is close, and the programmer of the package can easily create abstractions that have no holes.) There is no good reason to revisit this decision (particularly so early in the life of Ada 2012 - the standard has been approved only for a few weeks as this is written).
Note that the problem of AI12-0042-1 appears to be related to this AI, but it isn't really related as it can happen whether or not interfaces allow invariants. The solution adopted for that AI will work for interfaces.
!example
-- This window should always display exactly 100 pixels
type Window is interface with Type_Invariant'Class => Window.Get_Width * Window.Get_Height = 100;
function Get_Width (This : Window) return Integer is abstract; function Get_Height (This : Window) return Integer is abstract;
!corrigendum 7.3.2(1/3)
Replace the paragraph:
For a private type or private extension, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
by:
For a private type, private extension, or interface, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
!corrigendum 7.3.2(3/3)
Replace the paragraph:
Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression. Type_Invariant'Class may be specified on a private_type_declaration or a private_extension_declaration.
by:
Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression. Type_Invariant'Class may be specified on a private_type_declaration, a private_extension_declaration, or a full_type_declaration for an interface type.
!ACATS test
ACATS C-Test(s) should be created to test that Type_Invariant'Class can be specified on interfaces, and extensions check the invariants appropriately.
!appendix

[Note: This topic was originally mixed into the mail that is filed in
AI12-0042-1, there is a small amount of discussion there.]

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

From: Tucker Taft
Sent: Thursday, September 27, 2012  3:56 PM

One of our engineers, Quentin Ochem, produced the following AI, about allowing
Type_Invariant'Class on an interface, and perhaps on an abstract null record
type as well.  It seems like a reasonable proposal.  See below.

-------------
* Problem in the standard *

While Type_Invariant'Class can be specified on private types as well as private
tagged types, it can't be specified on an interface - although interface
primitives can be associated with Post'Class. So the capabilities to specify
behavior constraints by the interface implementer are limited in comparison to
what would be possible on an abstract (private) type.

[Option 1]

An abstract type with a null record is pretty close to an interface, so it could
offer properties as close as possible to an interface and allow
Type_Invariant'Class in this case as well.

[Option 2]
Generally speaking, although the need is less clear, we could simplify the rule
even more by saying that Type_Invariant or Type_Invariant'Class is allowed on
any type declared immediately within the visible part of a package spec.

* Proposed solution *

The proposed solution is to allow Type_Invariant'Class on interfaces. When a
type implements one or several interfaces, its inherited type invariant would
then be the combination of all ancestor Type_Invariant'Class.

* Where to modify the reference manual *

7.3.2 Type Invariants

Modify 3/3

Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression.
Type_Invariant'Class may be specified on a private_type_declaration, a
private_extension_declaration **, or an interface_type_declaration**.

[Option 1]:
**, an interface_type_declaration, or the declaration of an abstract null record
type**.

Add 9/3

If a tagged type inherits from several invariants, coming from several
interfaces and tagged types, the resulting invariant is an expression combining
all the inherited invariant with an "and then" operator.

[Option 2]

Replace 2/3

Type_Invariant
This aspect shall be specified by an expression, called an invariant expression.
Type_Invariant may be specified on any type declared immediately within the
visible part of a package spec, with the exception of abstract types and
interfaces.

Replace 3/3

Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression.
Type_Invariant'Class may be specified on any tagged type or interface declared
immediately within the visible part of a package spec.

* Discussion / Rationale *

Type_Invariant is used on a private type to define constraints on the
implementation. As such, they are particularly useful when derivation is used as
a means to interact with a component. The developer of a component can use a
combination of Post'Class and Type_Invariant'Class to ensure that the contracts
are correctly fulfilled by the client.

One very common pattern to provide these interactions between components is to
use interfaces, which are much more flexible than abstract tagged types.
Unfortunately, Type_Invariant'Class cannot be specified on an interface, thus
limiting the capability in this context. In particular, the invariant will allow
one to express the relation between primitives and / or the type and its
environment.

* Example *

-- This window should always display exactly 100 pixels

type Window is interface
with Type_Invariant'Class => This.Get_Width * This.Get_Height = 100;

function Get_Width (This : Window) return Integer is abstract;
function Get_Height (This : Window) return Integer is abstract;

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

Editor's note, November  29, 2012

I put this proposal into the form of an Amendment AI, using the basic
outline of the original proposal.

I did not include option 2 in the AI, as he gives no justification for
abandoning the model of "clients are always properly checked", and that
was an important reason for the "only for private types" definition.
It's possible that experience might cause us to change the model at
some point in the future, but Ada 2012 is way too young (not even
published as of this writing) to be making major changes.

His suggestion to change 7.3.2(9/3) makes no sense, because the "invariant
check" already potentially includes multiple Type_Invariant'Class expressions
inherited from various ancestors. Indeed, no change is needed at all for
that.

Specifically, 7.3.2(8/3) says that a Type_Invariant'Class expression applies
to all descendants of a tagged type (which includes interfaces). (That's
formally defined in 13.1.1(29/3). Then 7.3.2(22/3) says that all invariant
expressions that apply are checked. (That makes sense, because a private
extension can have it's own Type_Invariant'Class along with any inherited
from its ancestor, even without interfaces.) How they combine is not
explicitly mentioned by 7.3.2(22/3), but surely it wouldn't be different
for interfaces.

Therefore, I conclude the only change needed here is to add
"interface_type_declaration" to the list of places where
aspect Type_Interface'Class is allowed. (This surprises the heck out of
me.) That's small enough that we could consider making this a Binding
Interpretation.

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

Editor's note, November  18, 2014

The wording was:

Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression.
Type_Invariant'Class may be specified on a private_type_declaration{,}[ or] a
private_extension_declaration{, or an interface_type_declaration}.

Unfortunately, there is no such thing as an "interface_type_declaration".
We have to use a longer-winded approach, either
"full_type_declaration for an interface type" or
"full_type_declaration that contains an interface_type_definition".

I used the former.

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

Questions? Ask the ACAA Technical Agent