Re: Assertions in the Next Ada Standard

[FGD <presbeis@look.ca>]

Richard Riehle wrote:

> I am hoping to see something like pre-conditions, post-conditions,
> and invariants in the next revision of Ada.  I would be pleased if
> we simply adopted the wording already used in Eiffel:  require,
> ensure, and invariant, but I am not intractable about the terminology.

Though I'm not familiar with Eiffel and its use of those idioms, but 
this sounds like an attractive proposal. However, if you allow me to 
play Devil's advocate, could you give a concrete example where this has 
significant benefits.

For suprograms, this doesn't seem essential because of Ada's strong 
typing. It may however be very useful for loops and related constructs. 
But I can find *weak* replacements within Ada. For invariants, enclose 
loops in a block statement, e.g.

     declare
         Const_X : constant Integer := X;
         -- invariant X
         Pos_Y : Positive := Y;
         -- ensure Y > 0
         -- invariant (Y > 0)
     begin
         loop
             ...
         end loop;
     end;

This also allows for catching exceptions locally, or use pragma Suppress 
to allow optimizations. For require and ensure, enclose the loop in an 
inlined procedure similar to the above. These replacements are weak 
because Ada types cannot conveniently represent assertions such as X /= 
0 or X > Y for variable X and Y. Perhaps some type improvements could do 
the job instead?

There is one place where I can see some genuine benefits. It would be 
possible to specify exception conditions in declarative parts, e.g. 
(improvised syntax)

     function "/" (L, R : Integer_Type) return Integer_Type;
     for "/" require R /= 0;

     function "*" (L, R : Matrix) return Matrix;
     for "*" require L.Columns = R.Rows;
     for "*" ensure return.Rows = L.Rows;
     for "*" ensure return.Columns = R.Columns;

Or perhaps type improvements could do the job:

     -- Disconnected ranges?

     subtype Nonzero_Integer_Type is Integer_Type
         range Integer_Type'First .. -1 | 1 .. Integer_Type'Last;

     function "/"
         (L : Integer_Type;
          R : Nonzero_Integer_Type)
         return Integer_Type

     -- Dummy discriminants?

     function "*"
         (L : Matrix(Rows => M, Columns => L);
          R : Matrix(Rows => L, Columns => N))
         return Matrix(Rows => M, Columns => N);

Perhaps I'm missing something, how does Eiffel use these?

-- Frank