Re: Silly and stupid post-condition or not ?

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

"Stephen Leake" <stephen_leake@stephe-leake.org> wrote in message 
news:82ty36urik.fsf@stephe-leake.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
...
>> My philosophy is that it is always preferable to at least be able to tell
>> the compiler what you (the programmer) knows about a program entity.
>
> The compiler knows the body; why is the post condition better than that?

No, the compiler does *not* know the body (in general). Ada separates 
specifications and bodies after all. The specification can be compiled long 
before the body is created, and calls written and compiled against that 
specification.

A large part of the problem that I see with proof tools is that they often 
require peeking into the body to verify calls. This is just plain wrong, 
because it means that the proof has to be redone if the body changes. And it 
also means that the body has to exist (and in a near-final form) before the 
proof can be valuable.

An Ada compiler knows even less; when it generates a call it probably knows 
nothing about the body. (Janus/Ada was designed so that the compiler 
literally knows nothing about the body, and cannot get access to any 
information about the body even if it wanted to [other than the one being 
compiled, of course]. That's why Janus/Ada doesn't do any inlining [at 
compile time], as that requires breaking that absolute separation of 
specifications and bodies.) And an Ada compiler cannot presume to know 
anything about the body when compiling a call (as noted, the body may not 
have been written yet).

The postcondition (and precondition) moves this "contract" information to 
where it belongs (on the specification). That allows the compiler to take 
advantage of that information, and in many cases completely eliminate the 
associated checks (just like the compiler can eliminate a large proportion 
of constraint checks). Like constraint checks, well-written contracts should 
never need to be turned off (as always, it's like taking off the seatbelts 
when you leave the garage...).

                                              Randy.