Re: Ada 200X Assertions

[rod@praxis-cs.co.uk (Rod Chapman)]

Richard Riehle <richard@adaworks.com> wrote in message news:<3C0EEC25.E2738366@adaworks.com>...

> It sounds as if Dr. Lamm is
> taking on the job of seeking solutions for DBC within Ada.   Kudos to him.

I hope any such effort starts with a good look at how SPARK works,
where support for DBC is very strong.  Even without explicit pre-
or post-conditions, a simple subprogram declaration in SPARK carries
a far more onerous contract than the same piece of text in Ada.

One critical issue is visibility - most non-trivial assertions involve
states which aren't visible according to Ada's rules, so we have
to have the "--# global" annotation to extend visibilty of state
in annotation context.  The design of a useful assertion mechanism
in Ada0Y or later would have to consider this need carefully.
 - Rod