Q: SPARK visibility rules and inherit annotations.

Q: SPARK visibility rules and inherit annotations.

[Peter C. Chapin]

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?

Note that TMLib.Cryptographic_Services examines without error but it does
generate a warning because the private section is empty and currently hidden
from SPARK with a 'hide' annotation. It seems unlikely to me that has
anything to do with my problem. Note that TMLib.Cryptographic_Services is a
public child of TMLib.

I tried adding a 'with TMLib;' in the context clause but that didn't have any
effect. I realize the problem is probably something silly but I'm a bit
baffled here. Any pointers would be appreciated.

Thanks!

Peter

Re: Q: SPARK visibility rules and inherit annotations.

[Phil Thornley]

On 19 May, 16:04, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> 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?
>
> Note that TMLib.Cryptographic_Services examines without error but it does
> generate a warning because the private section is empty and currently hidden
> from SPARK with a 'hide' annotation. It seems unlikely to me that has
> anything to do with my problem. Note that TMLib.Cryptographic_Services is a
> public child of TMLib.
>
> I tried adding a 'with TMLib;' in the context clause but that didn't have any
> effect. I realize the problem is probably something silly but I'm a bit
> baffled here. Any pointers would be appreciated.
>
> Thanks!
>
> Peter

Peter,

The problem comes from the reference in one child of TMLib to another
child of TMLib.

Where this is the case, in the code and annotations - but not in the
inherit or context clauses - the common parent must not appear in the
name.

So change the line:
   (Raw_Data   : in TMLib.Cryptographic_Services.Octet_Array;
to:
   (Raw_Data   : in Cryptographic_Services.Octet_Array;

This comes from the rule that no entity in a SPARK program can have
more than one name - and in the Ada this type can be called either
TMLib.Cryptographic_Services.Octet_Array or
Cryptographic_Services.Octet_Array.

In SPARK the decision was to enforce the second of these.

(I'm sure that this is one error message that could be improved...)

Cheers,

Phil

Re: Q: SPARK visibility rules and inherit annotations.

[Yannick Duchêne (Hibou57)]

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.

Re: Q: SPARK visibility rules and inherit annotations.

[Gavino]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 485 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message
news:op.vcynrvxnule2fv@garhos...
>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.

See end of Section 7.1.1 of the SPARK Reference Manual:
"A child package is denoted by a direct name at places where its declaration
is directly visible."

Re: Q: SPARK visibility rules and inherit annotations.

[Peter C. Chapin]

Phil Thornley wrote:

> Peter,
> 
> The problem comes from the reference in one child of TMLib to another
> child of TMLib.
> 
> Where this is the case, in the code and annotations - but not in the
> inherit or context clauses - the common parent must not appear in the
> name.
> 
> So change the line:
>    (Raw_Data   : in TMLib.Cryptographic_Services.Octet_Array;
> to:
>    (Raw_Data   : in Cryptographic_Services.Octet_Array;

That did the trick, thanks. Now that you mention it, I seem to recall this
coming up for me before, although it was a while ago now.

Thanks for your explanation as well.

One thing I like about Ada in general is how you can express a design in
package specifications and then let the compiler check a few things about its
consistency before embarking on the implementation. With SPARK that effect is
even greater. For example in my Cryptographic_Services package the Examiner
initially complained about how there was no way to initialize one of my
private types. It was an oversight on my part (I was missing a critical
operation). I would have figured it out eventually, I'm sure, but it was nice
to have the issue caught earlier rather than later. It made me reflect on
what I was really trying to accomplish with the package and that can only be
a good thing.

Peter

Re: Q: SPARK visibility rules and inherit annotations.

[Yannick Duchêne (Hibou57)]

Le Wed, 19 May 2010 23:29:22 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> One thing I like about Ada in general is how you can express a design in
> package specifications and then let the compiler check a few things  
> about its
> consistency before embarking on the implementation. With SPARK that  
> effect is
> even greater. For example in my Cryptographic_Services package the  
> Examiner
> initially complained about how there was no way to initialize one of my
> private types.
I've noticed the same, it requires some good practice to be applied,  
someway comparable to what you could get with AdaControl and a good rules  
file (I mean AdaControl's rules). As an example, SPARK sees an error if  
you forget the give the name of procedure at its end statement.

While sometime, I would like to better understand some choices, like the  
one I've meet, which is that it does not accept nested package  
specifications, or, more important, why it don't wants “type ... is new  
...;”. If I could understand the rational behind this latter restriction,  
this could perhaps help me to redesign.

Re: Q: SPARK visibility rules and inherit annotations.

[Gavino]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 532 bytes --]


"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message
news:op.vczdx3teule2fv@garhos...
>While sometime, I would like to better understand some choices, like the
>one I've meet, which is that it does not accept nested package
>specifications, or, more important, why it don't wants "type ... is new
>...;". If I could understand the rational behind this latter restriction,
>this could perhaps help me to redesign.

It's to avoid overloading, especially the implicit declaration of
user-defined subprograms.

Re: Q: SPARK visibility rules and inherit annotations.

[Yannick Duchêne (Hibou57)]

Le Thu, 20 May 2010 13:03:01 +0200, Gavino <invalid@invalid.invalid> a  
écrit:
>> While sometime, I would like to better understand some choices, like the
>> one I've meet, which is that it does not accept nested package
>> specifications, or, more important, why it don't wants "type ... is new
>> ...;". If I could understand the rational behind this latter  
>> restriction,
>> this could perhaps help me to redesign.
>
> It's to avoid overloading, especially the implicit declaration of
> user-defined subprograms.
While this only occurs with tagged types, and SPARK 95 has support for  
tagged type. Or may be I'm wrong somewhere, or else, I did not understood  
what you were to say.


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

Re: Q: SPARK visibility rules and inherit annotations.

[Gavino]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 765 bytes --]


"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message
news:op.vc0hbmfnxmjfy8@garhos...
>Le Thu, 20 May 2010 13:03:01 +0200, Gavino <invalid@invalid.invalid> a
�crit:
>> It's to avoid overloading, especially the implicit declaration of
>> user-defined subprograms.
>While this only occurs with tagged types, and SPARK 95 has support for
>tagged type. Or may be I'm wrong somewhere, or else, I did not understood
>what you were to say.

Firstly, derived types can introduce overloaded enumeration literals, which
SPARK prohibits.
Secondly, if the parent type is one declared immediately within the visible
part of a package, then certain subprograms declared there are implicitly
declared for the derived type, again a form of overloading.

Re: Q: SPARK visibility rules and inherit annotations.

[Yannick Duchêne (Hibou57)]

Le Fri, 21 May 2010 12:42:53 +0200, Gavino <invalid@invalid.invalid> a  
écrit:
> Firstly, derived types can introduce overloaded enumeration literals,  
> which
> SPARK prohibits.
> Secondly, if the parent type is one declared immediately within the  
> visible
> part of a package, then certain subprograms declared there are implicitly
> declared for the derived type, again a form of overloading.
Yes, I forget about it, and especially about the first one (about  
enumeration literals).

This part of the one which is the most troublesome to me with SPARK, as I  
like to “type ... is new ...” some types are not be mixed and the  
interface defines special function when it is required. At least, when  
mixed is done, this is clearly visible and this is a clear indication on  
source review to look at it three times better than two.

Subtype is nice with SPARK, as validity conditions are checked. But if the  
source is to be as nice with and without SPARK, some troubles comes :  
subtype are not so much nice without SPARK. Ada with SPARK less needs  
derived types, and subtype is enough, but Ada without SPARK, needs derived  
types. So I can't have something which is good without SPARK too... or I  
have to make all numeric types independent, but doing so, I miss the  
expression of relations between these types.

Any way, thanks for your reply, which was the good one (this recalled me a  
detail I had forget, as I'm not really relying on it).

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