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,c91e482ae6ca8d4b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!p23g2000vbl.googlegroups.com!not-for-mail
From: xorque <xorquewasp@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Clarification for SPARK postconditions on hidden subprograms.
Date: Fri, 26 Jun 2009 03:41:40 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <3ac1c20c-32ad-4a89-8661-28625f23a7e8@p23g2000vbl.googlegroups.com>
References: <898abcf6-7315-4015-9d73-d9365a870294@v2g2000vbb.googlegroups.com>
	<2bcddeb9-4823-469b-b496-d37f183fd929@s16g2000vbp.googlegroups.com>
	<b5695e1d-8385-4820-a710-94d269f0ddb3@r25g2000vbn.googlegroups.com>
	<189c5cbe-10ce-46c7-89df-dcafcc78cfad@s6g2000vbp.googlegroups.com>
NNTP-Posting-Host: 62.249.247.223
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1246012901 13081 127.0.0.1 (26 Jun 2009 10:41:41
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 26 Jun 2009 10:41:41 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: p23g2000vbl.googlegroups.com; posting-host=62.249.247.223;
	posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7)
	Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6638
Date: 2009-06-26T03:41:40-07:00
List-Id: <comp.lang.ada>

Rod Chapman wrote:
>
> Does this function have a global variable by any chance? If so, then
> in annotations, you have to give additional actual parameters.
> See section 3.3 of the Examiner_GenVCs manual.

It does indeed. Checking now...

> We have very deliberately made the _entire_ set of manuals
> available with the GPL release.  We hope in future to make
> more tutorial-style information available on-line.

And they are certainly appreciated. They're not particularly
easy to search, however, especially when you're not exactly
sure what you're looking for. I'm really after more practical
examples - the case studies in the manuals are somewhat
abstract and Tokeneer is a bit on the large side. I look forward
to the tutorials.