Re: Silly and stupid post-condition or not ?

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net...
...
> You and Randy confuse a generalized semantics with an undefined one. The
> key question is the relation of the variance of the 
> generalized/unspecified
> part to the program's behavior. In your example odd values like 1,3 are 
> not
> used by the program, or at least supposed to be unused. In the OP example,
> Format_Error of unspecified semantics is to be used heavily.

In practice, they're the same thing. It will never be practical to fully 
describe the semantics a real program (like, say, an Ada compiler). Even if 
someone invents a far more descriptive formalism than plain Ada expressions 
to describe such things, it's going to be far too complex to use. 
(Personally, I get confused when people start going beyond basic boolean 
logic; I'd rather people didn't even bother to go beyond that because it's 
worthless to the majority of programmers.)

Beyond that, there is not such thing as "I don't intend to use something". 
Unless the program somehow prevents it, *it* will get used and will happen. 
You will get odd values in the data type that J-P described -- it does not 
matter how they happened. And you will be happy (or at least ought to be) 
that some bugs are detected even if not all.

But to claim that just because it's practically impossible to describe the 
complete behavior of real systems does not mean that there is no benefit to 
describing the easy part. And that is exactly what you are arguing -- and it 
should be clear to any Ada programmer that that is a fallicy.

Similarly, describing *part* of the semantics of a subprogram with a 
postcondition, and part with comments is perfectly valid and possibly 
useful. (That's especially true as checking many of the requirements might 
be too expensive at runtime, and thus they practically have to be omitted 
from the formal postcondition.)

                                          Randy.