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 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.224.215.194 with SMTP id hf2mr33199241qab.0.1368989649853; Sun, 19 May 2013 11:54:09 -0700 (PDT) X-Received: by 10.49.71.75 with SMTP id s11mr190643qeu.20.1368989649785; Sun, 19 May 2013 11:54:09 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!t11no416707qal.0!news-out.google.com!y6ni50289qax.0!nntp.google.com!t11no416700qal.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sun, 19 May 2013 11:54:09 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=81.129.168.208; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe NNTP-Posting-Host: 81.129.168.208 References: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com> <5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com> Subject: Re: SPARK Question From: phil.clayton@lineone.net Injection-Date: Sun, 19 May 2013 18:54:09 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 6275 Xref: news.eternal-september.org comp.lang.ada:15624 Date: 2013-05-19T11:54:09-07:00 List-Id: On Tuesday, 7 May 2013 21:44:12 UTC+1, Jacob Sparre Andersen news wrote: > "Georg Bauhaus" <...@futureapps.de> wrote in message=20 > news:...@newsspool4.arcor-online.net... > > On 07.05.13 08:59, Yannick Duch=EF=BF=BDne (Hibou57) wrote: > >> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley=20 > >> <...@gmail.com> a =EF=BF=BDcrit: > >>> Assuming you are using the latest version of SPARK, the simplest way = to > >>> do this is to also include the proof function Vec_Length in the body, > >>> and give it a return annotation. So in the spec put: > >>> > >>> --# function Vec_Length (The_Vector : in Basic_Vector) > >>> --# return Positive; > >>> > >>> function Get_Value > >>> (The_Vector : in Basic_Vector; > >>> At_Position : in Positive) > >>> return Basis_Type; > >>> --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector)= ; > >>> > >> > >> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: abil= ity=20 > >> to define something for use in pre/post only, without injecting it in = the=20 > >> real program. That's finally what the above do. > >> > > > > In practical cases, contract-only predicates might well vanish > > during optimization phases in compilers, I think, in case the > > programmers decide that assertion checking can be turned off. >=20 > I agree. Compilers do not include dead code in programs, regardless of wh= y=20 > that code is dead. So there is little practical difference between having= =20 > some sort of contract-only predicate functions and having them generally= =20 > available. >=20 > Moreover, I'm very skeptical that having contract-only functions is a goo= d=20 > idea, especially for preconditions. For a precondition, the caller is=20 > supposed to ensure that the precondition is true before making the call. = How=20 > can a programmer do this if the predicate is not available to them? For= =20 > instance, it's common to have code like: >=20 > if Is_Open (Log_File) then > Put_Line (Log_File, ...); > -- else don't log, file has failed for some reason. > end if; >=20 > where the precondition on Put_Line includes "Is_Open (File)". >=20 > If the programmer can't write Is_Open in their code, they cannot avoid th= e=20 > failure nor program around it. All they can do is handle the exception,= =20 > which is often the worst way to handle the situation. >=20 > Similarly, postconditions often include conditions that hold true after t= he=20 > call, and it's quite common for those conditions to feed into following= =20 > preconditions (as in Post =3D> Is_Open(File) after a call to Open). So, a= s=20 > much as possible, postconditions should use the same functions that are u= sed=20 > in preconditions. (The more that's done, the more likely that the compile= r=20 > can completely eliminate the pre- and post- condition checks even when=20 > they're turned on.) Addressing the last paragraph above, the basis of the point is that reusing= the same syntactic form of predicate in pre- and postconditions makes it e= asy for a compiler to spot that a predicate is a consequence of an earlier = predicate. I certainly agree with that! But surely this would allow only = the _subsequent_ occurrences of the predicate to be optimized out? Above, = you seem to suggest that both the initial and subsequent occurrence of a pr= edicate can be optimized out. In the example above example, it may be poss= ible for the initial occurrence, the postcondition Is_Open(File) of subprog= ram Open, to be optimized out but that is surely for different reasons - th= e compiler having special knowledge about the subprogram Open. In general,= for user-defined subprograms, determining statically whether a predicate P= (X) holds is, in general, difficult. Once established, it is straightforwa= rd to use the theorem=20 P(X) =E2=87=92 P(X) to establish that subsequent occurrences of the same form hold. Separately, even when reusing the same syntactic form of predicate in pre- = and postconditions, optimizing out subsequent occurrences of the predicate = may not be possible as often as one would hope. Given two occurrences of t= he predicate P(X), to establish that the subsequent occurrence holds, it ne= cessary (for the theorem above) to establish that the X is the same in both= occurrences. In the case that X is visible outside its package and betwee= n the two occurrences of P(X) there is a call to a subprogram in another pa= ckage, I can't see how a compiler would know that X won't be changed. (I'm= assuming that compilers don't look at the bodies of other packages when co= mpiling a package.) To avoid such issues, formal methods tools typically r= equire subprograms to have a 'frame' annotation that indicates which variab= les a subprogram may change. So, in summary, optimizing out predicates in pre- and postconditions may no= t be that easy. Phil