Re: Assertions in Ada

[bobduff@world.std.com (Robert A Duff)]

(e-mailed and posted)

In article <34036C83.4AA6@ist.flinders.edu.au>,
Adrian P. Morgan <apmorgan@ist.flinders.edu.au> wrote:
>As an alternative to using a pragma as an assertion mechanism, would it
>be possible to add new attributes to subprograms such as 'Precondition?

Maybe, but it seems tricky.  Preconditions normally reference the
subprogram's parameters, but those parameters aren't normally visible in
a following attribute_definition_clause.  So you'd have to have special
visibility rules.  Also, how would you do Eiffel's "old" feature, where
you can have a post-condition that asserts something like "X = old X + 1"?

>Then we could say,
>
>for P'Precondition use Boolean_Expression;
>for P'Postcondition use Boolean_Expression;

And something like "for My_Type'Invariant use ..."?  Or should
invariants be attached to packages?  Or both?  IMHO Eiffel's invariants
are more important than pre- and post- conditions, because you can
simulate pre- and post- conditions with much less pain.

>for P'Time_Constraint use 3.0; -- alternative to select then abort

Putting timing constraints in assertions seems to open a can of worms.

- Bob