A split between two kinds of Ada programmers?

A split between two kinds of Ada programmers?

[Georg Bauhaus]

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.

Re: A split between two kinds of Ada programmers?

[yannick.moy]

Hi Georg, I implemented the -gnatw.t warning and the above patch, so I can tell you what our objective is.

On Thursday, March 15, 2012 3:07:30 PM UTC+1, Georg Bauhaus wrote:

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

The compiler is there to help honest programmers, not to defeat malicious ones. If you want to guard against misuse of any feature in Ada, best use a coding standard checker such as GNATcheck. Here you could have a rule that no precondition or postcondition is the static literal "True" or "False".

Note that GNAT still warns about statically true or false preconditions and postconditions, for example if you write it "My_True_Constant" or "1 > 0".

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

For this and other uses, it is not helpful that the compiler warns about 
   Pre => True
or 
   Post => False
hence the modification of -gnatw.t that you saw.

Re: A split between two kinds of Ada programmers?

[Georg Bauhaus]

On 16.03.12 16:42, yannick.moy wrote:
> Hi Georg, I implemented the -gnatw.t warning and the above patch, so I can tell you what our objective is.
> 
> On Thursday, March 15, 2012 3:07:30 PM UTC+1, Georg Bauhaus wrote:
> 
>> Can a project use -gnatw.t when integrating source text written
>> by both kinds of programmers?
> 
> The compiler is there to help honest programmers, not to defeat malicious ones. 

o.K.

> Note that GNAT still warns about statically true or false preconditions and postconditions, for example if you write it "My_True_Constant" or "1 > 0".

O.K., I see that a tool like GNATcheck might perform the task as needed;
I was wondering if there could (or should) be some way of saying

 "really, nothing worthy of a condition has happened"

in words that are less overloaded than a mere True, such as a name or
expression that kind of "honestly" silences the compiler.

Thanks for taking the time to explain!