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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!feeder.news-service.com!newsfeed00.sul.t-online.de!t-online.de!news-lei1.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: On pragma Precondition etc. Date: Fri, 25 Jul 2008 12:50:41 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <4889886d$0$18827$9b4e6d93@newsspool2.arcor-online.net> Reply-To: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: tigger.scc.uni-weimar.de 1216978648 29424 141.54.178.228 (25 Jul 2008 09:37:28 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Fri, 25 Jul 2008 09:37:28 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <4889886d$0$18827$9b4e6d93@newsspool2.arcor-online.net> Xref: g2news1.google.com comp.lang.ada:1322 Date: 2008-07-25T12:50:41+02:00 List-Id: 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: function More(X, Y: Integer) return Integer; pragma Precondition(More, X > 2 * Y); --1-- function More(X, Y: Integer) return Boolean; pragma Precondition(More, (X>0) or (Y>0)); --2-- function More(X, Y: Whatever) return Whatever; --3-- The intention is that precondition --1-- sticks to the function returning Integer and precondition --2-- sticks to the one returning Boolean -- not that both preconditions stick to both functions! And neither precondition should stick to the function marked by --3--. Depending on the type Whatever, that shouldn't even compile ... So the syntactical link between a subprogram declaration and its precondition cannot just depend on the subprogram name. But then, the function name actually becomes redundant, and the current GNAT convention appears to be the better one: function More(X, Y: Integer) return Integer; pragma Precondition(X > 2 * Y); --1-- function More(X, Y: Integer) return Boolean; pragma Precondition((X>0) or (Y>0)); --2-- function More(X, Y: Whatever) return Whatever; --3-- An alternative would be to repeat the entire function declaration in the pragma: function More(X, Y: Integer) return Integer; pragma Precondition(function More(X,Y: Integer) return Integer, X > 2 * Y); --1-- Ada is always a bit verbose, which often is good for readability. But this would throw a bit too much of redundant information at the reader. Stefan -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------