Re: Silly and stupid post‑condition or not ?

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

On 31.01.12 14:52, Dmitry A. Kazakov wrote:

> Take another example, let you see:
> 
>    x := 1;
> 
> The information about x is incomplete. You know that it could probably
> accommodate the value 1, and that is. You may argue at nausea that this
> "adds value", but that is not Ada, which requires the type of x manifested
> before its use. And what does a type declaration? It lists all possible
> values of x, exhaustively. Again, there are languages that take a different
> path, so my comment is Ada's POV, of course.
> 

OK, I see, even though the claim of Ada's POV is seems
biased, see below. -- I will not presume any kind of formal logic when
watching people judge software systems. We just say words and argue,
referring to other things that seem relevant when discussing software
systems. Words like "LRM" or "Ariane" or "engineering" or "constructivism"
or "deadlines" or "cost" or "DRY", etc.

The program below is also an example of Ada's POV. Alas, it exhibits
the least desirable state of things. It must be Ada's POV,
since the program is legal, is simple, and uses perfectly usual
statements.  Its effect is, however, unpredictable at any level
of precision, because Ada does *not*, by default, require that variables
be initialized. (And no exception propagates out of T_IO if X
happens to be in T'Base, IINM.)  One might say "predictable
with precision" is still true when this label is attached to
some set of all possible effects. But this doesn't sound right.

Anyway, Ada's POV still requires (a) programmers to do
the right thing, and (b) requires us to make good guesses as to
what this right thing might be.  In the program below, it might have
been to see what the bits at X'Address happen to be.

Notice that the declarations list the possible values, exhaustively.

with Ada.Text_IO;

procedure Ada_POV is

   use Ada.Text_IO;

   type T is range 1 .. 10;
   package T_IO is new Integer_IO (T);

   X : T;  -- perfectly legal from Ada's POV
begin
   Put ("X is "); T_IO.Put (X); New_Line;
end Ada_POV;