From: Phil Thornley on
On 14 May, 04:07, Yannick Duchêne (Hibou57) <yannick_duch...(a)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
From: Phil Thornley on
On 14 May, 05:15, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr>
wrote:

> > Is this file part of the language definition or did I missed some  
> > relevant documentation elsewhere ?
>
> Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs  
> for SPARK Programs)

Yannick,

As you are discovering, the documentation for the optional proof
assertions in SPARK is not easy to find (it is spread across several
documents, and rather scattered within those documents).

You might find it helps to look at the tutorials on www.sparksure.com
(one set for the proof annotations and one set for the Proof Checker).

Cheers,

Phil
From: Rod Chapman on
> As you are discovering, the documentation for the optional proof
> assertions in SPARK is not easy to find (it is spread across several
> documents, and rather scattered within those documents).

Noted. For SPARK Pro 9.0, we merged all the Proof material
into one manual and gave it the rather more obvious title "Proof
Manual".
We also produced a one-page clickable index to _all_ the manuals,
which has also proven useful.
- Rod Chapman, SPARK Team
From: Yannick Duchêne (Hibou57) on
Le Fri, 14 May 2010 10:17:50 +0200, Phil Thornley
<phil.jpthornley(a)googlemail.com> a écrit:
> As you are discovering, the documentation for the optional proof
> assertions in SPARK is not easy to find (it is spread across several
> documents, and rather scattered within those documents).
I wouldn't say so much. There was actually in the QR #1, a little “[VCG
3]: ...” and at the bottom of the card, something like “[VCG] Generation
of VCs for SPARK Programs”, so cross references are there ; this was just
that I missed one file (I finally moved all release notes documents
elsewhere to make the docs directory more handy).

> You might find it helps to look at the tutorials on www.sparksure.com
> (one set for the proof annotations and one set for the Proof Checker).
Seems good material :) The link goes to my bookmarks (will tell about it
at fr.comp.lang.ada also).

--
There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on
Le Fri, 14 May 2010 10:11:29 +0200, Phil Thornley
<phil.jpthornley(a)googlemail.com> a écrit:
> 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.
Oh, yes, I see. Thanks Phil

--
There is even better than a pragma Assert: an --# assert