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:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net...
> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
>> ...
>>>> Legality has nothing to do with preconditions or postconditions.
>>>
>>> => It is OK to violate a "contract" defined by these. Here you are.
>>
>> No, it's not OK; that is the crux of our disagreement. You seem to think
>> that the only kind of "contract" is some sort of static thing.
>
> Exactly. Because the contract exists *before* any programs implementing it
> and after them. The contract exists even when there is no such program.
> Therefore it cannot depend on the program state.
>
> Another way to understand this: a contract describes states of a program.
> As such it cannot depend on them.

That's not my meaning of "contract". It doesn't have anything specific with 
"program states" (whatever the heck you mean by that -- I can't assume any 
reasonable interpretation because you make up terminology all the time).

> Yet another way: the language of contracts is not the object language:

We're not interested in other languages here (this is an Ada forum, after 
all); Ada is the *only* language worth talking about. So by your definition, 
nothing you are talking about is even relevant. Why do you bother? (Why do 
*I* bother? ;-)

...
>> But that's never, ever been true in Ada.
>
> I already said that type constraints are not contracts. E.g. an actual
> value of the discriminant does not create a new contract. The contract
> covers *all* possible values of the discriminant.
>
>> Exactly. You claim that there cannot be such a thing as a dynamically
>> enforced contract.
>
> Absolutely. How could you enforce a contract which has been *already*
> violated? If a program reaches an illegal state, it is in that state.
> Period.

Illegal /= Wrong. An illegal state cannot be reached because you can't 
compile the program. An incorrect state can be reached simply by violating a 
check or contract.

>> But handling exceptions raised for contracts does not make the program 
>> any
>> less wrong;
>
> Really? What is the purpose of the exercise? Raising exception, rolling 
> the
> stack, finalizing stuff, and so on only to resign that the program is as
> wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))

Practicality -- it's not possible to find all program errors before a 
program is fielded. And a lot of programs cannot fail - so that they have to 
have a failback position even when they self-detect that they are internally 
incorrect. It doesn't make the program any less wrong, but it keeps the 
system up so the plane still can land or you can still retrive files for 
www.ada-auth.org.

But if you *could* have detected the "wrong" program earlier, you surely 
would have wanted to, so you could have eliminated the incorrect state.

A whole lot about programming language design is about practicality and not 
about ivory tower exercises. Languages which are purely ivory tower 
exercises rarely have been used off of a college campus.

>>>> 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.
>>
>> Certainly not if you insist on using an unnecessarily limiting definition 
>> of
>> "contract".
>
> Yes, the contract as opposed to the implementation limits the former not 
> to
> be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
> 2012 "contracts" are implementations [POV #1]. Do you?

No, because I use a very different definition of these terms.

Contract is roughly equivalent to (Ada) specification. Implementation is 
roughly equivalent to (Ada) body.

No caller should *ever* depend in any way on "implementation". (Ada screws 
this up for exceptions and tasking behaviors like blocking and abort.) The 
only things a caller can depend upon is that which is given in the 
specification. And that includes both dynamic and static parts.

Tools which depend in any way on the contents of Ada bodies (other than the 
one they are processing) are limiting and violate the philosophy of Ada. 
Thus we have to get more machine-processable information into the Ada 
specification, so tools can process calls without having to violate 
separation by looking at the implementation (that is, the body).

...
> The actual fallacy is in pretending that a bug can be handled. You can
> handle/be in only anticipated states.

Really? That's certainly not true of my web server or many other programs.

   exception
        when Err:others =>
              Log_Error (Err);
              Reset_to_Known_Good_State;

The above is that the bottom of most of my tasks. I have no idea what state 
the task is in when it gets to this handler; it certainly represents an 
"unanticipated state" in that any state that I actually anticipated has its 
own handlers and recovery mechanisms. But this handler works to recover the 
processing in 99% of the cases (good enough for this application); whatever 
caused the problem is abandoned, and it resets to handle another command.

I suppose you'll twist the terminology around in some bizarre way to claim 
that an unanticipated state - which is the only way to reach this handler - 
is somehow anticipated simply because I can write a handler for it. That's 
of course nonsense - whatever I (or any other programmer) thought of is what 
I anticipated, and there is no way for an outside observer to know anything 
about those. So you cannot reason about those in any useful way - it's an 
irrelevant qualifier.

>> Right. I recall in the past that you've been unwilling to grasp the idea 
>> of
>> bugs being detected at runtime.
>
> Sure, because that is rubbish, and always was:
>
> http://en.wikipedia.org/wiki/Liar_paradox

I don't get it. Just because you cannot detect *all* bugs -- that is, that 
you can't ever make a statement that a program is bug-free -- does not mean 
that you cannot detect *some* bugs. Indeed, this misguided focus on 
absolutes has prevented most practical progress in this area. And you're 
trying hard to prevent progress as well.

I'm obviously wasting my time discussing this with you, so I'm done. (If I 
can resist, I'm surely going to try.)

                                  Randy.

...
>> [As an aside, this means you do not want real exception contracts, since
>> they cannot usefully be done without having it be implementation-defined
>> when an exception is raised by a predefined check. The canonical 
>> semantics
>> of Ada would require assuming that every line raises Storage_Error,
>> Program_Error, and usually Constraint_Error -- that would make it 
>> virtually
>> impossible to eliminate those exceptions from contracts.
>
> I don't see it as a big problem. There is a difference between an
> obligation to raise exception and a possibility that an exception could be
> raised.

No one cares about an "obligation to raise an exception"; I can't imagine 
including those in exception contracts. (Indeed, any such "obligations" 
should be in the precondition or subtype predicates, so they never even 
reach the body of the subprogram.)

The only contracts of interest are the "possibility that an exception could 
be raised", as those probably depend on outside effects (user input, file 
system results, etc.)

...
> The vendors could gradually reduce the number of cases where E may be
> raised without making clients relying on weaker contracts illegal. The
> second cannot be misused to prove that E is raised. It just does not 
> follow
> from the second, and conversely.

I don't see this at all. Once you call a routine that has a contract that 
says "E might be raised", you have to include "E might be raised" in your 
contract as well. This "poisoning" is the major objection to exception 
contracts in practice.

Moreover, if you have a language-defined check that raises E in a subprogram 
S, then you have to include the "E might be raised" contract if you have any 
exception contract at all. That's where the legality comes in. If you allow 
that contract to be omitted if the compiler can prove that the 
language-defined check will not fail (and this is common), then you have an 
implementation-defined legality check. If you *don't* allow that contract to 
be omitted, then you will have to include such a host of "E might be raised" 
contracts on every subprogram that no one would ever use the feature. (There 
are at least 8 common exceptions that could occur in large chunks of my 
code; and almost no code could be without Constraint_Error, Program_Error, 
and Storage_Error.)

I'm pretty certain that the only useful exception contract would have to 
allow check elimination to affect legality -- and that's definitely a 
problem for some. (And they might even be right.) But my feeling is that it 
would be very valuable to specify that a routine does *not* raise 
Constraint_Error, and have the compiler verify (or refute) that fact.

                                                Randy.