Re: Silly and stupid post-condition or not ?

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

"Stephen Leake" <stephen_leake@stephe-leake.org> wrote in message 
news:82k445fu9n.fsf@stephe-leake.org...
...
> I agree with Dmitry; post conditions should be _complete_. If the Ada
> post condition language is not strong enough to be complete, don't use
> it; use natural language comments.

That's a pretty silly position, it essentially says that everything that 
makes Ada great is not worthwhile because it only can detect a portion of 
the problems. If you really believe this, you might as well be programming 
in a dynamically typed language, because then there is essentially no 
benefit to what Ada provides.

For instance, if you have an object

           Dart_Score : Natural range 1 .. 60; -- Holds the score for a 
single dart.

The range 1 .. 60 is not a complete specification of the possible scores. 
(For instance, 58 is not a possible score, but it is allowed by the range.) 
But even so, this specification still catches a lot of errors. Your comment 
above denies this and says that it is better to just have the comment rather 
than the range (because it is not "complete" in some sense).

[Aside: Ada 2012 has a way to make this complete, but of course there are 
many other things that are too hard to describe.]

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. That 
allows the compiler and other tools to make checks (both compile-time and 
run-time) about that information -- and my years of experience shows me that 
those checks catch a lot of bugs (but by no means all). Moreover, as tools 
and compilers get better, they get able to do more with the information they 
are given, so you want to give them as much information as you can now --  
it's a lot harder to retrofit that information in after the fact.

So I want to describe as much as I can in terms of contracts (preconditions, 
postconditions, predicates, constraints, exclusions, and invariants for Ada 
2012, hopefully exception and data contracts in the future), but not to the 
extent of necessarily requiring completeness. At some point it just gets too 
hard.

I've always hated the emphasis on completeness of these things, because it 
is *exactly* the wrong approach to getting something in wide-spread use 
(even in the Ada community). Something like SPARC, that requires an 
all-or-nothing approach, very often ends up with nothing.

OTOH, an approach that just applies the easiest contracts first sets up a 
positive feedback loop for newcomers to Ada. They'll add a few range 
constraints and discover that those have detected some bugs early (possibly 
even at compile time). Which encourages them to add more contracts, which 
discovers more bugs early, and so on. That's how *I* learned the real 
benefits of Ada years ago - and I find it hard to believe that I'm unusual.

I think that things like SPARC can actually be harmful, as they focus 
attention on the wrong things. There is a lot that can be proved about 
dynamic constructs in Ada (far more than in other most languages), and it is 
unfortunate that instead of taking advantage of this (and making widely 
usable results), most of effort has been on proving the Fortran 66 subset of 
Ada. (I do see signs that this is changing, finally, but I think a lot of 
the work should have been done years ago.)

                                                    Randy.