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

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

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.