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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,4e0df1f3e9a1ac5d X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!g25g2000yqn.googlegroups.com!not-for-mail From: George Newsgroups: comp.lang.ada Subject: Re: SPARK: Problem with using constants in a post annotation Date: Thu, 13 Jan 2011 04:23:30 -0800 (PST) Organization: http://groups.google.com Message-ID: <0baaf796-d54d-4489-96d0-387a8a7702ae@g25g2000yqn.googlegroups.com> References: <880b38c9-e06a-4fe5-8285-bd30a8471639@f35g2000vbl.googlegroups.com> NNTP-Posting-Host: 155.207.113.40 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-7 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1294921410 4281 127.0.0.1 (13 Jan 2011 12:23:30 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 13 Jan 2011 12:23:30 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: g25g2000yqn.googlegroups.com; posting-host=155.207.113.40; posting-account=6UhNNwoAAAAqPvbGV2FILHuA9mXqxy3m User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; GTB6.6; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; InfoPath.2; .NET4.0C),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:17386 Date: 2011-01-13T04:23:30-08:00 List-Id: On 13 =C9=E1=ED, 13:15, Phil Thornley wrote: > On Jan 13, 9:26=A0am, George wrote: > > > > > > > PLEASE IGNORE THE PREVIOUS. THE FOLLOWING IS A CORRECT VERSION OF THE > > MESSAGE: > > > Hello, > > > I'm trying to use inside a post annotation two constants that are > > declared in the package body. But, I can't do it, because the two > > constants are not recognised at the point where they are used in the > > annotation. Does anyone have an idea of how to overcome this problem? > > Is it possible to overcome this by using only annotations without > > changing the code? > > The package specification and body, as well as the error messages are > > shown below: > > > -- File P2.ads > > --# inherit P1; > > package P2 > > is > > =A0 =A0procedure Proc; > > =A0 =A0--# global in out P1.Val; > > =A0 =A0--# derives P1.Val from P1.Val; > > =A0 =A0--# post (P1.Val <=3D C1 -> P1.Val =3D 0) and =A0-- error appear= s here > > =A0 =A0--# =A0 =A0 =A0(P1.Val >=3D C2 -> P1.Val =3D 1); =A0 =A0 -- erro= r appears here > > > end P2; > > > -- File P2.adb > > with P1; > > package body P2 is > > > =A0 =A0C1: constant P1.Type :=3D 10; > > =A0 =A0C2: constant P1.Type :=3D 20; > > > =A0 =A0procedure Proc > > =A0 =A0is > > =A0 =A0 =A0 V1: P1.Type; > > =A0 =A0begin > > =A0 =A0 =A0 V1 :=3D P1.Val; > > =A0 =A0 =A0 if V1 <=3D C1 then > > =A0 =A0 =A0 =A0 =A0P1.Val :=3D 0; > > =A0 =A0 =A0 elsif V1 >=3D C2 then > > =A0 =A0 =A0 =A0 =A0P1.Val :=3D 1; > > =A0 =A0 =A0 end if; > > =A0 =A0end Proc; > > > end P2; > > > OUTPUT > > 13:30 =A0 Semantic Error =A0 1 - The identifier C1 is either undeclared= or > > not visible at this point. > > 14:30 =A0 Semantic Error =A0 1 - The identifier C2 is either undeclared= or > > not visible at this point. > > It always helps if complete (examinable) code is supplied - in this > case there seems to be a type declared in the package P1 called "Type" > - which can't be valid. > > The constants C1 and C2 are not visible in P2 specification as they > aren't declared until the body. > > If you don't want to move these declarations to the specification then > you can use parameterless proof functions to reference their values: > > --# function C1_Value return P1.Type; > --# function C2_Value return P1.Type; > > In theory you can use these functions in the postcondition in the > specification and provide a refined postcondition on the body of Proc > that does reference C1 and C2 - then you just need two user rules to > discharge the resulting refinement VC: > p1_user(1): c1_value may_be_replaced by 10; > p1_user(2): c2_value may_be_replaced by 20; > > BUT - there is an defect in the current (ie GPL 2010) version of SPARK > where this may generate incorrect VCs for Proc. =A0This seems to occur > when a pre- and/or post-condition is refined but there is no refined > information flow (ie the derives annotation). =A0I don't know of any > reliable workaround for this. > (I understand that the SPARK team have fixed this defect, so if you > are a supported customer you should be able to get an updated > Examiner.) > > If you are using the GPL version, and can't use a refined > postcondition, then just use the proof functions in the postcondition > in the spec and the above two rules - plus any others that are needed > - to discharge the resulting VCs. > > Cheers, > > Phil- =C1=F0=FC=EA=F1=F5=F8=E7 =EA=E5=E9=EC=DD=ED=EF=F5 =F3=E5 =F0=E1=F1= =DC=E8=E5=F3=E7 - > > - =C5=EC=F6=DC=ED=E9=F3=E7 =EA=E5=E9=EC=DD=ED=EF=F5 =F3=E5 =F0=E1=F1=DC= =E8=E5=F3=E7 - Thank you very much for your response.