Re: SPARK

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 14 May, 04:07, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> The Quick Reference Card #1 talks about “type assertion”:
>
> > A type assertion allows the user to specify the base type which the
> > compiler will associate with a signed integer type. The base type
> > must be supplied to the Examiner in the configuration file. This
> > assertion allows the Examiner to generate VCs which are much more
> > readily discharged [RTC 5.2].
>
> > Example:
> > type T is range 1 .. 10
> > --# assert T’Base is Short_Short_Integer;
>
> As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it  
> cannot care to any implicit representation clause either. So what's the  
> purpose of this kind of assertions ? Does the examiner check something  
> else which is not only the range ? Does it have something to deal with  
> type conversions ?
>
> --
> pragma Asset ? Is that true ? Waaww... great

Yannick,

These base type assertions are used to get the ranges for overflow
checks - see Section 5 of Generation of RTCs for SPARK Programs
(GenRTCs).

The Examiner can't validate this assertion, so it's up to the user to
get it right (but you might be able to use compiler assertions to
check it).  It is safe to assert a smaller base type than the compiler
actually chooses, so the portability problem can be reduced by
specifying the smallest possible base type.

Cheers,

Phil