Re: Silly and stupid post-condition or not ?

[Stephen Leake <stephen_leake@stephe-leake.org>]

"Randy Brukardt" <randy@rrsoftware.com> writes:

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

That's pretty silly as well; I use Ada for everything, and have said so
many times here. 

But I'll try to keep an open mind and find something useful to say.

> For instance, if you have an object
>
>            Dart_Score : Natural range 1 .. 60; -- Holds the score for a 
> single dart.

Nothing in this declaration says it's a _valid_ dart_score. But it would
be helpful for the comment to include the notion of invalid scores:

    Dart_Score : Natural range 1 .. 60; 
    -- Holds the score for a single dart. Note that not all scores in
    -- this range are possible on a standard dart board.

So this uses part Ada and part natural language to specify the
actual constraints.

The original post condition was:

   function Parsed (S : String) return Parsed_Type
      with Post =>
        (if S'Length not in Image_Length_Type then
            Parsed'Result.Status = Format_Error);
         -- There may be other failure conditions.

I was ignoring the comment; it's pretty weak. I would improve it:

   function Parsed (S : String) return Parsed_Type
      with Post =>
        (if S'Length not in Image_Length_Type then
            Parsed'Result.Status = Format_Error);
   -- There are other failure conditions indicated by
   -- Parsed'Result.Status = Format_Error.

I still find this less satisfying than in the Dart_Score case. But maybe
that's just because I'm used to range constraints, and not used to post
conditions.

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

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

The post condition also specifies a run-time check; that will catch
bugs. But I don't consider that "telling the compiler something"; I
consider it a way of specifing what checks to perform.

If assertions are enabled, the compiler can assume post conditions are
satisfied after a call (since otherwise an exception will be raised).
That does give the compile information it can act on.

In the particular case of Parsed, the information is not useful after
the function returns, since it is actually a precondition.

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

Ok, as long as there is a comment saying what's left out, when it is
significant (as it is in the Parsed case; less so in the Dart_Score case).

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

That makes sense; I had not considered that aspect.

-- 
-- Stephe