!standard 7.3.2(2-3/3) 17-10-05 AC95-00296/00 !class Amendment 17-10-05 !status received no action 17-10-05 !status received 17-09-12 !subject Support type invariants for null type extensions !summary !appendix !topic Support type invariants for null type extensions !reference Ada 2012 RM7.3.2(2/3-3/3) !from Victor Porton 17-09-12 !keywords type invariants, private types, null type extensions !discussion I propose to change: Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration that declares the completion of a private type or private extension. to Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, null_extension_declaration, or on a full_type_declaration that declares the completion of a private type or private extension. that is to allow type invariants with null extensions. A practical example (a little rewritten real code): -- It may be either boolean result or graph result type RDF_Query_Results is tagged private; function Is_Boolean (Results: RDF_Query_Results); function Is_Graph (Results: RDF_Query_Results); type Boolean_RDF_Query_Results is new RDF_Query_Results with null record with Type_Invariant'Class => Is_Boolean(Boolean_RDF_Query_Results); type Graph_RDF_Query_Results is new RDF_Query_Results with null record with Type_Invariant'Class => Is_Graph(Graph_RDF_Query_Results); This would allow to create something like subtypes for reliably detecting the correct object type. No need to say that this increases reliability. I remind, that having null extension instead of private extension simplifies constructing objects of the type. And there is no reason which would make this hard to implement. If it works with private extensions, it would work with no problems with null extensions. *************************************************************** From: Egil Harald Hoevik Sent: Tuesday, September 12, 2017 6:40 AM > This would allow to create something like subtypes for reliably > detecting the correct object type. > > No need to say that this increases reliability. Foo : RDF_Query_Results'Class := Some_Factory_Function; begin if Foo in Boolean_RDF_Query_Results'Class then -- Foo is Boolean here... elsif Foo in Graph_RDF_Query_Results'Class then -- Foo is Graph here end if; end; I'd say this is readable enough. ************************************************************** From: Victor Porton Sent: Saturday, September 30, 2017 4:34 PM My proposal is about AUTOMATIC bug detection. Your code does not do this. ************************************************************** From: Randy Brukardt Sent: Monday, October 2, 2017 2:30 PM > -- It may be either boolean result or graph result type > RDF_Query_Results is tagged private; > > function Is_Boolean (Results: RDF_Query_Results); function Is_Graph > (Results: RDF_Query_Results); > > type Boolean_RDF_Query_Results is new RDF_Query_Results > with null record > with Type_Invariant'Class => Is_Boolean(Boolean_RDF_Query_Results); > > type Graph_RDF_Query_Results is new RDF_Query_Results > with null record > with Type_Invariant'Class => Is_Graph(Graph_RDF_Query_Results); > > This would allow to create something like subtypes for reliably > detecting the correct object type. You can use Dynamic_Predicates for this: type Boolean_RDF_Query_Results is new RDF_Query_Results with null record with Dynamic_Predicate => Is_Boolean(Boolean_RDF_Query_Results); type Graph_RDF_Query_Results is new RDF_Query_Results with null record with Dynamic_Predicate => Is_Graph(Graph_RDF_Query_Results); Moreover, you can write these as subtypes using a dynamic predicate, which usually is better (as it avoids unnecessary conversions): subtype Boolean_RDF_Query_Results is RDF_Query_Results with Dynamic_Predicate => Is_Boolean(Boolean_RDF_Query_Results); subtype Graph_RDF_Query_Results is RDF_Query_Results with Dynamic_Predicate => Is_Graph(Graph_RDF_Query_Results); A Type_Invariant is only checked at package boundaries and is inappropriate for types with potentially visible components, and really are inappropriate for any type that might not be declared in a package. (Indeed, I wanted to require checks to prevent type invariants from even being inherited to non-private types, but the full group decided to not check and just strongly suggest that users not do that, mainly because of the extra complexity of the Legality Rules needed.) Moreover, type invariants have a number of holes in the checking that can only be mitigated in a package specification. Type_Invariants are rarely used, as they have to apply to all objects of a type. A predicate is much more likely to be useful, as they can apply to just a subset of objects as needed. Secondly (and this is a personal opinion not shared by all), it is evil to provide a capability for a null extension and not provide the same capability for record extensions. My personal programming style is to create a new extension using a null extension and then to add components as they become needed during implementation. In this style, extra capabilities provided by a null extension suddenly become unavailable when a component is added, preventing smooth incremental development (the only sane kind of development, IMHO). In any case, if you want us to seriously consider this proposal, we need to know why Dynamic_Predicates are not sufficient to solve the problem (they clearly are in the example you gave, and are preferable since they are checked in more places). ************************************************************** From: Victor Porton Sent: Monday, October 2, 2017 2:40 PM I've realized that I am not well informed about type predicates and their design rationale: Why there are both Type_Invariant and Dynamic_Predicate? Why not use Type_Invariant never and use always Dynamic_Predicate instead? ************************************************************** From: Randy Brukardt Sent: Monday, October 2, 2017 3:03 PM > I've realized that I am not well informed about type predicates and > their design rationale: > > Why there are both Type_Invariant and Dynamic_Predicate? In hindsight, I have no idea. :-) There is such a thing in static proving languages, and it was thought Ada needed it too. But it doesn't seem to. > Why not use Type_Invariant never and use always Dynamic_Predicate > instead? Yes, that's what I'd recommend. The number of cases where you have a condition that you want to apply to all objects of a type are rare enough that a separate feature for that case isn't worth the effort (to define, to learn, etc.). (And this one has been a LOT of effort.) Type_Invariants have class-wide inheritance, but it's unclear if that is really useful. And once a predicate has been applied to a subtype, it will apply to any later subtypes derived from the original, so it also effectively inherits. ************************************************************** From: Tucker Taft Sent: Monday, October 2, 2017 2:56 PM A type invariant can be violated while inside the package defining the type. The invariant is re-checked on leaving the "boundary" provided by the package. On the other hand, a subtype predicate is checked everywhere that subtype is used. A type-invariant is equivalent to "sprinkling" a requirement into the pre- and post-conditions of every "boundary" subprogram (typically the primitive subprograms) of a package, essentially saying that the invariant will be true on exit from a subprogram, if it was true on entry. A subtype predicate, on the other hand, is checked at every point where an object of that subtype is assigned a new value (no matter where it occurs), so is not particularly appropriate for properties that are preserved by primitive operations, but not preserved at intermediate points inside the operation. Type invariants are often defined in terms of internal properties of a type (e.g. of a stack, it might talk about which values of the underlying array must be initialized), while subtype predicates are generally defined in terms of the external properties of a type, and generally are used to characterize an interesting subset of all possible values of the type. As Randy mentioned, both have holes as far as run-time checking, but tools like our SPARK toolset enforce the invariant or subtype predicate more completely at compile time. Doing full run-time checking, particularly for dynamic predicates on composite types, was felt too expensive under certain circumstances. You could add explicit "pragma Assert(X in Subtype_With_Predicate)" at crucial points if you wanted to. ************************************************************** From: Steve Baird Sent: Monday, October 2, 2017 3:40 PM >> Why there are both Type_Invariant and Dynamic_Predicate? > In hindsight, I have no idea.:-) A type invariant can be temporarily violated inside the implementation of the private type. Consider an implementation of some sort of balanced tree data structure which is declared as a private type. The outside world should never see an unbalanced tree, but midway through some tree insertion operation it is ok for a tree to be temporarily unbalanced. ************************************************************** From: Randy Brukardt Sent: Monday, October 2, 2017 4:00 PM > A type invariant can be temporarily violated inside the implementation > of the private type. The need to do that shows exactly why the concept is unnecessary. :-) > Consider an implementation of some sort of balanced tree data > structure which is declared as a private type. > > The outside world should never see an unbalanced tree, but midway > through some tree insertion operation it is ok for a tree to be > temporarily unbalanced. You can easily do this with predicates, simply by having the type have no redicate and using a subtype with a predicate for all public interaction (that is, parameter declarations). Indeed, that's the normal case for using predicates (no predicate on the type, some predicate on one or more subtypes used for parameter and/or component declarations). In this case, the predicate would require the tree to be balanced. Operations within the package using the raw type would not require balancing. You could almost emulate the entire Type_Invariant mechanism with that sort of predicate (without the many pages of rules needed for Type_Invariant), using the subtype to complete the private type. (Some details would be different.) In hindsight, that would have been a much better plan; it would have left us a lot more time to work on things that are actually useful. ************************************************************** From: Tucker Taft Sent: Monday, October 2, 2017 4:28 PM I don't agree. The notion of Type_Invariant is fundamental to many abstractions. Yes you can emulate much of it using Subtype_Predicates, but that is perverting both notions, in my view. Note that at one point Steve suggested implementing Type_Invariants by implicitly using Subtype_Predicates in the compiler, and in addition to introducing some unanticipated complexity in certain cases, it simply muddied the waters to what is a well-known concept in the formal methods community. Also, I believe in most cases Type_Invariants should be private to the abstraction, while Subtype_Predicates generally have to be visible. In many cases, a Type_Invariant is exactly the extra stuff you need to add to the visible pre- and post-conditions to allow them to be provable for a given implementation of an abstraction. ************************************************************** From: Randy Brukardt Sent: Monday, October 2, 2017 4:40 PM > I don't agree. The notion of Type_Invariant is fundamental to many > abstractions. Yes you can emulate much of it using > Subtype_Predicates, but that is perverting both notions, in my view. > Note that at one point Steve suggested implementing Type_Invariants by > implicitly using Subtype_Predicates in the compiler, and in addition > to introducing some unanticipated complexity in certain cases, it > simply muddied the waters to what is a well-known concept in the > formal methods community. This is where we went wrong, in my view. Yes, the "formal methods community" has such a concept, but it really is not very useful if you have predicates. And for me, at least, predicates make much more sense (they follow the model of a well-known Ada concept) and are much less complex than type invariants. On top of which, I have very few use-cases for such invariants (I have a zillion use-cases for predicates - most things only apply to a subset of types). For course, this is water under the bridge these days; we're surely not removing the type invariant contract. For most users, ignoring the existence of type invariants will not lose any functionality. (Data point: it appears that that is the case for GNAT users; when Jeff wrote his type invariant ACATS tests, GNAT got almost nothing about them correct. One would have expected that basic bugs would have been eliminated had any actual users tried the feature.) ************************************************************** From: Jeff Cousins Sent: Monday, October 2, 2017 4:19 PM I've changed from using type invariants to using subtypes with dynamic predicates in my bellringing programs that I'd previously adapted to become ACATS tests. The original question seems to say that if you allow type invariants on private extensions then you may as well allow them on null extensions, but personally (from my experience of writing ACATS tests) I don't think that they should have been allowed on private extensions, it opens too many loopholes. ************************************************************** From: Yannick Moy Sent: Monday, October 2, 2017 11:20 PM > This is where we went wrong, in my view. Yes, the "formal methods community" > has such a concept, but it really is not very useful if you have predicates. > And for me, at least, predicates make much more sense (they follow the model > of a well-known Ada concept) and are much less complex than type invariants. > On top of which, I have very few use-cases for such invariants (I have a > zillion use-cases for predicates - most things only apply to a subset of > types). >Type invariants are "weak" invariants: only true for clients, not inside unit >that defines the type. Predicates are "strong" invariants: always true, even >on intermediate modifications. To me, both have value, and I'm using both. Yes you could somewhat emulate type invariants with predicates, at the cost of repeated conversions. Not something I would call a full-fledge feature. >For most users, ignoring the existence of type invariants will not lose any >functionality. (Data point: it appears that that is the case for GNAT users; >when Jeff wrote his type invariant ACATS tests, GNAT got almost nothing >about them correct. One would have expected that basic bugs would have been >eliminated had any actual users tried the feature.) That one would be true of many contracts included in Ada 2012, both predicates and type invariants IMHO. Users slowly get to use them. ************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 12:36 AM >... Yes you could somewhat emulate type invariants with predicates, at >the cost of repeated conversions. Not something I would call a >full-fledge feature. Since predicates are used on subtypes, there aren't any explicit conversions needed. Implicit conversions have little effect on readability, so there isn't much difference. The advantage of predicates for typical Ada users (those without much formal methods experience) is that they work pretty much the same as range and discriminant constraints. There's nothing complex to learn (or to define, for that matter -- most of the complication for predicates comes down to handling cases of mixed Ignore/Check policies -- which don't happen much anyway). >> For most users, ignoring the existence of type invariants will not >> lose any functionality. (Data point: it appears that that is the case for >> GNAT users; when Jeff wrote his type invariant ACATS tests, GNAT got almost >> nothing about them correct. One would have expected that basic bugs >> would have been eliminated had any actual users tried the feature.) >That one would be true of many contracts included in Ada 2012, both predicates >and type invariants IMHO. Users slowly get to use them. Admittedly, we don't have that data point for predicates, as Bob wrote predicate tests early on (2013ish, I think). Nobody expected users to have used anything back then. But the type invariant tests were written last year (2016). The state of them then suggests that no one had used them (or at least cared that almost nothing was checked properly). In any case, we're stuck with them, even if no one implements the corner cases. (Thus I wouldn't trust them to actually detect errors anywhere near as well as predicates, which have a fairly clear and simple model.) **************************************************************