Re: SPARK Question

[phil.clayton@lineone.net]

On Tuesday, 7 May 2013 21:44:12 UTC+1, Jacob Sparre Andersen news  wrote:
> "Georg Bauhaus" <...@futureapps.de> wrote in message 
> news:...@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 
> >> <...@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.)

Addressing the last paragraph above, the basis of the point is that reusing the same syntactic form of predicate in pre- and postconditions makes it easy for a compiler to spot that a predicate is a consequence of an earlier predicate.  I certainly agree with that!  But surely this would allow only the _subsequent_ occurrences of the predicate to be optimized out?  Above, you seem to suggest that both the initial and subsequent occurrence of a predicate can be optimized out.  In the example above example, it may be possible for the initial occurrence, the postcondition Is_Open(File) of subprogram Open, to be optimized out but that is surely for different reasons - the compiler having special knowledge about the subprogram Open.  In general, for user-defined subprograms, determining statically whether a predicate P(X) holds is, in general, difficult.  Once established, it is straightforward to use the theorem 
  P(X) ⇒ P(X)
to establish that subsequent occurrences of the same form hold.

Separately, even when reusing the same syntactic form of predicate in pre- and postconditions, optimizing out subsequent occurrences of the predicate may not be possible as often as one would hope.  Given two occurrences of the predicate P(X), to establish that the subsequent occurrence holds, it necessary (for the theorem above) to establish that the X is the same in both occurrences.  In the case that X is visible outside its package and between the two occurrences of P(X) there is a call to a subprogram in another package, I can't see how a compiler would know that X won't be changed.  (I'm assuming that compilers don't look at the bodies of other packages when compiling a package.)  To avoid such issues, formal methods tools typically require subprograms to have a 'frame' annotation that indicates which variables a subprogram may change.

So, in summary, optimizing out predicates in pre- and postconditions may not be that easy.

Phil