Re: SPARK Question

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University