Re: Q: SPARK visibility rules and inherit annotations.

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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

> 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 some
> 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 is  
> 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 have
> those things?

Hi Peter :)

I could find something interesting, experimentally.

I you use “Cryptographic_Services.Octet_Array” instead of  
“TMLib.Cryptographic_Services.Octet_Array”, this will probably 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 reference  
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.