!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) @drepl For a private type or private extension, the following language-defined aspects may be specified with an @fa (see 13.1.1): @dby For a private type, private extension, or interface, the following language-defined aspects may be specified with an @fa (see 13.1.1): !corrigendum 7.3.2(3/3) @drepl @xhang<@xterm This aspect shall be specified by an @fa, called an @i. Type_Invariant'Class may be specified on a @fa or a @fa.> @dby @xhang<@xterm This aspect shall be specified by an @fa, called an @i. Type_Invariant'Class may be specified on a @fa, a @fa, or a @fa 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. ****************************************************************