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

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

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.