Re: Assertions in the Next Ada Standard

["Nick Roberts" <nickroberts@adaos.worldonline.co.uk>]

"Dale Stanbrough" <dstanbro@bigpond.net.au> wrote in message
news:dstanbro-07F79B.20222311012002@mec2.bigpond.net.au...

> 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.
> >
> > So, who is working on the proposal for this?
> >
> > Richard Riehle
>
> I think another valuable one would be "assume" which is an
> assertion that allows the compiler to invoke any code
> optimisation it can.


A counter-argument to the addition of any of these facilities being added
can be illustrated in the following procedure:


   subtype Must_Be_True is Boolean range True..True;


   procedure P (...) is
      ...
      [invar.]: constant ... := [i. expr.]; --D
      [a. name]: constant Must_Be_True := [assumption]; --D
   begin
      if [debug] and then not [pre-conditions] then raise [excep.]; end
if; --D
      ...
      if [debug] and then not [post-conditions] then raise [excep.]; end
if; --D
      if [debug] and then not [invar.] /= [i. expr.] then raise [excep.];
end if; --D
   end P;


This procedure demonstrates how pre-conditions, post-conditions, invariants,
and assumptions can all be programmed in existing Ada. For efficiency,
certain assumptions may be made of the compiler, in terms of static
evaluation and/or dead code removal (but these would effectively be required
for the efficient implementation of the proposed pragmas).

A procedure such as P could be made a 'wrapper' to another Q (which does the
real work). P could then be replaced by Q when debugging is completed.
Alternatively, a simple text modification tool could be used to remove all
lines containing "--D".

It may seem like an extreme form of Blimpism to argue against the suggested
pragmas, but I have found in real code that I often wanted to code quite com
plicated test routines into subprograms for debugging purposes. I can't
believe I'm the only one who has found this. The proposed pragmas would be
of little advantage in these cases (they can only take an expression).

Sometimes, what sounds like a great idea turns out not to be so brilliant
when you closely look at it. And sometimes, it turns out that a bigger idea
subsumes it anyway. (Read on... ;-)

One little thing that (I think there is wide agreement on) would be most
welcome would be a 'raise ... when ...;' statement:


   procedure P (...) is
      ...
      [invar.]: constant ... := [i. expr.]; --D
      [a. name]: constant Must_Be_True := [assumption]; --D
   begin
      raise [excep.] when [debug] and then not [pre-conditions]; --D
      ...
      raise [excep.] when [debug] and then not [post-conditions]; --D
      raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; --D
   end P;


However, a major new feature that I would like to see introduced at the next
revision would be a provision for 'separation of concerns'. As a 'straw
man', this might work something like as follows.

Each declarative item which is or can contain a subprogram requires a
completion in Ada 95. In the case of a subprogram, the completion (the body)
is permitted to be the declaration also. My proposed facility would permit
multiple completions for a subprogram (separately declared). The facility
would always apply to a library unit: if the unit is a package, all the
subprograms in the package would be permitted multiple completions.

For example, the declaration of a library procedure P might be declared:


   procedure P ([parameters]);


A new kind of library-level declaration would allow a set of different
'aspects' to be declared, together with a pattern for the way in which they
are applied to subprograms. E.g.:


   procedure P ([parameters]) is separate (Debugging.Before, Main_Function,
Debugging.After);


This declares that P has three separate completions, named Debugging.Before,
Main_Function, Debugging.After. There is also a fourth optional completion,
Debugging, which is a kind of 'parent' to Debugging.Before and
Debugging.After. Whenever P is called, all three declared completions will
be called, in the order declared. The fourth completion, Debugging, will
also be called, before those for Debugging.Before and Debugging.After. The
completions would look similar to current Ada subunits:


   separate (Main_Function)
   procedure P ([parameters]) is
      ...
   begin
      ...
   end P;


A completion for Debugging allows for shared declarations, and an
initialisation:


   separate (Debugging)
   procedure P ([parameters]) is
      [invar.]: constant ... := [i. expr.];
      [a. name]: constant Must_Be_True := [assumption];
   begin
      null;
   end P;


This body will be executed before those for Debugging.Before and
Debugging.After (to provide a set of common declarations for them, and
possibly an initialisation).

Finally, we must separately complete the final two outstanding bodies:



   separate (Debugging.Before)
   procedure P ([parameters]) is
   begin
      raise [excep.] when [debug] and then not [pre-conditions];
   end P;


   separate (Debugging.After)
   procedure P ([parameters]) is
   begin
      raise [excep.] when [debug] and then not [post-conditions];
      raise [excep.] when [debug] and then not [invar.] /= [i. expr.];
   end P;


Things get a little more complex with packages. Here we define a pattern
that applies to all the subprograms the package contains implicitly. E.g.:


   package My_Stuff.Utilities is
      procedure P (...);
      procedure Q (...);
      ...
   end;


   package My_Stuff.Utilities is separate (Debugging.Before, Main_Function,
Debugging.After);


There are now three bodies required to fully complete this package, one for
each of the three aspects. I have also chosen to make the package a child,
to illustrate naming within hierarchies. Within each of the package bodies,
the completions of the given aspect of each of the package's subprograms
must be given. E.g.:


   separate (Main_Function)
   package My_Stuff.Utilities body is

      procedure P (...) is
         ...
      begin
         ... -- implementation of P's main functionality
      end;

      procedure Q (...) is separate;

   end;


I have made the completion of Q a normal subunit, to illustrate the naming
scheme:


   separate (My_Stuff.Utilities.Main_Function)
   procedure Q (...) is
      ...
   end Q;


There would then be:


   separate (Debugging)
   package My_Stuff.Utilities is
      -- any declarations common to Debugging.Before and Debugging.After
   begin
      -- any initialisation code
   end;


   separate (Debugging.Before)
   package My_Stuff.Utilities is

      procedure P (...) is
      begin
         raise [excep.] when [debug] and then not [pre-conditions];
      end P;

      procedure Q (...) is null;

   end;


   separate (Debugging.After)
   package My_Stuff.Utilities is

      procedure P (...) is
      begin
         raise [excep.] when [debug] and then not [post-conditions];
         raise [excep.] when [debug] and then not [invar.] /= [i. expr.];
      end P;

      procedure Q (...) is null;

   end;


I have invented a new form of null procedure, which would probably be handy.
(A bit analogous to the new form of null record declaration for types.)

Finally, each completion would be permitted to be a completion by renaming,
as normal. In many cases, this would greatly facilitate code re-use (if the
design is good).


Obviously there are a lot of details to fill in on this one. But hopefully
it can be seen how it solves the problem of the separation of debugging
code, as well as helping to solve the problems of code separation in a much
wider way.

--
Best wishes,
Nick Roberts