Version 1.2 of acs/ac-00296.txt

Unformatted version of acs/ac-00296.txt version 1.2
Other versions for file acs/ac-00296.txt

!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.)

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


Questions? Ask the ACAA Technical Agent