Re: Assertions in the Next Ada Standard

[Wes Groleau <wesgroleau@spamcop.net>]

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

The "ensure" works, but not the "invariants."  Neither of those
declarations prevents an assignment to X or Y.

I never saw the official proposal (if there was one) but
I'd think it should be inside a subprogram:

pragma Require   ( condition );
pragma Invariant ( condition );
pragma Ensure    ( condition );

or after a subprogram declaration:

pragma Require   ( subprogram, condition );
pragma Invariant ( subprogram, condition );
pragma Ensure    ( subprogram, condition );

Rules of scope could be based on those of Eiffel, unless Eiffel
experience has shown a need for modification.

Since they're pragmas, any vendor could try them out without
affecting validation.

-- 
Wes Groleau
http://freepages.rootsweb.com/~wgroleau