Assertions in Ada

Assertions in Ada

[AdaWorks]

Subject: Assertions in Ada
Newsgroups: comp.lang.ada
Organization: Netcom On-Line Services
Summary: 
Keywords: 

Subject: Assertions in Ada
Newsgroups: comp.lang.ada
Organization: Netcom On-Line Services
Summary: 
Keywords: 

I have found the thread on Eiffel versus Ada quite interesting. For a
long time I have believed that Ada should include some form of assertion
mechanism.  I favor the Eiffel words: require, ensure, and invariant.

These could be pragmas in the general form,

    pragma Require(Entity, Data-type, Boolean-Expression)

which would add no new syntax to the language.  Or they could be in
the form of a child package to Ada.Exceptions, also adding no new
syntax to the language.  

In other words, Ada may not need to be redesigned to introduce assertions.
Existing language features might work just fine.  Much of the argument
in favor of Eiffel would simply vanish with the addition of a reliable
assertion mechanism in Ada.

Richard Riehle

-- 

richard@adaworks.com
AdaWorks Software Engineering
Suite 30
2555 Park Boulevard
Palo Alto, CA 94306
(415) 328-1815
FAX  328-1112

Re: Assertions in Ada

[Tucker Taft]

AdaWorks (adaworks@netcom.com) wrote:

: ...
: These could be pragmas in the general form,

:     pragma Require(Entity, Data-type, Boolean-Expression)

I'm not sure what the "Entity" and "Data-type" arguments signify,
but the basic ability to introduce an assertion is supported
in the Ada 95 compilers from GNAT, Aonix, Green Hills, and
Intermetrics (and perhaps others) via:

    pragma Assert(<boolean_expression> [, <string>]);

I would hope that most other Ada 95 vendors now or would
soon support this as well.

This can accomplish many of the same goals as the Eiffel mechanisms,
though it is not associated with a type/class, but rather with a 
particular point in the execution (which is undeniably less powerful).  
A pragma Assert does not support the ability to specify a loop "variant," 
at least not without the programmer adding some extra variables.

Note that during the 9X design we did consider adding more complete
assertion/invariant constructs, but dropped them in the desire to
reduce the overall scope of the revision.

The Eiffel mechanisms are certainly interesting, though I 
believe the class-oriented assertions are in fact a bit 
limiting, in that one must write only assertions that all
subclasses can satisfy.  There is less support for writing assertions
that apply only to a class, but not to its subclasses.  Such 
class-specific assertions make good sense and can help in debugging 
and proving correctness of a particular class, even though they do 
not apply to subclasses.

My biggest complaint about Eiffel (and Java, for that matter), however, 
is that they don't physically separate interface from implementation (except 
via the notion of "deferred" classes).  The normal response is that
you can use a tool to "extract" the interface any time you want,
but that seems to break the whole notion of "design by contract."
I would never go to an implementor and ask them "what is today's
contract?"  The contract should be a separate entity (e.g. the
package spec) which does not "belong" to (and is not extracted from)
either the client or the implementation of the abstraction.
The compiler can then check conformance of an implementation against
its contract.  If you bundle the interface with the implementation,
then there is nothing against which the compiler can check conformance.

It is sort of like answering the question "what does it do?" with the
answer "it does what it does."

I realize that assertions can represent a contract, but the
parameter/result profile is also an important kind of contract
(especially when it includes parameter modes, as it does in Ada).
And if assertions are the only form of separate contract, they
are less useful if they cannot be class-specific, but must
always be constructed in a way that they can apply to any
subclass as well.

: ...
: Richard Riehle
: richard@adaworks.com
: AdaWorks Software Engineering

--
-Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
Intermetrics, Inc.  Burlington, MA  USA

Re: Assertions in Ada

[Brian Rogoff]

On Thu, 21 Aug 1997, Tucker Taft wrote:
> Note that during the 9X design we did consider adding more complete
> assertion/invariant constructs, but dropped them in the desire to
> reduce the overall scope of the revision.

This decision seems exactly right to me, though for a different reason. It 
isn't clear to me that there is enough consensus on formal (in the sense of
"mathematically formal") programming methodologies to consider choosing a 
set of constructs to put in the language proper. It makes more sense to 
let people experiment with tools/notations/methods like Anna, Larch, Z, B, 
and others. So IMO, Ada got this right, and Eiffel got it wrong, just like 
Eiffel got modules wrong.

This "Eiffel envy" strikes me as kind of silly, since I don't find Eiffel a 
particularly elegant language.

> My biggest complaint about Eiffel (and Java, for that matter), however, 
> is that they don't physically separate interface from implementation (except 
> via the notion of "deferred" classes).  

Agreed. Separate package spec and body is a nice feature.

-- Brian

Re: Assertions in Ada

[Robert Dewar]

Jon Anthony says

<<b) If a) is the expectation, then why was this pragma left out of the
   standard??  Just hadn't thought of it at the time? (oops that makes
   3)>>


It is one thing to stick this into an implementation, quite another to
formally define what you mean. In particular the whole issue of whether
the compiler can use the assertion involves some tricky business. We
found that different people had very different ideas in mind.

In GNAT (I can't speak for the other vendors)

pragma Assert (X);

is *exactly* equivalent to

  if not X then
     raise System.Assertions.Assert_Failure;
  end if;

This is a simple definition, but it is not at all what some people want. They
argued that the assert statement should not be allowed to affect the program
in any way (this is quite tricky to define exactly, in fact there is more
than one possible definition), but clearly the above equivalence does not
meet this requirement, because the compiler can assume a postcondition of
X after the assert.

We could not resolve this issue, so the feature got omitted. It's always
surprising (especially to those who do not have experience in language
design) how the simplest appearing things can turn out to be very complex.

Re: Assertions in Ada

[Tucker Taft]

Robert Dewar (dewar@merv.cs.nyu.edu) wrote:

: Jon Anthony says

: <<b) If a) is the expectation, then why was this pragma left out of the
:    standard??  Just hadn't thought of it at the time? (oops that makes
:    3)>>


: It is one thing to stick this into an implementation, quite another to
: formally define what you mean. In particular the whole issue of whether
: the compiler can use the assertion involves some tricky business. We
: found that different people had very different ideas in mind.

: ...

: We could not resolve this issue, so the feature got omitted. It's always
: surprising (especially to those who do not have experience in language
: design) how the simplest appearing things can turn out to be very complex.

Other stumbling blocks to including it in the Standard:

   The safety-critical community seemed generally to prefer methods
   based on separate tools that look from the "outside" to
   verify conditions in the code, without adding anything to
   the generated code in the target machine.  Since we had presumed
   the safety-critical community would have been one of the big
   supporters of the pragma, this lack of interest was a big blow.

   One reviewer felt very strongly that a pragma assert in the
   declarative part should be interpreted as a block-wide invariant,
   rather than as a one-time assertion about the state at the
   point of the pragma.  This further broke the consensus on the meaning
   of the pragma, and when you can't get consensus, it is difficult
   to standardize.

Be that as it may, most "every day" programmers very much like
the notion of a pragma Assert, and I expect to see it widely used,
and presumably therefore widely (universally?) supported.

"Assert" is perfect for a pragma in Ada, because if an implementation 
doesn't support it, it simply ignores it, so the program is still fully
portable.

--
-Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
Intermetrics, Inc.  Burlington, MA  USA

Re: Assertions in Ada

[Robert Dewar]

Brian says

<<This decision seems exactly right to me, though for a different reason. It
isn't clear to me that there is enough consensus on formal (in the sense of
"mathematically formal") programming methodologies to consider choosing a
set of constructs to put in the language proper. It makes more sense to
let people experiment with tools/notations/methods like Anna, Larch, Z, B,
and others. So IMO, Ada got this right, and Eiffel got it wrong, just like
Eiffel got modules wrong.>>

I basically agree. I think it useful to have the simple minded Assert
that is provided in GNAT (and several other compilers have copied this,
as Tuck notes). This assert is not some kind of wonderful silver bullet
that will make all Ariane-like problems disappear, but it is a useful
tool, as has been well known by programmers for longer than I can
remember. The GNAT compiler itself for instance is full of assertions,
and they have been invaluable in 

   (a) avoiding silent generation of wrong code, the most heinous
       crime a compiler can commit.

   (b) speeding up the tracking of errors

GNAT is now at the point where it is stable enough that it makes sense
to turn off these assertions for the production version, and we intend
to do this in version 3.11 of GNAT -- our experiments show that (a) is
no longer a significant concern, and we will still keep the assertions
around to help with (b) -- one of the handy things about the pragma
Assert is that it can be externally activated (the -gnata switch in GNAT).

But I agree that putting in anything formal or elaborate would have been
premature. What would be nice to see is people experimenting with possible
interesting annotations, etc with GNAT. 

(by the way, if you want to experiment with the fast version of GNAT, with
assertions off, you can do it yourself, by rebuilding the compiler with
the -gnatn switch on and the -gnata switch omitted :-)

Assertions in Ada

[AdaWorks]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2309 bytes --]



Thanks for the responses to my posting on this subject.  My proposal was intended as the start of a 
dialogue on this subject, not as fodder for comparing the virtues of one progamming language against 
those of another.  I certainly am not calling for immediate action but for recognition that pre-, post, and 
invariant assertions may have a place in designing with Ada.  Except for the gratuitous put-downs,  
�especially to those who do not have experience in language design,�  and �Eiffel envy� the comments 
have been interesting and well-considered.  That said, there is little benefit in any of us comparing Eiffel 
to Ada in this dialogue.

My original note on this subject concerned how the pre-condition, post-condition and invariant 
would benefit Ada.  I probably should have avoided all mention of Eiffel since such mention inevitably
foments language comparisons.  I did say that I like the words �require,�  �ensure,�  and �invariant.�
as they are used in Eiffel.  But that does not imply we should make Ada more like Eiffel.  Instead, it 
means there might be some benefit in further examination of this feature to enhance Ada�s existing 
support for �programming by contract.�

I understand that there would need to be some discussion in the Ada community before we could
come to an agreement on what each assertion means.  The addition of pragma Assert to GNAT is
a good start in the right direction.  

Perhaps this would be a good topic for some kind of Working Group.  

I hesitate to make explicit proposals for the behavior of the pre-, post-, and invariant pragmas in this
posting.  I do have some ideas, of course.  In fact, in a one-on-one discussion with Robert Dewar at 
Ada Europe, he agreed that some of the ideas has merit.  Mostly, I am interested in whether, without
comparing Ada to other languages, Ada could benefit from this feature.  I believe it could.  

I already know there are those with reasons why it cannot work.  Now I would like to see the comments 
from those with reasons why it could.

Richard Riehle
AdaWorks
Suite 30
2555 Park Blvd
Palo Alto, CA  94306
(415) 328-1815
richard@adaworks.com
-- 

richard@adaworks.com
AdaWorks Software Engineering
Suite 30
2555 Park Boulevard
Palo Alto, CA 94306
(415) 328-1815
FAX  328-1112

Re: Assertions in Ada

[Ken Garlington]

Tucker Taft wrote:
> 
> Note that during the 9X design we did consider adding more complete
> assertion/invariant constructs, but dropped them in the desire to
> reduce the overall scope of the revision.

At least in the meetings I attended, there was also a significant
conflict among the attendees as to the goals, syntax, etc. of
such constructs. I never heard any significant coalition that
seemed to agree in any of these areas.

Even now, it appears that pragma Assert has some variations
among vendors (e.g. the example code in my paper, which works
under GNAT, has to have the pragmas moved to work with the
Aonix products).

> My biggest complaint about Eiffel (and Java, for that matter), however,
> is that they don't physically separate interface from implementation (except
> via the notion of "deferred" classes).  The normal response is that
> you can use a tool to "extract" the interface any time you want,
> but that seems to break the whole notion of "design by contract."

I agree, although maybe we're being too Ada-centric about this. It
does seem to complicate matters to have to deal with an extraction,
rather than "the thing" itself.
 
> --
> -Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
> Intermetrics, Inc.  Burlington, MA  USA

Re: Assertions in Ada

[Ken Garlington]

Tucker Taft wrote:
> 
> Other stumbling blocks to including it in the Standard:
> 
>    The safety-critical community seemed generally to prefer methods
>    based on separate tools that look from the "outside" to
>    verify conditions in the code, without adding anything to
>    the generated code in the target machine.  Since we had presumed
>    the safety-critical community would have been one of the big
>    supporters of the pragma, this lack of interest was a big blow.

Yes, I think this definitely represents my feelings at the time.
Although I don't think anyone argued _against_ including assertions,
I know I didn't feel that it was something we desperately needed,
particularly vs. pragma Reviewable, etc. (Obviously, if you've
read my Ariane responses, you know I haven't changed my mind
yet, either!)

> --
> -Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
> Intermetrics, Inc.  Burlington, MA  USA

Re: Assertions in Ada

[Robert Dewar]

<<Even now, it appears that pragma Assert has some variations
among vendors (e.g. the example code in my paper, which works
under GNAT, has to have the pragmas moved to work with the
Aonix products).>>


Yes, Ken pointed out this variation, but this is not a matter of design,
it is more a matter of a bug in GNAT that no one ever noticed before,
namely GNAT allows pragma Assert in a place where it probably does not
intend to. In GNAT a pragma Assert is simply optional executable code,
it is not some kind of abstract specification, and therefore it should
only occur where a statement or declaration can appear.

Re: Assertions in Ada

[Brian Rogoff]

On Sat, 23 Aug 1997, Ken Garlington wrote:
> 
> Yes, I think this definitely represents my feelings at the time.
> Although I don't think anyone argued _against_ including assertions,
> I know I didn't feel that it was something we desperately needed,
> particularly vs. pragma Reviewable, etc. (Obviously, if you've
> read my Ariane responses, you know I haven't changed my mind
> yet, either!)

Are the assertions that you're discussing GNAT style pragmas or the
more complete Eiffel/Sather set? I think the former are OK, and may
become a de-facto standard. While I understand the benefits of the 
latter, I'm still an agnostic about whether they belong in the language 
proper, or whether a more complete specification language is really 
better left as part of a formal development methodology like the 
B method. So for example if B tools generating Ada were available, the
effort of putting a powerful specification tools in the language would
have been wasted. I think the decision to do nothing was wise in more ways
than one. "When in doubt, leave it out".

-- Brian

Re: Assertions in Ada

[Robert Dewar]

Jeff said

<<another post by R. Dewar. The package provides checking even with
compilers that don't support pragma Assert. The advantage of the pragma
is that you can use it in a declarative region, where a procedure call
is not allowed. I considered also providing a function for use in
declarative regions, but didn't, because I expect optimization to
eliminate the unused constants I would declare with the function.>>


The constants could be eliminated, but not their initializing expressions
if they have potential side effects, which the assert call most surely
does, so your fear of being done in by the optimizer here is groundless.

Incidentally, GNAT also provides pragma Debug:

  pragma Debug (procedure-call-statement);

which is a procedure call that can be turned on or off by an external
compiler switch, and which can occur in a declarative region. This
allows more general processing than the assert pragma.

Re: Assertions in Ada

[Adrian P. Morgan]

I'm only a student, so I might be talking utter rubbish, but I find all
this rather interesting so here goes...

As an alternative to using a pragma as an assertion mechanism, would it
be possible to add new attributes to subprograms such as 'Precondition?
Then we could say,

for P'Precondition use Boolean_Expression;
for P'Postcondition use Boolean_Expression;
for P'Time_Constraint use 3.0; -- alternative to select then abort

If only to aid my personal understanding of what assertions are all
about (IIUC they are a mechanism for conditionalising the execution of a
subprogram from within the specification), I would appreciate mailed
comments on the above.

-- 

 _____________________________________________
/ Adrian Morgan <apmorgan@ist.flinders.edu.au>\
===============================================----------------------
| Studies:   2nd year BSc(Computing) at Flinders University in 1997 |
| Residence: Bible College of South Australia residential community |
| Interests: Science, Theology, Programming, SF, Comedy, Music, etc |
| Mail:      Welcome                                                |
---------------------------------------------------------------------

Re: Assertions in Ada

[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