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

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

!standard 6.1.1(1/3)          13-05-08 AI12-0045-1/03
!class binding interpretation 12-12-01
!status Amendment 202x 12-12-27
!status WG9 Approved 13-06-14
!status ARG Approved 11-0-0 12-12-06
!status work item 12-12-01
!status received 12-09-19
!priority Medium
!difficulty Medium
!subject Pre- and Postconditions are allowed on generic subprograms
!summary
Aspects Pre and Post can be specified on generic subprograms, but not on instances of generic subprograms.
!question
6.1.1(1/3) says:
For a subprogram or entry, the following language-defined aspects may be specified with an aspect_specification
and AARM 6.1(20.a/3) adds
... a generic subprogram is not a subprogram.
This implies that pre/post-condition aspect specifications are not allowed for generic subprograms. Should they be? (Yes.)
!recommendation
(See summary.)
!wording
Replace 6.1.1(1/3) with:
For a noninstance subprogram, a generic subprogram, or an entry, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
!discussion
If we allowed Pre and Post on instances that are subprograms, we would be introducing a maintenance problem, as converting the generic subprogram to a generic package containing that subprogram would require the removal of the aspects (there is no corresponding feature for subprograms declared inside of package instances). The examples of such usage have not been compelling (they usually are refinements of overly general aspects on the generic).
In addition, if we allowed these aspects on both the generic (which is important) and on the instance, we'd have to define how these combine. That is a problem for preconditions, which should combine with "and" or "or" depending on who you are talking to and about what. ["or" is required to follow LSP.] To avoid answering this question, we make the programmer answer it explicitly. That principle should be continued.
We considered allowing the aspects on an instance if none are given on the generic unit in order to avoid this latter problem. But we decided against this because of the maintenance problem mentioned above.
!corrigendum 6.1.1(1/3)
Replace the paragraph:
For a subprogram or entry, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
by:
For a noninstance subprogram, a generic subprogram, or an entry, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
!ACATS test
ACATS tests should be created to test these rules.
!appendix

From: Steve Baird
Sent: Wednesday, September 19, 2012  1:07 PM

6.1.1(1/3) says:
   For a subprogram or entry, the following language-defined aspects
   may be specified with an aspect_specification

  and annotation 6.1(20.a/3) adds
    ... a generic subprogram is not a subprogram.

I conclude that pre/post-condition aspect specifications are not allowed for
generic subprograms.

Was this intended?  Should such aspect specifications be allowed?
IMO, they should be allowed.

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

From: Robert Dewar
Sent: Wednesday, September 19, 2012  1:27 PM

Yes, of course they should be allowed, this is a typical case of the RM tripping
over the trap it set for everyone in considering that a generic subprogram is
not a subprogram (TERRIBLE choice!)

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

From: Steve Baird
Sent: Wednesday, September 19, 2012  2:04 PM

As I said earlier, I think pre/post-conditions for generic subprograms hould be
allowed.

This would, however, require defining the interactions between
pre/post-conditions for a generic subprogram and for an instance thereof.

Bob Duff said (in some non-ARG mail):
> If it's allowed, and pre/post are given on both generic and instance,
> then it seems pretty obvious that both should apply.
> I think the usual rule for multiple pre/post is that the RM doesn't
> define any particular order, and allows but does not require short
> circuiting.

I agree that this is how the language should work, but I think explicit RM
wording would be needed to address this.

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

From: Randy Brukardt
Sent: Saturday, September 22, 2012  6:45 PM

I would not have expected them to be allowed on instances. To be discussed when
I get home.

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

From: Robert Dewar
Sent: Saturday, September 22, 2012  10:38 PM

Pre and post-conditions on instances are very useful, it would be bad to lose
them (very often the pre and post conditions can be tighted up when you have a
specific instantiation.

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

From: Tucker Taft
Sent: Saturday, September 22, 2012  10:54 PM

Examples, please!

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

From: John Barnes
Sent: Monday, September 24, 2012  2:11 AM

Spark allows them on both generics and instatiations.

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

From: Robert Dewar
Sent: Monday, September 24, 2012  5:48 AM

Are there some nice usage examples from the SPARK world?

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

From: Yannick Moy
Sent: Monday, September 24, 2012  6:03 AM

Here is the very simple example used in the document "SPARK Generics: a user view":

The generic is declared like that:

generic
    type T1 is range <>;
    type T2 is range <>;
    --# check T2 (T1'Last  * T1'Last)  <= T2'Last and
    --#       T2 (T1'First * T1'First) <= T2'Last and
    --#       T2 (T1'Last  * T1'Last)  >= T2'First;
    --#       T2 (T1'First * T1'First) >= T2'First;
function Square (X : in T1) return T2;
--# return R => R = T2 (X * X);

And here comes the instance, which states here a lower bound on the parameter (X
> 1), which results in a lower bound on the result (R >= 4):

type Actual_T1 is range 0 .. 10;
type Actual_T2 is range 0 .. Actual_T1'Last * Actual_T1'Last;

function My_Square
--# pre X > 1;
--# return R => R = T2 (X * X) and R >= 4; is new Square (T1 => Actual_T1, T2 => Actual_T2);

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

From: John Barnes
Sent: Monday, September 24, 2012  7:24 AM

> Are there some nice usage examples from the SPARK world?

See my new Spark book.  Sorry, in a rush right now. Funeral, probate and Holiday
to deal with.

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

From: Randy Brukardt
Sent: Tuesday, October  2, 2012  5:58 PM

I said while on vacation:

> I would not have expected them to be allowed on instances. To be
> discussed
when I get home.

In response to Steve's:

> As I said earlier, I think pre/post-conditions for generic subprograms
> hould be allowed.
>
> This would, however, require defining the interactions between
> pre/post-conditions for a generic subprogram and for an instance
> thereof.

> Bob Duff said (in some non-ARG mail):

> If it's allowed, and pre/post are given on both generic and instance,
> then it seems pretty obvious that both should apply.
> I think the usual rule for multiple pre/post is that the RM doesn't
> define any particular order, and allows but does not require short
> circuiting.

Actually, none of this follows at all. The model of specific preconditions is
that only one applies to any particular subprogram, and the reason for that is
that we couldn't agree on how multiple preconditions should apply. Specifically,
LSP suggests that multiple preconditions should be "or"ed; but most people
expect them to be "and"ed. Rather than trying to answer the question, we decided
only to allow one. (And we did the same for postconditions, mainly for
consistency.)

Therefore, there is no mechanism in the language to combine specific pre or
postconditions. One could be created, but it suffers from the same problems that
we were unable to solve for the language as a whole. I don't see any reason why
this is easier.

I'm assuming that class-wide pre- and post-conditions are not allowed on generic
subprograms because such subprograms cannot be primitive for any type. They can
only be allowed on instances; as such I'm only talking about specific pre- and
postconditions below. One could imagine trying to allow class-wide pre- and
post-conditions on generic subprograms, but that requires even more rule
changes.

There are a number of options for this problem:

(1) Leave the language alone (which does not allow pre- and post-conditions on
generic subprograms, but does allow them on instances). If it is truly valuable
to allow them on instances (and I admit I am skeptical), this is probably the
best option.

(2) Allow pre- and post-conditions on generic subprograms, but not on instances.
This is the rule I would have expected, as it avoids combining preconditions,
and it follows the contract model of the language. It should be clear that a
*post*condition on an instance is a dubious construct, as the postcondition puts
conditions on the body of a subprogram, and the body of a generic subprogram is
the same for all instances (the contract model makes that true). It doesn't make
much sense to put additional requirements on the body of some instance, as there
is almost no way for the implementation of the body to change. (For those of us
that use code sharing, this seems even more obvious, as the postcondition is
expected to be evaluated as part of the body, and thus it ought to be the same
for all instances. It can be implemented otherwise, but that's more work and
seems just wrong.)

If one considers a precondition a mirror image of a postcondition, one would
expect the same of preconditions. It makes more sense for the preconditions to
be different, but again the body cannot change (or take advantage of) a
different precondition.

One would hope that the Ada language is powerful enough to be able to write
pre- and post-conditions in terms of the formal parameters, so that the pre- and
post-conditions of the actual instance are more useful (and detailed) than the
conditions of the generic. If that's not the case, I'd rather strengthen the
expressions of the language (which would be useful in generic units as well)
than corrupt the contract model of the language.

It also should be noted that generic subprograms are not that common; most
generics are generic packages. For a subprogram declared in a generic package,
it is not possible to put any pre- or post-conditions on the subprogram in an
instance. I think it would be preferable (and surely more consistent) if the
language treated generic subprograms as if they are a generic package containing
a single subprogram (this is effectively how Janus/Ada implements them). It
seems weird to allow additional capabilities for generic subprograms over any
other subprogram that happens to be declared in a generic.

Moving on to other options:

(3) Allow pre- and post-conditions on *either* a generic subprogram or its
instance, but not both.

This avoids the combining problem, and gives maximum flexibility. But we still
have the problem of treating generic subprograms and subprograms declared in
generic packages differently.

Similarly,

(4) Allow pre- and post-conditions on both generic subprograms and instances
thereof, but the last declared specific pre- and post-condition is the only one
used.

This matches the rules for inheritance, but it seems likely to be confusing to
users. I think I'd prefer (3) to (4) if we're going to allow these on instances
at all.

Finally, of course

(5) Allow pre- and post-conditions on both generic subprograms and instances
thereof, and "and" them together. But, as noted above, we don't do this in any
other case in the language (for specific preconditions especially), and this
opens up a whole level of expectations that the language does not try to
accomplish. As such, I think this is a very bad idea, especially at this late
date.

P.S. Please try to have language discussions here or on Ada-Comment, and not
privately on AdaCore mailing lists that aren't on the (public) record and that
freeze out half of the ARG.

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

From: Bob Duff
Sent: Tuesday, October  2, 2012  6:35 PM

> Actually, none of this follows at all.

Yes, I (now) think you're right.

> It also should be noted that generic subprograms are not that common;
> most generics are generic packages.

Yes, that's a good point.  Which leads to --> leave it alone.

> P.S. Please try to have language discussions here or on Ada-Comment,
> and not privately on AdaCore mailing lists that aren't on the (public)
> record and that freeze out half of the ARG.

Well, I often have language discussions with misc folks (usually, but not
necessarily AdaCore folks), of the form "Is this worth asking ARG?". It's not a
matter of freezing anybody out, just trying to avoid extra possibly-useless work
for ARG.

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

From: Randy Brukardt
Sent: Tuesday, October  2, 2012  6:49 PM

> > It also should be noted that generic subprograms are not
> that common;
> > most generics are generic packages.
>
> Yes, that's a good point.  Which leads to --> leave it alone.

Actually, it doesn't, because that would allow preconditions on instances of
generic subprograms (but not the generic subprogram), while in a generic package
the situation is reversed.

I'd expect that to cause problems when converting a generic subprogram into a
package (or vice-versa, much less common). I know I've sometimes written generic
subprograms only to realize I needed a constant or a helper function. So I had
to convert it into a package, which is easy to do. It would be weird to have to
move the preconditions (and rewrite them as well) when doing such a change.

So I think (as I've stated before) that the best option is to allow specific
preconditions and postconditions on generic subprograms, but not to allow them
on instances.

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

From: Randy Brukardt
Sent: Tuesday, October  2, 2012  6:55 PM

...
> > P.S. Please try to have language discussions here or on Ada-Comment,
> > and not privately on AdaCore mailing lists that aren't on the
> > (public) record and that freeze out half of the ARG.
>
> Well, I often have language discussions with misc folks (usually, but
> not necessarily AdaCore folks), of the form "Is this worth asking
> ARG?".
> It's not a matter of freezing anybody out, just trying to avoid extra
> possibly-useless work for ARG.

Yes, that's fine. In this case, however, it appeared that the "outside the ARG
discussion" happened after the thread was opened here. That's what I objected to
(although it might have been that Steve had "dipped into the archives" for the
quote from you).

As for "possibly useless work for the ARG", having noted the extremely low
balance in my checking account, I'd welcome some useless work. ;-)

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

From: Tucker Taft
Sent: Tuesday, October  2, 2012  7:49 PM

> So I think (as I've stated before) that the best option is to allow
> specific preconditions and postconditions on generic subprograms, but
> not to allow them on instances.

Wouldn't that be incompatible with the (almost) published standard?
Allowing them on generics or instances but not both would be compatible, and
plenty flexible, and avoid the various issues about combining.

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

From: Robert Dewar
Sent: Tuesday, October  2, 2012  8:28 PM

> So I think (as I've stated before) that the best option is to allow
> specific preconditions and postconditions on generic subprograms, but
> not to allow them on instances.

I strongly disagree, allow them both places! I see no reason for a narrower
viewpoint.

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

From: Robert Dewar
Sent: Tuesday, October  2, 2012  8:31 PM

> (5) Allow pre- and post-conditions on both generic subprograms and
> instances thereof, and "and" them together. But, as noted above, we
> don't do this in any other case in the language (for specific
> preconditions especially), and this opens up a whole level of
> expectations that the language does not try to accomplish. As such, I
> think this is a very bad idea, especially at this late date.

I think this is the obvious choice and for me (1)-(4) are all non-starters.
Certainly in GNAT we will allow the pre/post pragmas in both places anyway (we
also allow multiple pragmas to appear).

I find the objection Randy raises unconvincing

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

From: Tucker Taft
Sent: Tuesday, October  2, 2012  8:35 PM

> I strongly disagree, allow them both places! I see no reason for a
> narrower viewpoint.

I agree in allowing them on either place, but allowing them on both for a given
subprogram seems unnecessary.  In the few cases where that is absolutely
critical, a wrapper is always possible.

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

From: Steve Baird
Sent: Wednesday, October  3, 2012  2:37 PM

> I agree in allowing them on either place, but allowing them on both
> for a given subprogram seems unnecessary.

This rule is similar in spirit to the existing 13.1.1(14/3) "don't specify the
same aspect twice" rule. Looks good to me.

> In the few oases where that is absolutely critical, a wrapper is
> always possible.

I think it is unlikely that anyone will complain anytime soon that introducing a
wrapper means that they can't pass it to a generic which takes a formal
instance.

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

From: Erhard Ploedereder
Sent: Thursday, October  4, 2012  6:58 PM

Is this now settled as:
- allow in either place
- but not in both
?

Makes sense to me.

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

From: Randy Brukardt
Sent: Thursday, October  4, 2012  8:39 PM

I think so, pending, of course, a vote at our next meeting.

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

From: Robert Dewar
Sent: Thursday, October  4, 2012  9:54 PM

Why is this example not convincing (for allowing them in both places), seems a
reasnable example to me!

["This" being Yannick's example of September 24th.]

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

From: Randy Brukardt
Sent: Friday, October  5, 2012  12:19 AM

We've essentially agreed to allow them in both places, but only one or the other
can appear (can't give a precondition on both, because we don't want any
combining of specific preconditions). That's certainly the case in this example,
the generic subprogram doesn't have a precondition. So I don't see that this
example changes anything.

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

From: Robert Dewar
Sent: Friday, October  5, 2012  9:03 AM

But you do have a postcondition on both!

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

From: Randy Brukardt
Sent: Friday, October  5, 2012  1:23 PM

It does? I missed that, probably because I don't speak SPARK.

Anyway, that caused me to take another look at the example, and I now think it
is bogus.

The idea in this case is the change the postcondition to reflect an added
precondition. But the postcondition on a generic unit (or anything else, for
that matter) shouldn't be changed simply because the body can't be changed to
reflect that. One presumes it depends on the properties of the formal type, and
the actual type ought to accurately reflect the appropriate properties.

In this case, we have the generic (written in Ada!):

generic
    type T1 is range <>;
    type T2 is range <>;
function Square (X : in T1) return T2
   with Post => Square'Result = T2 (X * X);

And the instance was:

type Actual_T1 is range 0 .. 10;
type Actual_T2 is range 0 .. Actual_T1'Last * Actual_T1'Last;

function My_Square is new Square (T1 => Actual_T1, T2 => Actual_T2)
   with Pre => X > 1; Post => Square'Result = T2 (X * X) and Square'Result >= 4;

But this is silly -- if there is an extra part to the postcondition, it should
have been part of the original postcondition depending on the formals. In this
case, it should be something like:

generic
    type T1 is range <>;
    type T2 is range <>;
function Square (X : in T1) return T2
   with Post => Square'Result = T2 (X * X) and
        (if T1'First >= 0 then Square'Result >= T2 (T1'First*T1'First);

In addition, the above instantiation has the wrong range for the Actual_T1
(sub)type; it uses a precondition rather than a subtype to provide the range.
That essentially causes the problem in this example. Ada ranges should always be
used rather than preconditions when possible, for the obvious reason that that
will work in all versions of Ada, not just Ada 2012. (Ada compilers have lots of
specialized code for handling ranges, as well, so the code quality of the result
is likely to be better, too, especially if checks are not suppressed.)

Once a range is used, the original postcondition adjusts to take it into
account. Doing so gives an instance of:

type Actual_T1 is range 0 .. 10;
subtype Restricted_Actual_T1 is Actual_T1 range 2 .. 10;
type Actual_T2 is range 0 .. Actual_T1'Last * Actual_T1'Last;

function My_Square is new Square (T1 => Restricted_Actual_T1, T2 => Actual_T2);

which needs no new pre or postconditions, and has the same postcondition as the
original example.

People probably use constructions like the example because of the limitations of
SPARK. That's no reason for them to use such silly constructions in full Ada.

There might be a compelling example of the use of pre or postconditions on an
instance, but this isn't it.

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

From: Yannick Moy
Sent: Monday, October  8, 2012  2:46 AM

> There might be a compelling example of the use of pre or
> postconditions on an instance, but this isn't it.

I think this might happen whenever a property is too complex to express on the
generic function, or is a consequence of the contract of the generic function,
that we would like to express more simply. For example, take a generic in-place
sorting function:

   generic
     type Collection is new Some_List_Type;
   procedure Sort (C : in out Collection) with
     Post => (for all E of C => C'Old.Contains (E))
                and then
             (for all E of C'Old => C.Contains (E));

If you instantiate with the type No_Duplicates defined as:

   type No_Duplicates is new Some_List_Type;

then you may want to add to the contract of the instance of Sort for
No_Duplicates that there are indeed no duplicates in the input collection and
likewise in the output collection:

   procedure Sort_No_Duplicates (C : in out Collection) is
     new Sort (No_Duplicates)
   with
     Pre  => No_Duplicates_In (C),
     Post => No_Duplicates_In (C);

I don't know if this is compelling, but I see this being used.

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

From: Robert Dewar
Sent: Monday, October  8, 2012  12:32 PM

Me too, it is a natural thing to do, and I don't see sufficient justification
for making it difficult!

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

From: Bob Duff
Sent: Monday, October  8, 2012  12:40 PM

>    type No_Duplicates is new Some_List_Type;

I'd put a Predicate on No_Duplicates.

In fact, I've found that it is often (usually?) better to use Predicate than Pre and Post.

> then you may want to add to the contract of the instance of Sort for
> No_Duplicates that there are indeed no duplicates in the input
> collection and likewise in the output collection:
>
>    procedure Sort_No_Duplicates (C : in out Collection) is
                                  ^^^^^^^^^^^^^^^^^^^^^^^ That's illegal syntax,
				  by the way.  And anyway, C is of type
				  No_Duplicates.

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

From: Robert Dewar
Sent: Monday, October  8, 2012  1:05 PM

> I'd put a Predicate on No_Duplicates.

How do you know you can?
Software people so often assume that arbitrary code can be modified!
Or perhaps No_Duplicates has associated routines that mess around and
temporarily have duplicates (yes, it might be better to make it private, but
sometimes we don't like to make things private, because they would be too
private!)

What if No_Duplicates is defined in an Ada 95 module that does not permit Ada
2012 stuff?

Why ask someone to write things in a different way than they see the problem at
first glance?

I know that you (Bob) find the use of predicates convincing, but I think a lot
of people will prefer to use Pre/Post because

a) they are used to it

b) they have a clearer idea of where the checks are made

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

From: Randy Brukardt
Sent: Monday, October  8, 2012  5:45 PM

If they need to know where the checks are made, they're doing something wrong.
That's because these checks should never fail in a correct program, and in
particular, a predicate is (logically) always true for the object to which it
applies. If someone is trying to sneak in something that "temporarily" is
violating a predicate, that's just plain wrong; otherwise, it doesn't matter
where the checks are made.

Predicates are easier to understand than pre/post because predicates work (more
or less) like constraints -- something every Ada programmer should be familiar
with. Pre/post are different and have subtlies (like caring about when they are
checked) that make them less obvious. (Yes, there are things that can't be
checked with a predicate, but those aren't that common and certainly shouldn't
be where someone starts using these things.)

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

From: Robert Dewar
Sent: Monday, October  8, 2012  6:07 PM

> If they need to know where the checks are made, they're doing
> something wrong. That's because these checks should never fail in a
> correct program, and in particular, a predicate is (logically) always
> true for the object to which it applies. If someone is trying to sneak
> in something that "temporarily" is violating a predicate, that's just
> plain wrong; otherwise, it doesn't matter where the checks are made.

It seems to me that for a complex data structure, it will be normal for routines
working on that complex data structure to violate invariants that normally hold
outside. yes, we like to make things private and use invariants, but that's not
always practical (for many reasons), and in such cases, predicates may not be a
satisfactory substitute for pre and post conditions

> Predicates are easier to understand than pre/post because predicates
> work (more or less) like constraints -- something every Ada programmer
> should be familiar with. Pre/post are different and have subtlies
> (like caring about when they are checked) that make them less obvious.
> (Yes, there are things that can't be checked with a predicate, but
> those aren't that common and certainly shouldn't be where someone
> starts using these things.)

Yes, when predicates work they are great, but they cannot always replace pre and
post conditions!

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

From: Randy Brukardt
Sent: Monday, October  8, 2012  6:39 PM

> It seems to me that for a complex data structure, it will be normal
> for routines working on that complex data structure to violate
> invariants that normally hold outside. yes, we like to make things
> private and use invariants, but that's not always practical (for many
> reasons), and in such cases, predicates may not be a satisfactory
> substitute for pre and post conditions

Perhaps. I mostly envision predicates being used on parameters whose value isn't
going to change in the subprogram. (That's most parameters.) And I mostly see
preconditions being used to check the values of incoming parameters -- but
that's usually better done using predicates.

> > Predicates are easier to understand than pre/post because predicates
> > work (more or less) like constraints -- something every Ada
> > programmer should be familiar with. Pre/post are different and have
> > subtlies (like caring about when they are checked) that make them less obvious.
> > (Yes, there are things that can't be checked with a predicate, but
> > those aren't that common and certainly shouldn't be where someone
> > starts using these things.)
>
> Yes, when predicates work they are great, but they cannot always
> replace pre and post conditions!

And I don't think anyone ever claimed that they could always replace
preconditions. (They can replace postconditions only rarely: just those that are
on "in out" and "out" parameters.)

Predicates and preconditions have a wide overlap in things that they can check,
as do invariants and postconditions. (This makes sense, given that these pairs
are implemented similarly; the other pairs may be implemented quite differently
[call-site vs. in body, for instance].) Invariants do not overlap at all with
preconditions, and predicates have a very small overlap with postconditions.

All things being equal, I prefer predicates to preconditions, for reasons I gave
previously, when either can be used. Of course, if only one or the other will
solve your problem, surely use the one that solves your problem, as opposed to
trying to make a square peg fit in a hexagonal hole.

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

From: Bob Duff
Sent: Tuesday, October  9, 2012  9:06 AM

> >>     type No_Duplicates is new Some_List_Type;
> >
> > I'd put a Predicate on No_Duplicates.
>
> How do you know you can?
> Software people so often assume that arbitrary code can be modified!

I'm sure ARG members are well aware of the fact that some people don't want to
modify their code.  And we don't need yet another lecture on that point.
Anyway, that fact is largely irrelevant to language design, because if they're
not modifying their code, they're not using all the fancy new features.

Obviously, when I say "I'd put a Predicate...", I mean that when I declare type
No_Duplicates, I'd put a Predicate on it. That's good advice, and I don't know
why you object to it, other than for rhetorical reasons.

> Or perhaps No_Duplicates has associated routines that mess around and
> temporarily have duplicates...

One of the strengths of Predicates is that they support exactly that usage.

>...(yes, it
> might be better to make it private, but sometimes we  don't like to
>make things private, because they would  be too private!)
>
> What if No_Duplicates is defined in an Ada 95 module that does not
> permit Ada 2012 stuff?

You can come up with all sorts of reasons why people can't use some useful
feature, Predicate is just one such.  So what? I mean, what if they whole
program is Ada 83 and can't use ... ?

To answer the above question:  Write a wrapper.

> Why ask someone to write things in a different way than they see the
> problem at first glance?

For all the reasons already discussed in this thread.

> I know that you (Bob) find the use of predicates convincing, but I
> think a lot of people will prefer to use Pre/Post because
>
> a) they are used to it

Pre/Post were added to the language at the same time as Predicates, so I don't
buy that argument.

> b) they have a clearer idea of where the checks are made

If you want to know where the checks are made, you should use pragma Assert.

We've yet to see a single compelling example of a postcondition on an instance.
And if it's so important to allow postconditions on instances, they why isn't
anybody clamoring for an ability to put postconditions on subprograms inside
package instances? That's by far the more common case of instances.

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  9:42 AM

> I'm sure ARG members are well aware of the fact that some people don't
> want to modify their code.  And we don't need yet another lecture on
> that point.  Anyway, that fact is largely irrelevant to language
> design, because if they're not modifying their code, they're not using
> all the fancy new features.

AARGH! The *NORMAL* mode of use of Ada 2012 will be that certain new units are
written in this mode, leaving big chunks of untouched legacy 95 code. If the
design of the language and the implementation do not accomodate that, then
almost no one will use Ada 2012 at all.

> Obviously, when I say "I'd put a Predicate...", I mean that when I
> declare type No_Duplicates, I'd put a Predicate on it.
> That's good advice, and I don't know why you object to it, other than
> for rhetorical reasons.

Because it may not be possible.

>> Or perhaps No_Duplicates has associated routines that mess around and
>> temporarily have duplicates...
>
> One of the strengths of Predicates is that they support exactly that
> usage.

I don't think so, not if they are checked when passed as parameters to other
procedures??? Or you declare a temp variable initialized with a value that does
not meet the predicate???

>> ...(yes, it
>> might be better to make it private, but sometimes we don't like to
>> make things private, because they would be too private!)
>>
>> What if No_Duplicates is defined in an Ada 95 module that does not
>> permit Ada 2012 stuff?
>
>> Why ask someone to write things in a different way than they see the
>> problem at first glance?
>
> For all the reasons already discussed in this thread.
>
>> I know that you (Bob) find the use of predicates convincing, but I
>> think a lot of people will prefer to use Pre/Post because
>>
>> a) they are used to it
>
> Pre/Post were added to the language at the same time as Predicates, so
> I don't buy that argument.

They are used to it because they have been writing in SPARK, or in Ada with our
precondition/postcondition pragmas (where have you been? :-) GNAT has had
preconditions and postconditions for ages, what the ARG does years later does
not change that!) or in Eiffel or with faked preconditions/postconditions using
assert etc.

>> b) they have a clearer idea of where the checks are made
>
> If you want to know where the checks are made, you should use pragma
> Assert.

I disagree with this kind of viewpoint. I have an absolutely clear idea of when
pre and post conditions are checked.

I must say, I prefer to use pre and post conditions to predicates in most cases,
especially for complex data. Why, because of all the discussion of predicates
not being fully check in all situations, which I don't understand and am not
sure I want to understand!

> We've yet to see a single compelling example of a postcondition on an
> instance.  And if it's so important to allow postconditions on
> instances, they why isn't anybody clamoring for an ability to put
> postconditions on subprograms inside package instances?
> That's by far the more common case of instances.

Yes, I think they should be allowed there too.

Oh well, in GNAT at least, we have the pragmas, so if the aspects have arbitrary
restrictions, real programmers will be able to get around them anyway by using
the pragmas which have no such restrictions.

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

From: Jean-Pierre Rosen
Sent: Tuesday, October  9, 2012  9:52 AM

> We've yet to see a single compelling example of a postcondition on an
> instance.
When a postcondition depends on the  properties of a formal subprogram?
Something along the lines (OK, not realistic, just to show the  idea):

generic
   with function Get_Value return Integer; function Double_It return Integer
   with Post => Double_It'Result mod 2 = 0;

function Get_Even return Integer
   with Post => Get_Even'Result mod 2 = 0;

function Double_Even is new Double_It (Get_Even)
   with Post => Double_Even'Result mod 4 = 0;

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  10:00 AM

>> We've yet to see a single compelling example of a postcondition on an
>> instance.

Well there are many useful things in the language that don't necessarily come
with compelling examples showing they are necessary. Where's the compelling
example showing that NOT IN is needed (after all we can always say not (A in
B))?

> When a postcondition depends on the  properties of a formal subprogram?
> Something along the lines (OK, not realistic, just to show the  idea):
>
> generic
>     with function Get_Value return Integer; function Double_It return
> Integer
>     with Post => Double_It'Result mod 2 = 0;
>
> function Get_Even return Integer
>     with Post => Get_Even'Result mod 2 = 0;
>
> function Double_Even is new Double_It (Get_Even)
>     with Post => Double_Even'Result mod 4 = 0;

sounds like a reasonable example

It's intereting that SPARK allows these multiple cases.
That's awkward if the language doesn't allow them. Well not so awkward I guess,
perhaps GNAT should add aspects Precondition and Postcondition which function
like the pragmas and avoid the restrictions of Pre and Post :-)

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

From: Tucker Taft
Sent: Tuesday, October  9, 2012  10:27 AM

There isn't any complexity in supporting *post*conditions on both generic and
instance.  The complexity comes from *pre*conditions. Are they "or"ed or
"and"ed?  If we could disallow preconditions on both places, that would avoid
most of the "hair."

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  10:30 AM

FWIW, GNAT always "and"s multiple preconditions, e.g. when multiple precondition
pragmas appear for a single subprogram, and if there is a pragma and an aspect,
they are also and'ed. That seems the natural semantics to me, "or" would seem
really weird.

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

From: Bob Duff
Sent: Tuesday, October  9, 2012  12:17 PM

> >> We've yet to see a single compelling example of a postcondition on
> >> an instance.
>
> Well there are many useful things in the language that don't
> necessarily come with compelling examples showing they are necessary.
> Where's the compelling example showing that NOT IN is needed (after
> all we can always say not (A in B))?

Heh?  There are lots of compelling examples showing that "not in"
is useful.  Obviously it's not essential, but that's not what we're talking about.

On the other hand, I haven't seen any compelling examples showing that
postconditions on instances are useful.  In fact, it seems to me they're asking
for trouble.  When you write a postcondition, you're supposed to write a body that
obeys the postcondition, but you can't do that for an instance.

> > When a postcondition depends on the  properties of a formal subprogram?
> > Something along the lines (OK, not realistic, just to show the  idea):
> >
> > generic
> >     with function Get_Value return Integer; function Double_It
> > return Integer
> >     with Post => Double_It'Result mod 2 = 0;
> >
> > function Get_Even return Integer
> >     with Post => Get_Even'Result mod 2 = 0;
> >
> > function Double_Even is new Double_It (Get_Even)
> >     with Post => Double_Even'Result mod 4 = 0;
>
> sounds like a reasonable example

Not to me.  ;-)

Here, we've put a postcondition on Double_Even, not knowing what's in the body
of Double_It, other than that it always returns an even number.

If the body says:

    It : Integer := 7;

    function Double_It return Integer is
    begin
        if Get_Value > 0 then
            return It * 2;
        else
            return 0;
        end if;
    end Double_It;

Now the postcondition on Double_It is correct, but the one on Double_Even is
wrong!  That's what happens when you write postconditions on things where you
have no control over the body.

> It's intereting that SPARK allows these multiple cases.

Does it?  I'm not up on the latest SPARK, but I thought it didn't yet support
generics.  I agree that supporting things that SPARK supports (hopefully with
the same semantics) is a good idea.

> That's awkward if the language doesn't allow them. Well not so awkward
> I guess, perhaps GNAT should add aspects Precondition and
> Postcondition which function like the pragmas and avoid the
> restrictions of Pre and Post :-)

Then we have to repeat this argument inside AdaCore.  ;-)

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

From: Bob Duff
Sent: Tuesday, October  9, 2012  12:17 PM

> > I'm sure ARG members are well aware of the fact that some people
> > don't want to modify their code.  And we don't need yet another
> > lecture on that point.  Anyway, that fact is largely irrelevant to
> > language design, because if they're not modifying their code,
> > they're not using all the fancy new features.
>
> AARGH! The *NORMAL* mode of use of Ada 2012 will be that certain new
> units are written in this mode, leaving big chunks of untouched legacy
> 95 code.

Yes, of course.  So what?  That's the case with Text_IO, which as you pointed
out, we're probably not going to touch.

AARGH! to you.  ;-)  Or maybe it should be ARG, since we're on the ARG list.

>...If the design of the language and the implementation  do not
>accomodate that, then almost no one will use Ada 2012 at all.

Mole-hill ==> mountain.  Generic subprograms are rare anyway.

My advice WHEN WRITING CODE is as I said -- put that Predicate on that
No_Duplicates type.  Obviously, if you already have a No_Duplicates type you
don't want to modify, you can't do that.  So what?  There's no way this will
prevent people from using Ada 2012.

You can write a wrapper that has Pre/Post, or has Assert.
But the most likely thing is to do nothing -- just like we're not itching to add
invariants to Text_IO.

There's nothing "unaccomodating" here, nothing stopping people from mixing Ada
95 and 2012!

> > Obviously, when I say "I'd put a Predicate...", I mean that when I
> > declare type No_Duplicates, I'd put a Predicate on it.
    ^^^^^^^^^^^^^^^^^^^
> > That's good advice, and I don't know why you object to it, other
> > than for rhetorical reasons.
>
> Because it may not be possible.

It is ALWAYS possible, when I declare type, to put a predicate.
The fact that some existing code can't be changed is irrelevant.
So don't put predicates on existing code unless you can change that code!

> >> Or perhaps No_Duplicates has associated routines that mess around
> >> and temporarily have duplicates...
> >
> > One of the strengths of Predicates is that they support exactly that
> > usage.
>
> I don't think so, not if they are checked when passed as parameters to
> other procedures??? Or you declare a temp variable initialized with a
> value that does not meet the predicate???

    type Sequence is ...;
    subtype Sequence_With_No_Duplicates is Sequence with
        Predicate => ...;

Then you declare formal parameters of one or the other subtype, depending on
where you want to allow duplicates.

> I must say, I prefer to use pre and post conditions to predicates in
> most cases, especially for complex data.
> Why, because of all the discussion of predicates not being fully check
> in all situations, ...

That seems exactly backwards to me.  The whole point of predicates and
invariants is so you don't forget to put in all the dozens of equivalent
Pre/Post.

Yes, there are loopholes in predicates, but there are loopholes in pre/post,
too.

> ...which I don't
> understand and am not sure I want to understand!

I'm sure you are quite capable of understanding where predicates are checked.
Every time there's a constraint check, there is a predicate check.  See
RM-3.2.4(31/3).

> > We've yet to see a single compelling example of a postcondition on
> > an instance.  And if it's so important to allow postconditions on
> > instances, they why isn't anybody clamoring for an ability to put
> > postconditions on subprograms inside package instances?
> > That's by far the more common case of instances.
>
> Yes, I think they should be allowed there too.
>
> Oh well, in GNAT at least, we have the pragmas, so if the aspects have
> arbitrary restrictions, real programmers will be able to get around
> them anyway by using the pragmas which have no such restrictions.

Heh?  Those pragmas don't allow pre/post on subprograms inside package
instances.

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

From: Randy Brukardt
Sent: Tuesday, October  9, 2012  3:19 PM

...
> We've yet to see a single compelling example of a postcondition on an
> instance.  And if it's so important to allow postconditions on
> instances, they why isn't anybody clamoring for an ability to put
> postconditions on subprograms inside package instances?
> That's by far the more common case of instances.

This is the crux of the issue, really. Allowing pre- and postconditions on
subprogram instances is different than the other parts of the language.
Instances of subprograms declared inside of generic packages cannot have
preconditions or postconditions added. Similarly, you can't add additional pre-
or postconditions to calls with access-to-subprogram parameters.

So writing them on a subprogram instance is a maintenance hazard: it will make
it harder to change the generic to another form. That's quite common. For
instance, all three of the following are roughly equivalent in functionality and
it's not uncommon to change one to one of the others:

generic
   with function Get_Value return Integer;
function Double_It return Integer
   with Post => Double_It'Result mod 2 = 0;

---

generic
   with function Get_Value return Integer;
package Operations is
   function Double_It return Integer
       with Post => Double_It'Result mod 2 = 0;
end Operations;

---

function Double_It (Get : access function return Integer) return Integer
   with Post => Double_It'Result mod 2 = 0;

---

But while the first appears to allow having pre and post on the instance, there
is no equivalent functionality on either of the others (on the package instance
or on the call of the latter). Which to me makes the first suspicious as well.

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

From: Randy Brukardt
Sent: Tuesday, October  9, 2012  3:39 PM

> > There isn't any complexity in supporting *post*conditions on both
> > generic and instance.  The complexity comes from *pre*conditions.
> > Are they "or"ed or "and"ed?  If we could disallow preconditions on
> > both places, that would avoid most of the "hair."
>
> FWIW, GNAT always "and"s multiple preconditions, e.g. when multiple
> precondition pragmas appear for a single subprogram, and if there is a
> pragma and an aspect, they are also and'ed.
> That seems the natural semantics to me, "or" would seem really weird.

"or" *is* really weird, but it is also what LSP and "Design-by-Contract"TM
require. People coming from an Eiffel background would expect preconditions to
be "or"ed and postconditions to be "and"ed.

It's true that even then, you probably want "and" in some circumstances.
Which is too hard for the language to solve, therefore we didn't try.

Everything in the rules of Ada 2012 assume that there is only one Pre or Post,
going all the way back to the definition of aspect_clause (which only allows an
item to be specified once). Changing that assumption would require a lot of
changes in wording throughout the Standard.

As Bob notes, you can always use a wrapper to effectively "add" a precondition
or postcondition to an existing routine. I don't see much need to have a weird
special case to allow adding them to subprogram instances - which are rare and
also causes a potential for maintenance headaches.

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  5:34 PM

>> ...which I don't
>> understand and am not sure I want to understand!
>
> I'm sure you are quite capable of understanding where predicates are
> checked.  Every time there's a constraint check, there is a predicate
> check.  See RM-3.2.4(31/3).

Yes, for scalar types I understand, but I am much less clear about predicates on
composite types. For example if I have a predicate on an array, does it get
checked every time an element is changed e.g. by passing the element as in out
to a procedure.

>>> We've yet to see a single compelling example of a postcondition on
>>> an instance.  And if it's so important to allow postconditions on
>>> instances, they why isn't anybody clamoring for an ability to put
>>> postconditions on subprograms inside package instances?
>>> That's by far the more common case of instances.
>>
>> Yes, I think they should be allowed there too.
>>
>> Oh well, in GNAT at least, we have the pragmas, so if the aspects
>> have arbitrary restrictions, real programmers will be able to get
>> around them anyway by using the pragmas which have no such
>> restrictions.
>
> Heh?  Those pragmas don't allow pre/post on subprograms inside package
> instances.

Why can't you have the pragmas in the instance, and pass their expressions in as
generic parameters?

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  5:35 PM

> So writing them on a subprogram instance is a maintenance hazard: it
> will make it harder to change the generic to another form. That's quite common.
> For instance, all three of the following are roughly equivalent in
> functionality and it's not uncommon to change one to one of the others:

I find this argument (maintenance hazard) convincing

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

From: Robert Deware
Sent: Tuesday, October  9, 2012  5:39 PM

>>> There isn't any complexity in supporting *post*conditions on both
>>> generic and instance.  The complexity comes from *pre*conditions.
>>> Are they "or"ed or "and"ed?  If we could disallow preconditions on
>>> both places, that would avoid most of the "hair."
>>
>> FWIW, GNAT always "and"s multiple preconditions, e.g. when multiple
>> precondition pragmas appear for a single subprogram, and if there is
>> a pragma and an aspect, they are also and'ed.
>> That seems the natural semantics tome, "or" would seem really weird.
>
> "or" *is* really weird, but it is also what LSP and
> "Design-by-Contract"TM require. People coming from an Eiffel
> background would expect preconditions to be "or"ed and postconditions to be
> "and"ed.

I don't think so, that's in the case of a hierarchy, if you just write

     procedure XYZ (A, B : Natural);
     pragma Precondition (A > 10);
     pragma Precondition (B > A);

I think anyone would expect an AND

> As Bob notes, you can always use a wrapper to effectively "add" a
> precondition or postcondition to an existing routine. I don't see much
> need to have a weird special case to allow adding them to subprogram
> instances - which are rare and also causes a potential for maintenance headaches.

Yes, that seems good enough, or if you always expect an extra precondition, you
can make it a generic parameter right?

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

From: Bob Duff
Sent: Tuesday, October  9, 2012  8:22 PM

> > I'm sure you are quite capable of understanding where predicates are
> > checked.  Every time there's a constraint check, there is a
> > predicate check.  See RM-3.2.4(31/3).
>
> Yes, for scalar types I understand, but I am much less clear about
> predicates on composite types. For example if I have a predicate on an
> array, does it get checked every time an element is changed e.g. by
> passing the element as in out to a procedure.

No.  The constraint on the composite does not get checked there, nor does the
predicate.  You are right to be confused by that -- it's one of the loopholes.

> Why can't you have the pragmas in the instance, and pass their
> expressions in as generic parameters?

Sure, you can do something like that, but you can't do it after the fact.

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

From: Robert Dewar
Sent: Tuesday, October  9, 2012  10:02 PM

>> Yes, for scalar types I understand, but I am much less clear about
>> predicates on composite types. For example if I have a predicate on
>> an array, does it get checked every time an element is changed e.g.
>> by passing the element as in out to a procedure.
>
> No.  The constraint on the composite does not get checked there, nor
> does the predicate.  You are right to be confused by that -- it's one
> of the loopholes.

Well this particular case we were talking about was the case of a predicate on a
composite.

What does it mean to have a predicate that says an array is ordered if you can
change an element and the predicate is not checked? I would rather stick to
preconditions and postcondittions in this case I think :-)

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

From: Randy Brukardt
Sent: Wednesday, October 10, 2012  3:13 PM

> What does it mean to have a predicate that says an array is ordered if
> you can change an element and the predicate is not checked? I would
> rather stick to preconditions and postcondittions in this case I think
> :-)

You're right of course, but I don't think preconditions and postconditions help
much either, as they don't know about the actual parameters of a routine and
have no benefit if the change is via an assignment statement.

For instance, if you have
    P_with_In_Out (Ordered(I));
you can't write a precondition or postcondition on P_with_In_Out to check
Ordered.

Indeed, pretty much all you can do in this case is add some pragma Asserts
around.

We talked about whether it made sense to do more checks for predicates, but to
do it right requires distributed overhead (in the above case, you need to make
the check when the parameter is changed, which is somewhere inside of
P_with_In_Out if the parameter is passed by-reference), and the rules aren't
obvious. So we decided to leave this to implementers; if they defined a mode
with additional checks and it proved useful, we'd consider adopting it down the
road.

So if you think this is important, I'd suggest coming up with a design for
additional checks and define an Assertion_Policy to invoke it. (I'd certainly
support such an invention, I'd like fewer holes, at least in a "paranoid" mode.)

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

From: Robert Dewar
Sent: Wednesday, October 10, 2012  3:51 PM

> So if you think this is important, I'd suggest coming up with a design
> for additional checks and define an Assertion_Policy to invoke it.
> (I'd certainly support such an invention, I'd like fewer holes, at
> least in a "paranoid" mode.)

Probably it should be under the -gnatV switch which adds 'Valid calls all over
the place :-)

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

From: Bob Duff
Sent: Wednesday, October 10, 2012  4:20 PM

> What does it mean to have a predicate that says an array is ordered if
> you can change an element and the predicate is not checked?

Basically, it means that you get a predicate check at the places where a
whole-array operation would do a constraint check.  Those places include
parameter passing and function return, so it covers all the places pre/post do.
That's why I think a predicate is better that duplicating that condition all
over in pre/post.

>...I would rather stick to preconditions and  postcondittions in this
>case I think :-)

But the predicate covers all the pre/post you might write (and it won't forget
to write some), plus it does MORE checks (like on whole-array assignments).

Yes, predicates on composite types leak like a colander (e.g. your example of
poking one component of an array).  That's a sad fact of life, but using
pre/post instead just puts more holes in the colandar, and doesn't plug up any
existing holes.

You want a way to say "array objects of this [sub?]type NEVER have duplicates".
Well, sorry, Ada doesn't provide that.  But predicates come closer than
pre/post.  Suppose you accidentally poke one element with a duplicate.  That's a
bug.  Most likely, you will soon pass that array as a parameter, or do some
other thing that checks for duplicates, and thereby find the bug.  It's not
guaranteed, but run-time checks don't guarantee lack of bugs in general.

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

From: Bob Duff
Sent: Wednesday, October 10, 2012  4:31 PM

> Basically, it means that you get a predicate check at the places where
> a whole-array operation would do a constraint check.

Oh, and you can also choose to make that array a private type. Then the "poke
one element" problem can only occur in the package body.  And if does occur,
you're pretty-much guaranteed that there will soon be a predicate check (on an
'in out', or on a function result, for ex.), so clients of that package will not
see objects that violate the desired properties.

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

From: Robert Dewar
Sent: Wednesday, October 10, 2012  4:44 PM

>> What does it mean to have a predicate that says an array is ordered
>> if you can change an element and the predicate is not checked?
>
> Basically, it means that you get a predicate check at the places where
> a whole-array operation would do a constraint check.  Those places
> include parameter passing and function return, so it covers all the
> places pre/post do.
> That's why I think a predicate is better that duplicating that
> condition all over in pre/post.

But I might not want the cheeck on every subprogram. For instance if I have a
subprogram that checks the ordering and is called with this parameter type, and
I have the predicate, don't I have an infinite recursion?

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

From: Steve Baird
Sent: Wednesday, October 10, 2012  4:55 PM

> But I might not want the cheeck on every subprogram. For instance if I
> have a subprogram that checks the ordering and is called with this
> parameter type, and I have the predicate, don't I have an infinite
> recursion?

The predicate is a property of the subtype, not of the type.
Given

     subtype Purple_Cow is Cow with
       Dynamic_Predicate => Is_Purple (Purple_Cow);

, the function Is_Purple should take a parameter of subtype Cow, not Purple_Cow.

But yes, you would get infinite recursion if it takes a Purple_Cow parameter.

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

From: Robert Dewar
Sent: Wednesday, October 10, 2012  5:02 PM

Sure, but most typically your composite type may not be a subtype as far as the
programmer is concerned.

type Ordered is array (1 .. 10) of Natural;

Now, what to do, we don't have Ordered'Base, so you are forced to write this in
a weird way

type OrderedB is array (Integer range <>) of Integer;
subtype Ordered is OrderedB (1 .. 10);

and you have to go rewriting rep clauses, e.g.

   for Ordered'Component_Size use 31;

will have to be rewritten.

Yes, all Ada lawyers know about first subtypes and base types in a case like
this, but not all programmers, so it's not so obvious.

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

From: Steve Baird
Sent: Wednesday, October 10, 2012  5:14 PM

> Now, what to do, we don't have Ordered'Base, so you are forced to
> write this in a weird way

Agreed. I think Bob has argued that it would be useful to have either 'Base or
something like it as a way of separating a (non-scalar) type from its predicate,
but the language does not provide that today.

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

From: Robert Dewar
Sent: Wednesday, October 10, 2012  5:15 PM

Can you recall why not? Now we have predicates, it's a very irritating omission.

I guess we could introduce an attribute
(we = implementor)

     XYZ'No_Predicate_Check

which would be a subtype of XYZ with the predicate removed

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

From: Randy Brukardt
Sent: Wednesday, October 10, 2012  5:26 PM

> Now, what to do, we don't have Ordered'Base, so you are forced to
> write this in a weird way
>
> type OrderedB is array (Integer range <>) of Integer; subtype Ordered
> is OrderedB (1 .. 10);
>
> and you have to go rewriting rep clauses, e.g.
>
>    for Ordered'Component_Size use 31;
>
> will have to be rewritten.

That's not how to do it.

Like *any* Ada type, you almost never want the type to be constrained or have a
predicate or have a null exclusion. (There are some cases where index
constraints are an exception.) You almost always want the root type to be
unchecked and then there to be a checked subtype.

Thus:

type Ordered is array (1 .. 10) of Natural;
subtype Checked_Ordered is Ordered
    with Dynamic_Predicate => ...;

Perhaps you should have different names on these, but that's not required (of
course).

> Yes, all Ada lawyers know about first subtypes and base types in a
> case like this, but not all programmers, so it's not so obvious.

That's not it at all. A checked *type* is almost always a bad idea, and part of
the reason is the recursion possibility that Steve mentioned. And that shows up
in many ways, certainly not all having to do with predicates.

This is identical to the way null exclusions have to be used. You can write a
type like:

    type My_Access is not null access Some_Type;

but that will cause all kinds of problems handling object and component
declarations, query functions, and anywhere else that null might appear briefly.
What you almost always want to do is write something like:

    type My_Access is access Some_Type;
    subtype Not_Null_My_Access is not null My_Access;

You then use My_Access where null might happen, and Not_Null_My_Access elsewhere
(usually parameters).

This is such a common pattern that pretty much all Ada programmers should be
familiar with it. For instance, I usually declare handles something like:

     type URL_Counts is range 0 .. Max_URLs;
     subtype URL_Indicies is URL_Counts range 1 .. URL_Counts'Last;

     URL_Store : array (URL_Indicies) of ...;

Because you always need a "not set" value, and you don't want to include that
value in the data set (so that accidentally using it is detected immediately).

Predicates are no different in this way. I can imagine that novice Ada
programmers will not have seen these patterns, but they're going to have issues
and learn them quickly. So doing this with predicates is just an extension what
one is doing anyway, there is little new here.

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

From: Bob Duff
Sent: Wednesday, October 10, 2012  5:28 PM

> Sure, but most typically your composite type may not be a subtype as
> far as the programmer is concerned.
>
> type Ordered is array (1 .. 10) of Natural;
>
> Now, what to do, we don't have Ordered'Base, so you

Yeah, that's why I want to allow 'Base.

> are forced to write this in a weird way
>
> type OrderedB is array (Integer range <>) of Integer; subtype Ordered
> is OrderedB (1 .. 10);

Indeed, I wrote some code just the other day that had something like:

    type Tree_Base is ...
    subtype Tree is Tree_Base with Predicate => ...;

Then I use Tree all over the place, except in a few places where I need
Tree_Base.  I think there was only one place where I needed Tree_Base -- in a
constructor function, I needed to create an uninitialized Tree_Base, and then
fill in some components to make it obey the predicate, and then the function
returns Tree. (For some reason, I couldn't initialize the thing with an
aggregate; if I could, then I wouldn't have needed Tree_Base there.)

> and you have to go rewriting rep clauses, e.g.
>
>    for Ordered'Component_Size use 31;
>
> will have to be rewritten.

Well, yeah, if you want to add predicates to existing code, you have to change
the code, and maybe even some clients of that code.  Or you can choose not to
use predicates, because you don't want to change the code.

> Yes, all Ada lawyers know about first subtypes and base types in a
> case like this, but not all programmers, so it's not so obvious.

Well, programmers know about constraints, and multiple subtypes of the same type
with different constraints.  If they're going to use predicates, then they're
going to have to learn that you can have different subtypes with different
predicates.

It seems very similar to:

    type Gizmo_Count is range 0 .. Max_Gizmos;
    subtype Gizmo_Index is Gizmo_Count range 1 .. Max_Gizmos;
    type Gizmo_Seq is array (Gizmo_Index range <>) of Gizmo;

which can also be expressed as:

    type Gizmo_Index is range 1 .. Max_Gizmos;
    subtype Gizmo_Count is Gizmo_Index'Base range 0 .. Max_Gizmos;
    type Gizmo_Seq is array (Gizmo_Index range <>) of Gizmo;

When teaching about predicates, I'd say:

Predicates are like constraints, except:

    - Much more general (arbitrary Boolean conditions).

    - Predicates have more loopholes than constraints;
      that's the price we pay for that generality.

Constraints have loopholes, too -- you can have an object of a subtype that
doesn't obey its constraint.  Likewise you can have an object that doesn't obey
the predicate of its subtype (but there are more ways to get into that bad
situation).

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

From: Steve Baird
Sent: Wednesday, October 10, 2012  5:38 PM

>>> Now, what to do, we don't have Ordered'Base, so you are forced to
>>> write this in a weird way
>>
>> Agreed. I think Bob has argued that it would be useful to have either
>> 'Base or something like it as a way of separating a (non-scalar) type
>> from its predicate, but the language does not provide that today.
>
> Can you recall why not?

I think it was mostly the lack of a specific proposal.

There would be some questions about what you want to allow with respect to
private types - do you really want to allow someone outside to strip away the
predicate of a private type?

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

From: Bob Duff
Sent: Wednesday, October 10, 2012  5:48 PM

> Can you recall why not?

My recollection is hazy.  I recall:

    In Ada 83, 'Base was allowed on composites generally,
    but on scalars it was severely restricted.

    In Ada 9X, we disallowed it on composites, due to some semantic
    anomalies (incompatible change!), and we made it work in general
    on scalars.

I'm not 100% sure, but I think the anomalies had to do with the fact that (in
Ada 83) 'Base removed the constraint, and that caused problems with constrained
arrays:

    type Index is Integer range 1..10;
    type T is array (Index) of ...;

and then T'Base is an unconstrained array.  I don't remember why that was a
problem.

And I think the (then-new) things like:

    type T2 (D2: ...) is new T1 (D1 => D2) with ...;

    ...T1'Class (T2'Base(X))...

were troublesome.

That's why I suggested yesterday that for composites, the resurrected 'Base
would not remove constraints.

My suggestion was: 'Base removes constraints (only for scalars), and always
removes "not null", predicates, and invariants.

>... Now we have predicates, it's
> a very irritating omission.
>
> I guess we could introduce an attribute (we = implementor)
>
>      XYZ'No_Predicate_Check
>
> which would be a subtype of XYZ with the predicate removed

Yes, but it seems a shame to use such a long attribute name when 'Base seems
nice and short and rather intuitive (except for the part about not removing
composite constraints).

Maybe ARG should issue a binding interp about 'Base.
Maybe AdaCore should implement it first, and see if it causes trouble.  Maybe
somebody (Steve? me?) should do some historical research.

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

From: Bob Duff
Sent: Wednesday, October 10, 2012  6:14 PM

> There would be some questions about what you want to allow with
> respect to private types - do you really want to allow someone outside
> to strip away the predicate of a private type?

Yeah, or its invariant?!  Sounds scary at first, but I think it's not a problem.

If package P implements some abstraction, with private type P.T, then P has full
control.  The rules about inv/pred are not trying prevent bugs in clients of P
(after all, clients can crash the program by dividing by zero, and there's
nothing P can do to prevent that). The rules are trying to:

    - Help ensure that P is correct.

    - Help ensure that clients can't break the P abstraction.

P can make sure that the default-init of P.T obeys invariants/predicates, or it
can forbid default-init via unknown discrims.

P can ensure incoming objects are "good" by not providing any 'in[out]' params
of subtype T'Base.  So clients can create junk objects, but can't do anything
with them.

P can prevent the creation of junk objects by not providing any '[in]out' params
or function results that return T'Base.

P has full control over whether clients can create and/or manipulate objects of
subtype P.T'Base.  How "open" the P abstraction is, is entirely up to the
programmer of P.

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

From: Robert Dewar
Sent: Wednesday, October 10, 2012  6:34 PM

> P has full control over whether clients can create and/or manipulate
> objects of subtype P.T'Base.  How "open" the P abstraction is, is
> entirely up to the programmer of P.

And you can always totally break privacy with unchecked conversion in any case,
so no need to get too fanatic about protecting privacy!

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

From: Tucker Taft
Sent: Wednesday, October 10, 2012  7:16 PM

I don't think we should try to treat predicates and invariants the same way
here.

A predicate is used to identify a subset of the values of a type.  If you define
a predicate on the first subtype that doesn't change the fact that there can
still be values of the type that don't satisfy the predicate.  And it generally
limits how the *client* can use an object with the specified predicate.

A type invariant serves a different purpose -- it is an implicit precondition of
every visible operation, and that visible operation must preserve the invariant,
and therefore it is also a postcondition. A type invariant need not be visible
to the user of the private type. There should be no way a client can cause the
invariant to be violated.

It makes perfect sense to talk about a subtype to which no predicate applies.
It doesn't really make sense to talk about a *subtype* of a type with a
type-invariant that violates the invariant. An invariant is something that is
preserved by visible operations.  A predicate is used to select a subset of
values of a type.

Another approach to this might be to define an aspect rather than an attribute
which would allow the redefining of a predicate.  E.g.:

    subtype Base_Subtype is Subtype_Having_Predicate
      with New_{Static,Dynamic}_Predicate => True;

This would give Base_Subtype a predicate that is not the "and" of the new
predicate and the old predicate, but rather simply the new predicate.

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

From: Tucker Taft
Sent: Wednesday, October 10, 2012  7:38 PM

>> Can you recall why not?
>
> My recollection is hazy.  I recall:
>
>      In Ada 83, 'Base was allowed on composites generally,
>      but on scalars it was severely restricted.

In Ada 83, 'Base was only allowed as a prefix to attributes such as 'Base'First
'and Base'Last.

>      In Ada 9X, we disallowed it on composites, due to some semantic
>      anomalies (incompatible change!), and we made it work in general
>      on scalars.

Ada 9x allowed the use of 'Base more generally, not merely as a prefix to
another attribute, so you could declare objects of blah'Base.  We tried to allow
this use with composite types, but gave up because of the anomalies.  To avoid
confusion, we decided to disallow the use of 'Base on composite types in
general.  There really were almost no attributes defined on unconstrained
composite subtypes.  'Size might have been the only one, and it isn't clear what
'Base'Size would mean if the first subtype of a derived record type were
constrained with a specified representation that couldn't easily represent an
unconstrained version of the type.

> I'm not 100% sure, but I think the anomalies had to do with the fact
> that (in Ada 83) 'Base removed the constraint, and that caused
> problems with constrained arrays:
>
>      type Index is Integer range 1..10;
>      type T is array (Index) of ...;
>
> and then T'Base is an unconstrained array.  I don't remember why that
> was a problem. ..

One problem was that you could specify the representation on a derived type with
a constrained first subtype which would make no sense if you could de-constrain
the subtype.

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

From: Tucker Taft
Sent: Wednesday, October 10, 2012  7:45 PM

> Sure, but most typically your composite type may not be a subtype as
> far as the programmer is concerned.
>
> type Ordered is array (1 .. 10) of Natural;
>
> Now, what to do, we don't have Ordered'Base, so you
> are forced to write this in a weird way
>
> type OrderedB is array (Integer range <>) of Integer; subtype Ordered
> is OrderedB (1 .. 10);

This particular case doesn't seem so weird.
What would be the input type to the Sort routine whose output was Ordered?

The "Tree" example is a bit more convincing.

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

Questions? Ask the ACAA Technical Agent