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: a07f3367d7,69c50fc0d29ced1b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re: Q: SPARK visibility rules and inherit annotations.
Date: Wed, 19 May 2010 18:22:33 +0200
Organization: Ada At Home
Message-ID: <op.vcynrvxnule2fv@garhos>
References: <4bf3fce5$0$2399$4d3efbfe@news.sover.net>
NNTP-Posting-Host: H0Ci3WDhdyTdURnA0sNEyw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:11773
Date: 2010-05-19T18:22:33+02:00
List-Id: <comp.lang.ada>

Le Wed, 19 May 2010 17:04:05 +0200, Peter C. Chapin <pcc482719@gmail.com=
>  =

a =C3=A9crit:

> I'm working on a SPARK program. Right now I'm just doing design so my =
 =

> focus is
> on package specifications; there are no package bodies. I'm having som=
e
> trouble with the following:
>
> with TMLib.Cryptographic_Services;
>
> --# inherit TMLib.Cryptographic_Services;
> package TMLib.Credentials is
>    type Credential_Type is private;
>
>    -- Converts the raw bytes of a certificate transfer format to a  =

> credential.
>    procedure Certificate_To_Credential
>      (Raw_Data   : in TMLib.Cryptographic_Services.Octet_Array;
>       Credential : out Credential_Type;
>       Valid      : out Boolean);
>    --# derives Credential from Raw_Data &
>    --#         Valid      from Raw_Data;
>
>    -- Other stuff not shown here...
> end TMLib.Credentials;
>
> The SPARK Examiner complains about the use of "Cryptographic_Services"=
  =

> in the
> declaration of the Raw_Data parameter to the procedure. Specifically I=
  =

> get
> error 754 that says (roughly) "The identifier Cryptographic_Services i=
s  =

> not
> declared or not visible." I am then told that I probably need both a  =

> 'with'
> statement in the context clause and an 'inherit' annotation. Don't I h=
ave
> those things?

Hi Peter :)

I could find something interesting, experimentally.

I you use =E2=80=9CCryptographic_Services.Octet_Array=E2=80=9D instead o=
f  =

=E2=80=9CTMLib.Cryptographic_Services.Octet_Array=E2=80=9D, this will pr=
obably work, as it  =

worked for me.

Here is what I did:


    -- ----------------------------------------------------------------

    package TMLib is

       -- Empty root package.

    end TMLib;

    -- ----------------------------------------------------------------

    package TMLib.Cryptographic_Services is

       type Octet_Array is private;

    private

       type Octet_Array is range  0 .. 1;
       -- Dummy type for test purpose.

    end TMLib.Cryptographic_Services;

    -- ----------------------------------------------------------------

    with TMLib.Cryptographic_Services;
    --# inherit TMLib.Cryptographic_Services;

    package TMLib.Credentials is

       type Credential_Type is private;

       -- Converts the raw bytes of a certificate transfer
       -- format to a credential.
       procedure Certificate_To_Credential
         (Raw_Data   : in Cryptographic_Services.Octet_Array;
          Credential : out Credential_Type;
          Valid      : out Boolean);
       --# derives Credential from Raw_Data &
       --#         Valid      from Raw_Data;

    private

       type Credential_Type is range  0 .. 1;
       -- Dummy type for test purpose.

    end TMLib.Credentials;

It seems to expect the path to the package to be expressed explicitly as=
 a  =

path in a child package hierarchy. Now will have to look to the referenc=
e  =

about it, as I don't remember about this kind of detail anywhere.

Note: I still get warnings with the above (some because information flow=
  =

analysis was enabled)

Is it OK for you that ?

-- =

There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between=
  =

SPARK and VDM, please, let me know. Will enjoy to talk with you about it=
.