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
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!newsfeed.kamp.net!newsfeed.kamp.net!newsfeed.freenet.ag!takemy.news.telefonica.de!telefonica.de!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 07 May 2013 09:54:02 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:17.0) Gecko/20130328 Thunderbird/17.0.5
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: SPARK Question
References: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com>
 <MPG.2beb2a4dab7f2a819896a7@news.zen.co.uk> <op.wwpcddnbule2fv@cardamome>
In-Reply-To: <op.wwpcddnbule2fv@cardamome>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 07 May 2013 09:53:59 CEST
NNTP-Posting-Host: ece81221.newsspool4.arcor-online.net
X-Trace: 
 DXC=[DWglTYT9BjEB;5>eE0T7m4IUK<Cl32<a4Fo<]lROoRa8kF<OcfhCOk?kaliLGR5R`nc\616M64>jLh>_cHTX3jm[c=cXDdjF3a
X-Complaints-To: usenet-abuse@arcor.de
Xref: news.eternal-september.org comp.lang.ada:15402
Date: 2013-05-07T09:53:59+02:00
List-Id: <comp.lang.ada>

On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley <phil.jpthornley@gmail.com> a écrit:
>> Assuming you are using the latest version of SPARK, the simplest way to
>> do this is to also include the proof function Vec_Length in the body,
>> and give it a return annotation. So in the spec put:
>>
>>    --# function Vec_Length (The_Vector : in Basic_Vector)
>>    --#   return Positive;
>>
>>    function Get_Value
>>      (The_Vector : in Basic_Vector;
>>       At_Position : in Positive)
>>       return Basis_Type;
>>    --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);
>>
>
> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability to define something for use in pre/post only, without injecting it in the real program. That's finally what the above do.
>

In practical cases, contract-only predicates might well vanish
during optimization phases in compilers, I think, in case the
programmers decide that assertion checking can be turned off.