"Georg Bauhaus" 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 >> 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.