Re: Silly and stupid post-condition or not ?

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

On Fri, 3 Feb 2012 21:16:34 -0600, Randy Brukardt wrote:

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

Sure, but this is a fault of your (read: ARG) approach.

Look, you are trying to describe the semantics of a program written in the 
language (Ada expression) in the same language (Ada expression), though in 
the form of "pre-"/"post-" conditions. That would not work. No need to even 
try! Isn't it obvious, that there is no value added? It is the same 
language of same power. Why do you expect it work any better by merely 
moving code from bodies to the declarations?

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

Absolutely. But that does not imply that a dynamic check could magically 
make unusable usable.

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

No, I am very unhappy when the original appearance of a bug is modified by 
some middleman (e.g. exception propagation).

That is assuming absence of false positives. But as we learned from the 
history accessibility checks, false positives are very likely to happen. 
When highly qualified Ada designers failed to design a check properly, what 
to expect from a layman programmer adding fancy pre-/postconditions in his 
program?

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

No, if that description is incomplete;
No, if that is a dynamic check, rather than a description;
No, if the remaining part cannot be implemented because of the choice made;
No, if the easy part is unimportant to the goal at hand.

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