Re: about the new Ada 2012 pre/post conditions

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

On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:

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

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

No. He cannot decide them to implement the contract. That he actually can,
per allowing dynamic checks, is a language design bug.

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

=> It is OK to violate a "contract" defined by these. Here you are.

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

Yes, but irrelevant. These checks are not contract checks, because,
otherwise you are in contradiction. No words can change that.

But also there are important consequences for software engineering. Since
these checks have nothing to do with contracts, they must be considered as
a part of the program semantics and all possible outcomes must be
*handled*. The problem of buffer overflow is exactly in pretending that it
cannot overflow. So the program is broken when it does.
 
> 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.

Terminology is secondary to the semantics. The problem is with the meaning.

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

You don't need to prove every possible aspect of the program. The language
should allow the programmer to choose. Ada 83 had provable contracts stated
in terms of types. Nothing prevents us from having more detailed contracts
as well as other program correctness stuff. I simply don't understand where
is a problem with that.

> Instead of getting the benefits of building in Ada now, 
> and getting more and more static checks as compilers improve.

I don't see tracking down exceptions as a benefit. Neither would it be a
for the maintainer to discover that the program suddenly became illegal
because static checks has been "improved."

I prefer to rely on things known to work now. These I use and hope that
they will continue to work in the future.

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