From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on ip-172-31-65-14.ec2.internal X-Spam-Level: X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00,T_SCC_BODY_TEXT_LINE, XPRIO autolearn=ham autolearn_force=no version=3.4.6 Path: eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Contracts in generic formal subprogram Date: Sat, 8 Apr 2023 04:09:38 -0500 Organization: A noiseless patient Spider Message-ID: References: <0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com> Injection-Date: Sat, 8 Apr 2023 09:09:40 -0000 (UTC) Injection-Info: dont-email.me; posting-host="8cffde185656e4854c99d85efea8bf85"; logging-data="1285900"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19t3ycVfOnWkqOp/owAM8KkeVpAHZ+xTzo=" Cancel-Lock: sha1:v1Umh4OMpm/owYCnEIAMdViXBIQ= X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246 X-RFC2646: Format=Flowed; Original X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 Xref: feeder.eternal-september.org comp.lang.ada:65080 List-Id: Ada 2022 allows such contracts; Ada 2012 did not. (See 6.1.1, and specifically 6.1.1(1/5)). Whether your compiler has caught up, who knows. Logically the contracts should "match" (with the weakening/strengthing that Dmitry mentioned), but that was too hard for Ada, so they're just additive. (A proper matching mechanism is more the sort of thing that SPARK does, Ada only enforces these contracts at runtime) That is, when you call through a generic formal subprogram, you enforce the preconditions of both the formal and the actual subprogram, and similarly for the postconditions. If they mismatch, you might not be able to make a successful call. If it hurts, don't do that. ;-) Randy. "mockturtle" wrote in message news:0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com... Dear.all, this is something that looked like a natural and nice idea to me, but the compiler disagree :-): specifying contracts in formal subprograms in generic declarations. Actually, RM 12.6 does not prohibit this on a syntactic level (a aspect_specification part is included), but the compiler complains. To understand what I mean, please check the following real code toy-zed (can you hear the grammar screaming?) ----------------------- generic type Ring is private; with function Divides (Num, Den : Ring) return Boolean; with function Is_Invertible (X : Ring) return Boolean; with function Inv (X : Ring) return Ring with Pre => Is_Invertible (X); with function Gcd (X, Y : Ring) return Ring with Post => Divides (X, Gcd'Result) and Divides (Y, Gcd'Result); package Pippo is -- stuff end Pippo; ---------------------------------- The meaning I have in mind is something like * For "Pre" aspect: who writes function Inv can assume that X is invertible since Inv will never be called (by the package code, at least) with X not invertible. Also Inv cannot have a stricter pre-condition. In a sense, the package expects Inv to work correctly if and only if the pre-condition is true. * For "Post" aspect: I expect that the result of GCD satisfies the post condition. Post conditions for the actual subprogram can be stricter, as long as the post condition of the formal parameter is satisfied. For example, if Ring is Integer, GCD could always return a positive value that divides both X and Y. The fact that the result is positive does not hurt. Should the actual subprogram specify the same contract? I am not sure (and I guess this could be a stumbling block for the adoption of this idea). One could say that the actual subprogram gets a contract that is the AND of the actual subprogram and the contract specified in the generic declaration, it is up to the programmer to check that they are compatible. I guess the compatibility could be verified by the compiler itself in simple cases, but I expect that this could not be feasible in some cases (maybe of academic interest?). Riccardo