From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,cd5c71f09395807a
X-Google-Attributes: gid103376,public
From: bobduff@world.std.com (Robert A Duff)
Subject: Re: Assertions in Ada
Date: 1997/08/31
Message-ID: <EFsnL6.BpC@world.std.com>#1/1
X-Deja-AN: 269222329
References: <EFBI6M.F2K.0.-s@inmet.camb.inmet.com>
 <199708251351.PAA13197@basement.replay.com> <dewar.872559855@merv>
 <34036C83.4AA6@ist.flinders.edu.au>
Organization: The World Public Access UNIX, Brookline, MA
Newsgroups: comp.lang.ada
Date: 1997-08-31T00:00:00+00:00
List-Id: <comp.lang.ada>


(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