Re: SPARK Question

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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.