Re: about the new Ada 2012 pre/post conditions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote:

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

You seem to imply that value in the range is a precondition of the
operation constrained to that range. This is wrong. If S is a subtype of T
then the precondition is

   X in T

The postcondition is

   (X in S and <something>) or (X not in S and Constraint_Error propagated)

> And Ada *always* has had dynamic preconditions:
> 
>     procedure New_Line (Spacing : in Positive_Count := 1);

The precondition here is Spacing in Positive_Count'Base because the
behavior of New_Line is *defined* when Spacing is not in
Positive_Count'Range.

   New_Line(0) 

is a *legal* Ada program.

>> And implementations leaking into declarations is certainly a very bad 
>> idea.
> 
> This is NOT implementation; it's part of the contract.

OK, you switched from #1 to #2.

>> 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"

Why entire? Dynamic correctness checks are not defendable, as demonstrated
on numerous examples.

> (that's the separation of specification from implementation).

On the contrary, it is #1 which breaks that separation. #2 it is just flat
wrong.

> How your ideal language might work is irrelevevant in this forum.

It is not mine language. It is a methodology of defining and proving
program correctness as introduced by Dijkstra. It applies to all languages
without exemption.

> Please talk about Ada, not impossible theory.

The only impossible theory here is about meaning of dynamically checked
preconditions, e.g. #1 or #2? That is indeed impossible, because
inconsistent. Otherwise Dijkstra's approach works pretty well with any
language, e.g. SPARK does for Ada.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de