!standard 6.1.1(1/5) 18-04-09 AI12-0272-1/01 !standard 6.1.1(40/5) !standard 7.3.3(1/5) !standard 7.3.3(2/5) !standard 7.3.3(8/5) !standard 7.3.4(5/5) !standard F.1(1) !class Amendment 18-04-09 !status work item 18-04-09 !status received 18-04-05 !priority Low !difficulty Easy !subject Contracts for generic formal parameters !summary Pre and Post are allowed on generic formal (nonabstract) subprograms. Default_Initial_Condition is allowed on generic formal private types. !problem Ada has a strong "contract model" for generic units, which makes it possible to reason about generic bodies without knowing anything about the properties of the actual types. This model is fairly weak for formal subprograms, where even the subtypes of the subprogram profile are ignored. This can make it hard to reason in generic bodies. We have allowed contracts on access-to-subprogram types, which have a similar situation (and sometimes, similar uses) as generic formal subprograms. It seems inconsistent to allow one but not the other. Similarly, contracts that are allowed on private types probably should be allowed on generic formal private types. !proposal (See Summary.) !wording Modify 6.1.1(1/5): For a noninstance subprogram{ (including a generic formal subprogram)}, a generic subprogram, or an entry, or an access-to-subprogram type, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1): AARM Proof: A generic formal subprogram is a subprogram, and there are no rules to prevent such use. Add after 6.1.1(40/5): Redundant[For a call on generic formal subprogram, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the actual subprogram, along with any specific precondition and specific postcondition of the formal subprogram itself.] AARM Proof: This follows from the general dynamic semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended. [Editor's note: This follows from the rules of 6.1.1(37/4), but we can't give paragraph references in AARM notes.] Modify 7.3.3(1/5) [from AI12-0265-1] For a private type or private extension {(including a generic formal type)}, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1): Modify 7.3.3(2/5) [from AI12-0265-1] This aspect shall be specified by an expression, called a *default initial condition expression*. Default_Initial_Condition may be specified on a private_type_declaration{,}[ o]r a private_extension_declaration{, a formal_private_type_definition, or formal_derived_type_definition}. Add after 7.3.3(8/5): [from AI12-0265-1] Redundant[For a generic formal type T, default initial condition checks performed are as determined by the actual type, along with any default initial condition of the formal type itself.] AARM Proof: This follows from the general dynamic semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended. [Editor's note: This follows from the rules of 7.3.3(8/5), but we can't give paragraph references in AARM notes.] Modify 7.3.4(5/5): [from AI12-0187-1] For a {nonformal} private type, {nonformal} private extension, or full type that does not have a partial view, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1): Modify F.1(1) {Representation attribute }Machine_Radix may be specified for a decimal first subtype (see 3.5.9) via an attribute_definition_clause; the expression of such a clause shall be static, and its value shall be 2 or 10. A value of 2 implies a binary base range; a value of 10 implies a decimal base range. !discussion We do not require any matching of contracts. This follows the model of access-to-subprogram types; the contracts are dynamically checked and no static rules are enforced. Since access-to-subprogram and formal subprograms are often used for similar purposes, it would be odd to have different rules for them. --- Note that the dynamic model for generic formal subprograms is identical to the case if the programmer had defined a new routine in the generic package specification: generic type Foo is ... with function Reduce1 (Obj : Foo) return Integer with Post => Reduce1'Result in -9 .. 9; with function Reduce2 (Obj : Foo) return Integer; package Gen is ... function Local_Reduce2 (Obj : Foo) return Integer with Post => Local_Reduce2'Result in -9 .. 9 is (Reduce2(Obj)); ... end Gen; If the actual subprogram for Reduce1 and Reduce2 is the same, then a call on Reduce1 has the same semantics as a call on Local_Reduce2. Thus, a compiler can always generate a wrapper for the formal subprogram if other implementations are unavailable. This is essentially the same model that is used for access-to-subprogram types. --- Note that Pre'Class and Post'Class aren't allowed because a generic formal subprogram is never primitive for a type (not even a formal abstract subprogram -- it's dispatching but not primitive). Also, Pre and Post aren't allowed for abstract subprograms, so no contracts are allowed for formal abstract subprograms. One could imagine allowing Pre'Class and Post'Class on formal abstract subprograms, but since it is not clear how to reconcile those with the static binding model for class-wide contracts, we don't allow this for now. --- Note that AI12-0064-2 unintentially allowed aspects that are neither operational nor representation to be used on generic formal parameters. So we just need wording to reinforce that is meant on these aspects. We also need to check that other aspects aren't allowed on formal parameters. Here's the list of such aspects: (1) Pre/Post - OK on formal subprograms - see above; (2) Pre'Class/Post'Class - Not allowed, see above; (3) Static_Predicate - Not allowed, a formal is never static; (4) Dynamic_Predicate - Not allowed, only allowed on type_declarations or subtype_declarations. (Probably OK to allow, but would require rewording, did not investigate.) (5) Type_Invariant/Type_Invariant'Class - Not allowed, since the places it is allowed are given syntactically. Don't want it, either (see below). (6) Default_Initial_Condition - Not allowed, since the places it is allowed are given syntactically. But we do want it, so fixed that above. (7) Stable_Properties/Stable_Properties'Class for types - We don't want to allow it (see AARM 7.3.4(6.a/5)), but there's no wording to that effect. We add the missing wording here. (8) Stable_Properties/Stable_Properties'Class for subprograms - Not allowed, formal subprograms are never primitive. (9) Machine_Radix - ??? This should be a representation aspect, but that's not mentioned in F.1. we fix that here. --- We don't want Type_Invariants to be used on formal subprograms. We do this because the rules for checking a type invariant apply to the unit in which it is defined - so it doesn't make sense for a generic formal (which is declared in a *different* unit than the actual). It might be possible to reconcile this, but thinking about it just makes my head hurt. !ASIS [Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.] !ACATS test ACATS B- and C-Tests are needed to check that the new capabilities are supported. !appendix From: Randy Brukardt Sent: Thursday, April 5, 2018 8:01 PM When we discussed AI12-0220-1 on Monday, it was immediately concluded that Pre/Post for generic formal subprograms was "a separate issue for a separate AI". What we didn't discuss further was whether we wanted such an AI. I'd be willing to write up such an AI, but I'd like to have some idea of whether we actually are interested first. It seems that a lot of the same uses occur for formal subprograms and for access-to-subprogram types. I would not want an incentive to use access-to-subprogram parameters when a formal subprogram would be an equivalent choice (in particular, inside of a generic unit). As Steve noted in the e-mail discussion, the subtypes (and thus predicates) of a formal subprogram are effectively ignored and thus cannot be relied upon. Thus, we don't have any way to declare useful contracts for such entities (even for things like ranges). Note if there is no checking, one can get the effect by declaring a local subprogram that calls the formal: generic type Foo is ... with function Reduce (Obj : Foo) return Integer with Post => Reduce'Result in -9 .. 9; package Gen is ... could be replaced by: generic type Foo is ... with function Reduce (Obj : Foo) return Integer; package Gen is ... function Local_Reduce (Obj : Foo) return Integer with Post => Local_Reduce'Result in -9 .. 9 is (Reduce(Obj)); and this would have the same semantics. This workaround has all of the obvious problems (need for an extra declaration, easy to forget to call the extra routine rather than the original) and also would be harder to do static checks for (as it would add an additional level of declaration without any information). In particular, the instantiator has no guidance that a function that can return 42 is not expected by the generic. Ideally, one would include matching checks for the actual subprogram during the instantiation, but we probably wouldn't want to do those for instances for the same reason that we didn't try to do them for 'Access. (Mainly that if we did them, they'd necessarily have to be fairly conservative, and that would prevent SPARK from doing better on similar checks -- even if SPARK could tell that a given subprogram's definition is OK, it couldn't be used because Ada would reject it.) Before doing anything, I would like to know how SPARK deals with formal subprograms. Does it allow contracts on them, and if so, how are they interpreted. I'd also like to know whether or not checking is expected on the instance. (It's not particularly hard to define using conformance, but it's not clear how likely it would be to cause issues in practice.) Thoughts?? **************************************************************** From: Steve Baird Sent: Friday, April 6, 2018 8:36 PM > Before doing anything, I would like to know how SPARK deals with > formal subprograms. Does it allow contracts on them, and if so, how > are they interpreted. SPARK sidesteps this issue by not trying to prove things about generic units; instead SPARK focuses on instances (including instance bodies). CodePeer takes the same approach; generic units are not analyzed but instances are. So I don't think this proposal would be a big deal (either positive or negative) for either SPARK or CodePeer. > I'd also like to know whether or not checking is expected on the instance. I'm not sure what you are asking here. Are you talking about static conformance checking of some kind, somehow checking that the actual subprogram already has the desired PPC? I wouldn't expect anything like that. Or are you talking about the question of whether PPC checks are performed at runtime in a case like generic with procedure P (X, Y : in out Integer) return Integer with Pre => ..., Post => ...; package G is procedure Ren (X, Y : in out Integer) renames P; end G; procedure PP (X, Y : in out Integer); -- no PPC package I is new G (P => PP); procedure Foo (X, Y : in out Integer) is begin PP (X, Y); -- clearly no PPC check here I.Ren (X, Y); -- PPC check here? end; ? It would be something new if the two calls in the preceding example behaved differently at runtime (i.e., if only the second call performs PPC checks). This example does suggest that this AI might be less straightforward than it seems at first. Along those lines, how would name resolution work? Could a precondition for a formal subprogram of a generic package reference something declared in the visible part of the package? > As Steve noted in the e-mail discussion, the subtypes (and thus > predicates) of a formal subprogram are effectively ignored and thus > cannot be relied upon. Given that Ada does not require subtype conformance between a formal subprogram and a corresponding actual, adding postconditions seems somewhat odd. We'll let you write explicit PPCs for these guys, but we won't let you assume the usual implicit contract (i.e., Pre => in and in-out param values belong to their respective subtypes, Post => same for in-out and out params and for a function result). This seems inconsistent to me. Would we also want to introduce a "Conforming" aspect for formal subprograms indicating that subtype conformance is required for a corresponding actual? Perhaps that question doesn't belong in this AI (there would be details to work out regarding the "conventions must match" part of subtype conformance). > Thoughts?? I can see how a precondition like the one in generic type File is limited private; with function Open_For_Reading (F : File) return Boolean; with function Read_Line (F : File) return String with Pre => Open_For_Reading (F); ... package G is ... end; could help clarify/document/define an interface. The question is whether it is worth the added complexity. **************************************************************** From: Tucker Taft Sent: Thursday, April 5, 2018 9:07 PM Because things are re-checked in each instance in SPARK (and CodePeer), it would not seem unreasonable to take the same general attitude about pre/post-conditions, though that clearly creates contract model violations, since we are re-checking generic bodies of each instance. I would say we should create the AI, but leave it low priority for now, and take it up again for Ada 2028 if we have interest in it. **************************************************************** From: Randy Brukardt Sent: Friday, April 6, 2018 9:54 PM > > I'd also like to know whether or not checking is expected > on the instance. > > I'm not sure what you are asking here. > > Are you talking about static conformance checking of some kind, > somehow checking that the actual subprogram already has the desired > PPC? > I wouldn't expect anything like that. Yes, that's what I was thinking about. But since it would be inconsistent with the rest of the language, probably it shouldn't be included. (SPARK probably ought to check such things, though, although if the model is to forget the contract model, it really doesn't matter.) > Or are you talking about the question of whether PPC checks are > performed at runtime in a case like > > generic > with procedure P (X, Y : in out Integer) return Integer with > Pre => ..., Post => ...; > package G is > procedure Ren (X, Y : in out Integer) renames P; > end G; > > procedure PP (X, Y : in out Integer); -- no PPC > > package I is new G (P => PP); > > procedure Foo (X, Y : in out Integer) is > begin > PP (X, Y); -- clearly no PPC check here > > I.Ren (X, Y); -- PPC check here? > end; > > ? It would be something new if the two calls in the preceding example > behaved differently at runtime (i.e., if only the second call performs > PPC checks). This example does suggest that this AI might be less > straightforward than it seems at first. Of course the checks would be different. The recently approved AI12-0220-1 does exactly this, you can write precisely this example using access-to-subprogram types: type PPtr is procedure (X, Y : in out Integer) return Integer with Pre => ..., Post => ...; procedure PP (X, Y : in out Integer); -- no PPC Pobj : PPtr := PP'Access; procedure Foo (X, Y : in out Integer) is begin PP (X, Y); -- clearly no PPC check here Pobj.all (X, Y); -- PPC check here end; > Along those lines, how would name resolution work? Could a > precondition for a formal subprogram of a generic package reference > something declared in the visible part of the package? I'd expect just the things allowed in the formal part + parameters. But you are right that some thought would be required to see if that enough. Definitely wouldn't want anything inside of the package (lest you get recursive dependence between the formals and the instantiated routines). > > As Steve noted in the e-mail discussion, the subtypes (and thus > > predicates) of a formal subprogram are effectively ignored and thus > > cannot be relied upon. > > Given that Ada does not require subtype conformance between a formal > subprogram and a corresponding actual, adding postconditions seems > somewhat odd. We'll let you write explicit PPCs for these guys, but we > won't let you assume the usual implicit contract (i.e., Pre => in and > in-out param values belong to their respective subtypes, Post => same > for in-out and out params and for a function result). > > This seems inconsistent to me. Would we also want to introduce a > "Conforming" aspect for formal subprograms indicating that subtype > conformance is required for a corresponding actual? In that case, a PPC check would also make sense. (It's not really that hard to define, it just would be a bit inflexible in that the "parts" would have to fully conform.) > Perhaps that question doesn't belong in this AI (there would be > details to work out regarding the "conventions must match" > part of subtype conformance). Right. And if you are doing that sort of matching, you really need contract conformance as well. That's clearly messier than just adding some additional checking possibilities. > > Thoughts?? > > I can see how a precondition like the one in > > generic > type File is limited private; > with function Open_For_Reading (F : File) return Boolean; > with function Read_Line (F : File) return String > with Pre => Open_For_Reading (F); > ... > package G is > ... > end; > > could help clarify/document/define an interface. > The question is whether it is worth the added complexity. To me, this is precisely the same question as whether they are valuable on access-to-subprogram types. The constructs are often used for similar things. So it's certainly worth it unless there is some complexity that I don't know about (this doesn't seem any harder than the access-to-subprogram was). **************************************************************** From: Randy Brukardt Sent: Friday, April 6, 2018 10:08 PM > Because things are re-checked in each instance in SPARK (and > CodePeer), it would not seem unreasonable to take the same general > attitude about pre/post-conditions, though that clearly creates > contract model violations, since we are re-checking generic bodies of > each instance. ...in SPARK/Codepeer, not in Ada (which isn't doing any static checking at all, and if it did [as Steve sort of proposed], then it would solely be at the instance). I can't really care if other people's tools mess up the Ada model -- that's out of our hands in any case. > I would say we should create the AI, but leave it low priority for > now, and take it up again for Ada 2028 if we have interest in it. Well, as this is a "directly related" to a WG 9 instruction ("improve contracts"), if it exists it would "leap" ahead of any non-easy AIs that aren't "directly related". So we'd have to have it on the agenda at least once (although we could explicitly decide to put it on Hold then). Moreover, the basic version as discussed is probably in the "easy" category: if there is no static matching required, the rule changes needed would be just a few places to make it clear that it is allowed to give Pre/Post in formal subprograms (substantially less than the access-to-subprogram rules in the recently approved AI12-0220-1, which required more wording since a type is not any form of subprogram) [presumably also renames-not-as-body]. I'd have to verify that, of course, which would take some effort. I suspect that the discussion would come down to a yes/no type of vote, again mirroring what happened with AI12-0220-1. The version involving static matching of subtypes and contracts (that Steve suggests in his mail) is a more complex beast, probably best left for Ada 2028. (I'd suggest a version for access-to-subprogram as well, so that contract matching would be an option for those who want it.) I could write up an empty version of this, mainly to keep the idea for the future -- I'd put it into the Hold vote. *************************************************************** From: Tucker Taft Sent: Saturday, April 7, 2018 5:32 AM I am easy either way. I don't think contracts are critical on generic formals at this point, but I agree that in the long run they make sense. And as you point out, enhanced contracts are one of our key goals for 202X. And I suppose someone coming from outside would naturally ask: "why no contracts on generic formals?". I suppose Default_Initial_Condition would also make sense on a 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. ****************************************************************