Re: Assertions in the Next Ada Standard

[dewar@gnat.com (Robert Dewar)]

Wes Groleau <wesgroleau@spamcop.net> wrote in message news:<3C3F4D9B.79019B90@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.


Probably more realistically, someone could implement these
in the FSF version of GNAT perhaps. I doubt any vendor is
likely to do work in this area, I certainly have not seen
any significant interest from any of our supported users
in such a feature.

Robert Dewar
Ada Core Technologies