A split between two kinds of Ada programmers?

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

THURSDAY MARCH 8, 2012

[GNAT] Improve warnings from -gnatw.t �

"When a postcondition is explicitly True or False, it is reasonable
 to assume that this is exactly what is intended, and it is now the
 case that warnings for such postconditions are suppressed."

(From GNAT Development Log)


The message, IMHO, suggests that there are programmers dearly wishing
to express, in (pre and) post conditions, what they know about their
types. For example, when they know a subprogram needs no special
preconditions, that it will compute a state such that Post => ... , no
matter what, they say Pre => True. And Post => True as well, because
they may have reason to not say more about objects from the
subprogram's profile, or about objects in some outer scope. The
subprogram may just not affect any of these objects, and, therefore,
writing Post => True is reasonable. (If somewhat void, and implicit,
in the light of the explicitly listed reasons?)

Call them, in pompous terms mabye, the "open", "honest" programmers.

Other programmers might consider checked conditions not only a
debugging aid(*), but also a tool that allows superiors to oversee the
programmers. Why? Because a failed post condition is evidence of an
mistake.  "This programmer's mistake because he wrote the subprogram!"
Whatever the technical truth is, the statement's is superior.
How will the programmers react? Will they not resort to always writing
Post => True, say, knowing that doing so will make their subprograms
look better when assertion policy is Check?

Call them the "secretive", "self-protective" programmers.


The question then becomes:

Can a project use -gnatw.t when integrating source text written
by both kinds of programmers?


Some data points:

I have seen exceptions "explicitly" suppressed by programmers, but
sometimes for a reason. They had written empty handlers, no logging.
This was partly justified, since, in some cases, the customer would
predictably refuse to pay for work that obviously could raise an
exception, even in drafted software. So make silent errors a policy.

Remembering Eiffel, it seemed somewhat common to just say the
equivalent of Post => True when one wanted to defer thinking about
what the post condition should really be.

__
(*) which, according to J.-P. Rosen's introduction, it very well is,
besides functioning as a lemma, and also as part of a contractual
obligation.