From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,48e1a3c594fb62e8
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!n15g2000yqf.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK
Date: Fri, 14 May 2010 01:17:50 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <30e0a8bd-e6f8-425c-9423-6eba7f35972d@n15g2000yqf.googlegroups.com>
References: <op.vcl6900wule2fv@garhos> <op.vcn8npjiule2fv@garhos>
	<op.vcogrmzyule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1273825070 10910 127.0.0.1 (14 May 2010 08:17:50
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 14 May 2010 08:17:50 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: n15g2000yqf.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:11599
Date: 2010-05-14T01:17:50-07:00
List-Id: <comp.lang.ada>

On 14 May, 05:15, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

> > Is this file part of the language definition or did I missed some =A0
> > relevant documentation elsewhere ?
>
> Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs=
 =A0
> 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