Re: about the new Ada 2012 pre/post conditions

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

(Note: I haven't yet read anyone else's response to this thread; but I 
thought I owed Dmitry a response. If this ground was previously covered, 
please feel free to ignore my response.)

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net...
> 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.

It can't be "wrong", because the programmer of an abstraction decides what 
the preconditions and postconditions are.

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

Legality has nothing to do with preconditions or postconditions. 
Preconditions and postconditions are two sides of the same coin. They're 
checks made on the way into and the way out of a subprogram. There is 
absolutely no justification for saying that these are different in some way. 
You are saying that only a postcondition can have dynamic components, which 
is nonsense.

You seem to want to associate the actions of the precondition with the 
subprogram itself, but that is also wrong. Preconditions are checked 
*before* a subprogram is called, so those actions occur *before* anything in 
the subprogram (and thus anything in the postcondition to the subprogram).

You're trying to fit all exceptions into a single box, which is silly. Some 
exceptions are clearly part of the preconditions of the subprogram -- the 
only reason that they are exceptions is because it is currently beyond the 
state of the art to check these statically. Any occurrence of these 
exceptions in a program represents a bug; they should never happen in a 
correct program. For instance, the mode check for a file.

OTOH, some exceptions are reporting issues that only are detectable *after* 
the subprogram has been called (for example, the Use_Error caused when a 
disk is full). Those should be in the exception contract (not the 
postcondition; that's only for "normal" return; the exception contract might 
have a separate postcondition for each exceptional return).

Deciding between these is something that only the designer of a subprogram 
can do. No mathematical theory can ever do that.

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

The only kind of correctness checks that *can* exist in general are dynamic. 
Ada's entire reason to exist is to include checks like range checks and 
overflow checks to programs. Without them you get the buffer overflows and 
other errors that plague C code.

Compile-time detection of bugs is only possible in very limited and not very 
useful cases. Limiting a programming language to those cases only makes it 
unusable (exhibit #1 - SPARK).

I suppose you have a totally different definition of "correctness checks" 
than I do; as usual, we can't have a useful discussion because you have your 
own set of terminology.

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

We're not interested in "proving program correctness". That's (still) beyond 
the state of the art for any realistic programming language. We *are* 
interested in dynamic features that can provide information to future static 
analysis tools. But realistic analysis tools will never (and should never) 
try for "complete" analysis.

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

SPARK is next to useless for real programs - at best it can be used only to 
prove small parts of a program, and it takes a lot of effort to get there. 
It's the sort of thing that turns programmers off (it *certainly* has done 
that to me!) and essentially pushes them to stick with the unsafe languages 
that they are using. Instead of getting the benefits of building in Ada now, 
and getting more and more static checks as compilers improve.

This idea of "perfect" proving has essentially prevented these techniques 
from moving into the mainstream, and it is sad that this is the case.

Anyway, if you are going to push "program proving", then we literally have 
nothing to talk about. So this conversation is done.

                                          Randy.