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: a07f3367d7,4e0df1f3e9a1ac5d X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!f35g2000vbl.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK: Problem with using constants in a post annotation Followup-To: comp.lang.ada Date: Thu, 13 Jan 2011 03:15:08 -0800 (PST) Organization: http://groups.google.com Message-ID: <880b38c9-e06a-4fe5-8285-bd30a8471639@f35g2000vbl.googlegroups.com> References: NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1294917308 32733 127.0.0.1 (13 Jan 2011 11:15:08 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 13 Jan 2011 11:15:08 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: f35g2000vbl.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:17384 Date: 2011-01-13T03:15:08-08:00 List-Id: 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 appears = here > =A0 =A0--# =A0 =A0 =A0(P1.Val >=3D C2 -> P1.Val =3D 1); =A0 =A0 -- error = 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 o= r > not visible at this point. > 14:30 =A0 Semantic Error =A0 1 - The identifier C2 is either undeclared o= r > 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. This seems to occur when a pre- and/or post-condition is refined but there is no refined information flow (ie the derives annotation). I 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