!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 => Reduce'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. ****************************************************************