Re: about the new Ada 2012 pre/post conditions

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net...
> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
>> ...
>>> This is what constitutes the core inconsistency about dynamic
>>> pre-/post-conditions. If they #1 implement behavior (e.g the stack 
>>> contract
>>> to raise something when full), then they cannot be suppressed and do not
>>> describe the contract. If they do describe the contract #2, they may not
>>> implement it and thus shall have no run-time effect.
>>
>> You're right, but I don't see any inconsistency. They are clearly #1, and
>> that includes all of the existing Ada checks as well.
>
> If you take a stance on #1, then checking stack full is no more evaluation
> of the precondition, which does not depend on the stack state anymore, as
> it of course should be. So the "true" precondition is just: True.

Huh? This makes no sense whatsoever.

We can't require static detection of precondition failures any more than we 
can demand static detection of range violations. And Ada *always* has had 
dynamic preconditions:

    procedure New_Line (Spacing : in Positive_Count := 1);

Here, the precondition is "Spacing in Positive_Count". Your contention that 
a dynamic expression cannot be a precondition is the same as saying that no 
parameter can include a range (and thus ought be written as Count'Base 
above).

...
> And implementations leaking into declarations is certainly a very bad 
> idea.

This is NOT implementation; it's part of the contract. For the vast majority 
of subprograms, callers aren't supposed to call routines such that an 
exception is raised; it represents a bug. The only question is to whether 
those conditions are expressed in executable terms or in comments.

For instance, the containers have operations like:

procedure Insert_Space (Container : in out Vector;
                        Before    : in     Extended_Index;
                        Count     : in     Count_Type := 1);

If Before is not in the range First_Index (Container) .. Last_Index 
(Container) + 1, then Constraint_Error is propagated. If Count is 0, then 
Insert_Space does nothing. Otherwise, it computes the new length NL as the 
sum of the current length and Count; if the value of Last appropriate for 
length NL would be greater than Index_Type'Last, then Constraint_Error is 
propagated. {more text here}

It would have much better if this was written as:
procedure Insert_Space (Container : in out Vector;
                        Before    : in     Extended_Index;
                        Count     : in     Count_Type := 1)
    with Pre => (if Before not in First_Index (Container) .. Last_Index 
(Container) + 1 or else
                           Container.Length  > Index_Type'Last - Count then 
raise Constraint_Error);

The latter is less likely to be misinterpreted, it still can be checked at 
run-time, the compiler can use it to completely eliminate redundant checks 
(which cannot be done for checks in the body absent of inlining -- which is 
usually a bad idea), and static analysis tools (and compilers, for that 
matter) can detect and complain about cases where the checks are known to 
fail (that is, where the program has bugs). And you get all of this without 
peeking into the body of the subprogram.
We can't require the latter: it's beyond the state of the art to do that in 
most cases, but by doing this at runtime now, we get people writing these 
conditions so that as the state of the art improves more can be done for 
static detection. There never will be any static detection of conditions 
written as comments!

Also note that in the above, this precondition is NOT part of the body 
(implementation) of the subprogram. This is required of all 
implementations -- it's part of the contract, not the part that varies 
between implementations. As such, it makes the most sense to write it as 
part of the contract.

...
> Neither #1 nor #2 is defendable.

Nothing you say on this topic makes any sense, at least from an Ada 
perspective. Here you are saying that Ada's entire design and reason for 
existing is "not defendable" (that's the separation of specification from 
implementation). How your ideal language might work is irrelevevant in this 
forum. Please talk about Ada, not impossible theory.

                                         Randy.