Re: SPARK Question

["Jacob Sparre Andersen news" <randy@rrsoftware.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2699 bytes --]

"Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote in message 
news:5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net...
> 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.

I agree. Compilers do not include dead code in programs, regardless of why 
that code is dead. So there is little practical difference between having 
some sort of contract-only predicate functions and having them generally 
available.

Moreover, I'm very skeptical that having contract-only functions is a good 
idea, especially for preconditions. For a precondition, the caller is 
supposed to ensure that the precondition is true before making the call. How 
can a programmer do this if the predicate is not available to them? For 
instance, it's common to have code like:

    if Is_Open (Log_File) then
        Put_Line (Log_File, ...);
    -- else don't log, file has failed for some reason.
    end if;

where the precondition on Put_Line includes "Is_Open (File)".

If the programmer can't write Is_Open in their code, they cannot avoid the 
failure nor program around it. All they can do is handle the exception, 
which is often the worst way to handle the situation.

Similarly, postconditions often include conditions that hold true after the 
call, and it's quite common for those conditions to feed into following 
preconditions (as in Post => Is_Open(File) after a call to Open). So, as 
much as possible, postconditions should use the same functions that are used 
in preconditions. (The more that's done, the more likely that the compiler 
can completely eliminate the pre- and post- condition checks even when 
they're turned on.)

                                        Randy.