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: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. But that's 
never, ever been true in Ada.

Exactly. You claim that there cannot be such a thing as a dynamically 
enforced contract. But that's simply bogus - Ada has had those since the 
beginning of time - they were called "constraints". Failing one of these 
checks means that your program is wrong. Ada of course defines what happens 
(raising an exception, etc.), but handling those does not make your program 
less wrong. The only reason that these aren't detected statically is the 
difficulty (and impossibility, in some cases) of detecting them statically.

Yes, of course, there are also exceptions raised for reasons outside of a 
contract (that is, those that don't appear in the profile of a subprogram), 
and handling those might make sense in a correct program.

But handling exceptions raised for contracts does not make the program any 
less wrong; indeed, the only legitimate reasons for handling those is to 
make debugging easier [and, in a few applications, to make the application 
"bullet-proof"].

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

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

That's certainly a fallacy in general. Most Ada programs are best off *not* 
handling exceptions caused by outright bugs, because the Ada runtime will do 
a better job of pinpointing the source of the error than any facility you 
could create yourself. Of course, some programs have to be bullet-proof, but 
that is the tiny minority.

In a sense, of course, it's the Ada runtime that's providing the "handling" 
of those bugs (runtime contract failures). And that means a programmer 
doesn't have to, unless they need bulletproof code that is resistent to 
bugs. A lot of programs are *not* in this category. The Janus/Ada compiler, 
for instance, makes no attempt to handle such bugs -- it's much better to 
abandon the compilation attempt immediately rather than producing a program 
based on guessing what was intended.

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

Right. I recall in the past that you've been unwilling to grasp the idea of 
bugs being detected at runtime. Just because Ada defines what happens in 
those cases does not suddenly make it OK to introduce bugs into a program.

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

That's what we're trying to do, and you *obviously* have a problem with 
that. Learning more languages and more tools to do what an Ada compiler 
ought to be able to do is silly.

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

That's not a real problem, because any such program is already wrong (its 
depending on the failure of a dynamic contract). Sure, people can write such 
code, but it's just like overlaying objects using address clauses -- it 
might work, but its still wrong and there is no guarentee that a newer 
compiler version will not break such things.

[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. OTOH, compilers can 
and do remove most of those canonical checks, and letting the contracts be 
enforced against whatever is actually raised by the generated code would be 
much more useful. But it is impractical to specify the checks that have to 
be removed (and not very helpful - it could only be a very small number), so 
what is raised has to be implementation-defined. Which means that just 
because a contract works on one compiler does not mean that it will work on 
another compiler (including a later version of the same compiler). I agree 
with you that runtime detection of exception contract failure makes no 
sense, so the only choices are implementation-defined or non-existent.]

                               Randy.