Re: Silly and stupid post-condition or not ?

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 02.02.12 10:40, Stephen Leake wrote:

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

First, there is no completeness in most real program systems
product; it seems honest, then, to not assume we could manage
to even potentially achieve it is Post aspects, IMHO.
Yet, program system products use formal language.  The use
of formal language means best effort, not completeness of
all kinds, I think.

Post aspects can help being productive:

If programmers know something about the possible outcomes
of a subprogram, they can act accordingly. If there is a
specification that says: the result is such that if P1(Result)
then also P2(Result), they can act accordingly.

A postcondition gives programmers something to work with.
Since natural language does not change the correspondence of
postcondition and programmers writing based on assumptions
about the postcondition, formal language addressing some
results still produce an informed state of mind, a better
one, I think.

As another example,

   type Match (Found: Boolean) is record
      case Found is
          when True =>
             Value : Big_Natural;
          when False =>
             null;
      end case;
   end record;

   procedure Goldbach (A, B: Big_Natural; Result: Match)
     with Post =>
     (if A + B < Highest_Known_Sum then
       (if Result.Found then
               Is_Prime (A)
           and Is_Prime (B)
           and Result.Value mod 2 = 0)
     else  -- larger
       (if Result.Found then
	 Result.Value mod 2 = 0));

Post says that whenever there is a result and it is larger
than some state-of-the-art value, go look and see whether
A and B are prime. If not Result.Found, then data would be thrown
away in any case. Thus, precisely because there is some
kind of formal incompleteness here, the Post aspect tells
something about the results that will not get thrown away.