SPARK syntax and “use type” : lack of feature ?

SPARK syntax and “use type” : lack of feature ?

[Yannick Duchêne (Hibou57)]

Hi,

I meet a strange behavior with the SPARK syntax checker (via the examiner).

If I have something of the form

    procedure My_Procedure
    is
       Who_Know_What : Who_Know_What_Type;
       use type My_Type;
    begin
       ... bla-bla-bla ...
    end My_Procedure;

it's OK.

While if I have something like

    procedure My_Procedure
    is
       use type My_Type;
    begin
       ... bla-bla-bla ...
    end My_Procedure;

Then the spark syntax checker complains “Syntax Error reserved "IS" cannot  
be followed by "USE" here.”

So, if the “use type” comes after any kind of declaration (type or  
entity), that's OK, but if this comes at the first place, or worst, alone,  
so that it cannot be anywhere than at the first place, then it is rejected.

Strange. So much strange to me that I wonder if weither or not this is  
something which had not been seen as a possible issue.

What people here think about it ?

Is SPARK missing something or is there a rational ?

Re: SPARK syntax and “use type” : lack of feature ?

[Phil Thornley]

On 24 May, 19:41, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Hi,
>
> I meet a strange behavior with the SPARK syntax checker (via the examiner).

I can't get the behaviour that you are reporting (I'm still on GPL
version 8.1.1) - can you post a complete SPARKable example?

> If I have something of the form
>
>     procedure My_Procedure
>     is
>        Who_Know_What : Who_Know_What_Type;
>        use type My_Type;
>     begin
>        ... bla-bla-bla ...
>     end My_Procedure;
>
> it's OK.

This definitely should not be OK, 'use type' clauses should (normally)
only appear as part of a context clause.

With this code in a package body:

    type A_Type is range 1 .. 10;

    procedure My_Procedure(A : in     A_Type;
                           B : in     A_Type;
                           X :    out Integer)
    --# derives X from A, B;
    is
       Y : Integer;
       use type A_Type;
    begin
       Y := Integer(A + B);
       X := Y;
    end My_Procedure;

I get a semantic error (112) at the 'use type'.
"A use type clause may not appear here.  They are only permitted as
part of a context clause or directly following an embedded package
specification."

(although, of course, a use type clause never needs to reference a
type in the same package).

> While if I have something like
>
>     procedure My_Procedure
>     is
>        use type My_Type;
>     begin
>        ... bla-bla-bla ...
>     end My_Procedure;
>
> Then the spark syntax checker complains “Syntax Error reserved "IS" cannot  
> be followed by "USE" here.”

I do get that error (which is to be expected since a 'use type' clause
must follow a semi-colon).

> Is SPARK missing something or is there a rational ?

Not sure, unless you can post your complete SPARKable code?

Cheers,

Phil

Re: SPARK syntax and “use type” : lack of feature ?

[Rod Chapman]

>On May 25, 12:01 am, Phil Thornley <phil.jpthorn...@googlemail.com> wrote:

Phil is basically correct.

"use type" is only permitted in the language definition in two places:

1) As a context clause

2) Directly following an embedded package specification.

BUT...

1) is fully implemented.

2) is NOT implemented by any version of the Examiner.

This is documented (somewhat briefly) in section 11.1.1 of
the toolset release note, and page 402 of the book.
 - Rod

Re: SPARK syntax and “use type” : lack of feature ?

[Yannick Duchêne (Hibou57)]

Le Tue, 25 May 2010 01:01:08 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:

> On 24 May, 19:41, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
> wrote:
>> Hi,
>>
>> I meet a strange behavior with the SPARK syntax checker (via the  
>> examiner).
>
> I can't get the behaviour that you are reporting (I'm still on GPL
> version 8.1.1)
I'm using SPARK 8.1.1 too (I'm not working for a company).

> - can you post a complete SPARKable example?
Sure, here are two:

    package body Dummies is

       procedure Dummy
       is
          use type Natural;
          Entity : Natural;
       begin
          null;
       end Dummy;

    end Dummies;

This latter fails syntax check pass with the message “Syntax Error   
reserved word "IS" cannot be followed by reserved word "USE" here.”

    package body Dummies is

       procedure Dummy
       is
          Entity : Natural;
          use type Natural;
       begin
          null;
       end Dummy;

    end Dummies;

This latter one pass syntax check without any error message (just two  
obvious warnings).

The only difference, is the place where the “use type” clause comes. If it  
comes first, an error message is raised, if it comes after any declaration  
(type or entity), that's OK.

> This definitely should not be OK, 'use type' clauses should (normally)
> only appear as part of a context clause.
Eh, I'm dreaming, I have the result I am reporting.

> With this code in a package body:
>
>     type A_Type is range 1 .. 10;
>
>     procedure My_Procedure(A : in     A_Type;
>                            B : in     A_Type;
>                            X :    out Integer)
>     --# derives X from A, B;
>     is
>        Y : Integer;
>        use type A_Type;
>     begin
>        Y := Integer(A + B);
>        X := Y;
>     end My_Procedure;
I was doing a syntax check only (I feel it is important to state this, as  
you come with an example using Derives clauses).

I am preparing a set of packages to be later checked with SPARK. As a  
first step, I have to modify some little stuff to ensure it is valid SPARK  
syntax (like adding explicit type indication in “for Index in 1 .. N”  
which have to be turned into “for Index in Index_Type range 1 .. N”).

This is doing so, I've meet this strange thing.

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

Re: SPARK syntax and “use type” : lack of feature ?

[Yannick Duchêne (Hibou57)]

Le Tue, 25 May 2010 09:29:43 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:

>> On May 25, 12:01 am, Phil Thornley <phil.jpthorn...@googlemail.com>  
>> wrote:
>
> Phil is basically correct.
>
> "use type" is only permitted in the language definition in two places:
>
> 1) As a context clause
>
> 2) Directly following an embedded package specification.
>
> BUT...
>
> 1) is fully implemented.
>
> 2) is NOT implemented by any version of the Examiner.
>
> This is documented (somewhat briefly) in section 11.1.1 of
> the toolset release note, and page 402 of the book.
>  - Rod
Unfortunately, I've understood the documentation is somewhat incorrect or  
at least is missing some stuffs, so I'm not always referring to it.

As an example, the SPARK 95 reference states that renames clause can be  
use to drop parent part of package path only and the package have to be  
renamed using its original name exactly ; so, Parent.Child should only be  
renamed as Child to be able to refer to it without having to write the  
“Parent.” every where.

But I could rename some package using other names. The same with  
procedures renaming.

The same with generics. The SPARK reference say the only generic  
instantiation allowed is instantiation of Unchecked_Conversion. However, I  
have some generic packages instantiation, and the syntax checker do not  
complain at all about it. Well, may be it will fail later at the semantic  
analysis, I hope not, or else I will have to drop SPARK... I believe it  
will be OK, as I saw some words somewhere stating SPARK now support  
generic.

Time to say I've also encountered strange things with generic  
instantiation. I can instantiate a generic package only if the package  
name has no prefix and trying to instantiate something like “is new  
Parent.Child (Formal_Parameter => ...)” fails, and “is new Child  
(Formal_Parameter => ...)” is accepted.

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

Re: SPARK syntax and “use type” : lack of feature ?

[Phil Thornley]

On 25 May, 21:05, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

[...]
> This latter one pass syntax check without any error message (just two  
> obvious warnings).
>
[...]

> Eh, I'm dreaming, I have the result I am reporting.
[...]

> I was doing a syntax check only (I feel it is important to state this, as  
> you come with an example using Derives clauses).

AAAAHHHHHHHH - I hadn't noticed that your OP said "syntax check" -
that is why you are not getting an error on the first example - it is
not a syntax error. (Presumeably because the preceeding declaration
*might* be an embedded package - which is allowed by the language
definition even if it's not implemented by the Examiner.)

(But it is a semantic error, as shown by my earlier response.)

Cheers,

Phil

Re: SPARK syntax and “use type” : lack of feature ?

[Rod Chapman]

On May 26, 12:18 am, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> On 25 May, 21:05, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
> wrote:
> > I was doing a syntax check only (I feel it is important to state this, as  
> > you come with an example using Derives clauses).

Please don't use the "syntax check only" option - I wish we'd
never put it in there!

There are many many things which are allowed by the (context-free)
grammar used by the parser that are later rejected by the
semantic analyser - generic packages for one as you have
already discovered.
 - Rod

Re: SPARK syntax and “use type” : lack of feature ?

[Yannick Duchêne (Hibou57)]

Le Wed, 26 May 2010 09:38:49 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:
> There are many many things which are allowed by the (context-free)
> grammar used by the parser that are later rejected by the
> semantic analyser - generic packages for one as you have
> already discovered.
Uh-oh, this seems to mean there is really no-no support for generics.  
Unlike what I have believed I have read...


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