Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Bob Duff <bobduff@theworld.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Wed, 28 Oct 2015 12:06:33 +0100, Georg Bauhaus wrote:
>> However, another use of predicates is to document assumptions.
>
> Documenting *shall* have *no* run-time effects.

Really?!

In C, we can write:

    int num_gizmos = 0; // num_gizmos is always between 0 and 1024.

In Ada, we can write:

    type Gizmo_Count is range 0 .. 2**10;
    Num_Gizmos: Gizmo_Count := 0;

IMHO, documenting the 0..1024 requirement in executable code is much
better than using a comment:

    - It's more likely to be correct, especially if we have a good test
      suite.  The comment just says what the original programmer thought
      was true.  Maybe they were wrong.  More likely, they were right,
      but subsequent changes elsewhere made the comment wrong.

    - If I'm debugging a specific bug, and the run-time checks on
      Num_Gizmos don't fail, I know the problem isn't caused by an
      out-of-bounds value of that variable.  Even if the
      "range 0..2**10" is wrong, it's not the cause of THIS bug.

    - English comments can be ambiguous -- sometimes "between" means
      inclusive of the end points, sometimes exclusive (although we can
      guess "inclusive" in this case).  On the other hand, I know
      exactly what ".." means.

By the way, what exactly do you mean by "shall"?  A native speaker of
English doesn't usually use that word, except in legal documents and the
like.  You seem to use the word "shall" to express opinions about the
way things ought to be, which seems like an odd usage to me.

- Bob