From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,585fd78267abd80c X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: "Alex R. Mosteo" Newsgroups: comp.lang.ada Subject: Re: On pragma Precondition etc. Date: Fri, 25 Jul 2008 13:44:28 +0200 Message-ID: <6etsi6F8mbmbU2@mid.individual.net> References: <4889886d$0$18827$9b4e6d93@newsspool2.arcor-online.net> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7Bit X-Trace: individual.net 5KgNZ98Bz06tVxVU5OsvdwWDcmNm5M/iNMYJqZnX3qnlbctRE= Cancel-Lock: sha1:0jQqCIVl/4rRtFibNo+ivKpyb4c= User-Agent: KNode/0.10.9 Xref: g2news1.google.com comp.lang.ada:1325 Date: 2008-07-25T13:44:28+02:00 List-Id: mockturtle wrote: > > > stefan-lu...@see-the.signature ha scritto: > >> On Fri, 25 Jul 2008, Georg Bauhaus wrote: >> >> > We would have something like >> > >> > function More(X, Y: Integer); >> > -- ... >> > pragma Precondition(More, X > 2 * Y); >> > >> > >> > function Less(X, Y: Integer); >> > -- ... >> > pragma Precondition(Less, X < 2 * Y); >> > >> > And now there is no doubt about the subprogram to which a >> > Pre-/Postcondition belongs. (A rule that a spec Pre-/Postcondition >> > pragma must come right after its subprogram will establish >> > consistency.) >> >> This seems to break with overloading of subprogram names. I seem to recall >> that >> "pragma Inline(Foo)" >> is asking to inlie *all* functions / procedures with the name "Foo". This >> may be OK for inlining, but you definitively don't want to use the same >> preconditions which happen to have the same way. Consider the following: > > What about _allowing_ for the name of the procedure to appear in > the pragma? The true syntactic link would be given by the pragma > position > and the procedure name would act as a "double check" to be sure that > things were not messed up. Of course this does not save you if you > permute the pragma of overloaded functions... > > --- Piling more suggestions: I understand the point of using pragmas by Gnat at this stage, but if this is going to be standardized perhaps the syntax of a declaration could be changed. For example: function Foo (X, Y : Something) return Whatever with Precondition (Blah) and Postcondition (Urgh); So now it is all a indivisible whole and the OP concern is gone. I haven't seen Eiffel code. How do they do this?