CVS difference for ai12s/ai12-0272-1.txt

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0272-1.txt

--- ai12s/ai12-0272-1.txt	2018/04/10 06:05:12	1.1
+++ ai12s/ai12-0272-1.txt	2018/04/14 04:02:04	1.2
@@ -118,7 +118,7 @@
      generic
         type Foo is ...
         with function Reduce1 (Obj : Foo) return Integer
-           with Post => Reduce'Result in -9 .. 9;
+           with Post => Reduce1'Result in -9 .. 9;
         with function Reduce2 (Obj : Foo) return Integer;
      package Gen is
         ...
@@ -546,4 +546,215 @@
 generic formal private type or extension, as it is very much like a
 Postcondition.
 
+***************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, April 10, 2018  12:18 AM
+
+Having looked at the wording, I've convinced myself that we are already
+allowing (unintentionally) Pre/Post on formal subprograms.
+
+As such, the AI I'm writing is more "we meant that" rather than allowing 
+something new. If we *don't* want to allow this, we'll have to add some
+wording to make that happen.
+
+Specifically, we have a blanket rule that says that operational and 
+representation aspects are not allowed on generic formal parameters
+(13.1(9.4/5) - this was moved recently, not sure the old paragraph but it's
+an old rule). We used to have a similar rule for aspect specifications in
+general, but we got rid of it when aspect Nonblocking was defined on formal
+subprograms.
+
+So for any aspects that aren't specified as either operational or 
+representation and that don't specifically have an prohibition against formal
+parameters, we seem to have allowed using the aspect on a formal parameter.
+
+For Pre/Post/Default_Initial_Condition/Dynamic_Predicate and maybe even 
+Type_Invariant, this is what we want. I'll add a bit of wording to re-enforce
+that, but none is actually needed (the dynamic rules have the right effects
+for all but Type_Invariant).
+
+Looking at Pre/Post more closely, it seems certain that a generic formal 
+subprogram is a "callable entity" inside of the generic unit; if it wasn't,
+we'd need special rules to call them (and those don't exist so far as I can
+tell). As such, the rules work properly for a formal subprogram just as they
+would for any other subprogram (it just adds additional
+precondition/postconditions that apply to the subprogram).
+
+The same applies for Default_Initial_Condition and for Dynamic_Predicate 
+(Static_Predicate doesn't apply since no formal type is static).
+
+I suppose I need to check if there are any other such aspects that need 
+wording that they are not allowed on formal parameters.
+
+Agree? Disagree? Could care less?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, April 10, 2018  1:09 AM
+
+Having spent another hour looking at this, there are only a handful of other
+aspects that need wording fixes, and some of what I said in the earlier 
+message was wrong. I've attached the AI [this is version /01 of the AI - ED]
+so anyone who's really interested can see the full situation (I did indeed 
+check the entire set of aspects - most of them are operational or 
+representational or allow being used only on specific syntax).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, April 10, 2018  7:19 AM
+
+I think Type_Invariant is lowest priority.  Default_Initial_Condition and 
+Pre/Post seem useful.  Dynamic_Predicate would be pretty weird, I think, and
+probably a pain to implement.  You could always define a subtype and put a 
+Dynamic_Predicate on it, if that is what you wanted.  I suppose that could be
+what we would want for the semantics of a generic formal type with a 
+Dynamic_Predicate, namely that it is simply added on as though we were
+defining a new subtype.  But it seems odd to associate it with the generic 
+formal subtype rather than a newly defined subtype.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Tuesday, April 10, 2018  8:01 AM
+
+> I think Type_Invariant is lowest priority. 
+
+I think Type_Invariant for a generic formal type is a bad idea.
+Defining the "boundary" seems like it could get messy; it probably could be
+done, but would it be worth the trouble?
+
+> Default_Initial_Condition and Pre/Post seem useful.
+
+Agreed.
+
+> Dynamic_Predicate would be pretty weird, I think, and probably a pain to 
+> implement.
+
+Agreed, but see below.
+
+> You could always define a subtype and put a Dynamic_Predicate on it, if that
+> is what you wanted. I suppose that could be what we would want for the
+> semantics of a generic formal type with a Dynamic_Predicate, namely that it 
+> is simply added on as though we were defining a new subtype. But it seems
+> odd to associate it with the generic formal subtype rather than a newly 
+> defined subtype.
+
+I think there is a stronger argument for allowing this construct than what was
+given (but perhaps still not strong enough to justify allowing it).
+
+Specifying the Dynamic_Predicate as part of the instantiator/instantiatee 
+contract is different than declaring a subtype within the generic and then, by
+convention, using that subtype instead of the original formal type everywhere 
+within the generic.
+
+It conveys more information to the instantiator about how the type will be
+used in the generic and it enforces (as opposed to relying on a convention)
+that requirement for the generic's implementation.
+
+Still, I am not convinced that it is worth the added complexity.
+I don't think I've ever wished that I had this feature.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, April 11, 2018  6:10 PM
+
+> > I think Type_Invariant is lowest priority. 
+> 
+> I think Type_Invariant for a generic formal type is a bad idea.
+> Defining the "boundary" seems like it could get messy; it probably 
+> could be done, but would it be worth the trouble?
+
+That's what I said in the AI. The "boundary" for the formal type and the
+actual type would naturally be different, which would make its implied use
+as a restriction on the actual impossible. Or you could try to fix that, but
+it (like Type_Invariant itself) would be a mess. Best to stay out of that 
+morass.
+
+... 
+> I think there is a stronger argument for allowing this construct than 
+> what was given (but perhaps still not strong enough to justify 
+> allowing it).
+> 
+> Specifying the Dynamic_Predicate as part of the 
+> instantiator/instantiatee contract is different than declaring a 
+> subtype within the generic and then, by convention, using that subtype 
+> instead of the original formal type everywhere within the generic.
+> 
+> It conveys more information to the instantiator about how the type 
+> will be used in the generic and it enforces (as opposed to relying on 
+> a convention) that requirement for the generic's implementation.
+
+I didn't emphasize this part in the AI because the proposed dynamic-only 
+feature really doesn't provide it. You'd need a form of static contract
+"matching" (discussed in AI12-0273-1 - not for Ada 2020 - hopefully I'll get
+everything posted today) in order to really provide that capability.
+
+But one purpose of all of these constructs on generic formals is to provide 
+requirements on the actuals in an instantiation. Even if those requirements 
+are not actually enforced, they're still there.
+
+This, again, is similar to the purpose of giving Pre/Post on an 
+access-to-subprogram type, or a Dynamic_Predicate that references the 
+designated object of an access-to-object type.
+
+For instance, if you have:
+
+     generic
+        type Foo is ...
+        with function Reduce (Obj : Foo) return Integer
+           with Post => Reduce'Result in -9 .. 9;
+     package Gen is
+        ...
+     end Gen;
+
+An instantator of Gen can see that a function that can return any integer is
+inappropriate for this generic; passing it just causes a risk of an
+Assertion_Error for no good reason.
+
+If we bury that information somewhere else, it then just ends up as a comment
+somewhere associated with the generic. I think we all agree that an explicit 
+Pre/Post is much better than a comment.
+
+One would hope that CodePeer/SPARK would start checking instances for 
+"compatibility" in this sense.
+
+An example from the containers. There is a text requirement that all of the 
+ordering operators passed to the containers represent a "strict weak ordering".
+It would be so much better to specify this in the container generic contract
+rather than an obscure blanket rule buried in A.18.
+
+For instance:
+generic
+   type Element_Type is private;
+   with function "<" (Left, Right : Element_Type) return Boolean is <>
+       with Post => Is_Strict_Weak_Ordering (Left, Right);
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+package Ada.Containers.Ordered_Sets is
+
+Note: We can't actually do this particular thing because it isn't sensible to 
+write the function Is_Strict_Weak_Ordering. The definition is essentially:
+    function Is_Strict_Weak_Ordering (Left, Right : Element_Type) return Boolean is
+         (if Left < Right then (for all Z in Element_Type => (Left < Z or Z < Right))
+          elsif Right < Left then (for all Z in Element_Type => (Right < Z or Z < Left)));
+but we don't have an enumerator for all values of Element_Type [for good
+reason -- such values might not be numerable] and even if we did it would
+usually be too expensive to evaluate. Moral: not everything is reasonable to
+write as a contract.
+
+Still, the capability seems useful in the many cases where a requirement can be 
+usefully modeled as a Pre/Post.
+
+> Still, I am not convinced that it is worth the added complexity.
+> I don't think I've ever wished that I had this feature.
+
+Note that I didn't put Dynamic_Predicate on formal types into the proposed AI.
+Doing so would have taken some wording, and it seemed to answer a question
+that nobody had asked. But it did seem to me that someone would be asking it
+soon enough, because it is an obvious sort of additional contract.
+
 ****************************************************************
+

Questions? Ask the ACAA Technical Agent