AdaYY; Assertions?

AdaYY; Assertions?

[Lao Xiao Hai]

During the development of Ada 95, there was discussion about
including an assertion capability for pre-conditions, post-conditions,
and invariants.   During a conversation with someone, I was told
the safety-critical community was uneasy about this capability and
felt including it would lead to a false sense of security.

Since then, a lot of additional discussion has emerged regarding ideas
such as Design By Contract.   Also, I am using a textbook, for a C++
data structures class, in which all of the code examples include comment

code for pre-, post- and invariant conditions.   Of course, C++ has no
capability built into the language to support these assertions, so the
compiler can never check them.

It seems to me that Ada's architecture is inherently hospitable to the
concept.
Granted, the type definition model is a kind of implied assertion
capability,
conservative and reliable.  Also granted, one can declare pre-conditions
that
self-contradictory and totally confuse the resulting code.  However, a
modest
addition to the next version of Ada could be a powerful capability and
make
the language conformant with the publication of algorithm textbooks
that,
increasingly, demonstrate their examples by including pre-, post-, and
invariant
assertions.

Richard Riehle
richard@adaworks.com
rdriehle@nps.navy.mil       (I am currently teaching some classes,
including Ada,
                                            at the nearby Naval
Postgraduate School,
                                             and this is my email
address there)

Re: AdaYY; Assertions?

[Florian Weimer]

Lao Xiao Hai <laoxhai@ix.netcom.com> writes:

> Richard Riehle

Split personality? ;-)

Re: AdaYY; Assertions?

[Christoph Grein]

Florian Weimer wrote:
> Lao Xiao Hai <laoxhai@ix.netcom.com> writes:
  Old Little (Hai?)
> 
> > Richard Riehle
> 
> Split personality? ;-)

Re: AdaYY; Assertions?

[Tucker Taft]

Lao Xiao Hai wrote:
> ... However, a
> modest
> addition to the next version of Ada could be a powerful capability and
> make
> the language conformant with the publication of algorithm textbooks
> that,
> increasingly, demonstrate their examples by including pre-, post-, and
> invariant
> assertions.

I agree that adding more assertion support is a good idea.  Note
that most Ada 95 compilers already support "point" assertions
via "pragma Assert(bool_expr [, string_expr]);"

Adding pre/post conditions on subprogram specs at least would be
straightforward.  Adding invariants on private types and/or packages would
also be nice, though it requires a bit more design work relating to the
exact points at which the invariants are checked.

> 
> Richard Riehle
> richard@adaworks.com
> rdriehle@nps.navy.mil       (I am currently teaching some classes,
> including Ada,
>                                             at the nearby Naval
> Postgraduate School,
>                                              and this is my email
> address there)

-- 
-Tucker Taft   stt@avercom.net   http://www.averstar.com/~stt/
Chief Technology Officer, AverCom Corporation (A Titan Company) 
Burlington, MA  USA (AverCom was formerly the Commercial Division of AverStar:
http://www.averstar.com/services/ebusiness_applications.html)

Re: AdaYY; Assertions?

[Stephen Leake]

Lao Xiao Hai <laoxhai@ix.netcom.com> writes:

> <snip> However, a
> modest
> addition to the next version of Ada could be a powerful capability and
> make
> the language conformant with the publication of algorithm textbooks
> that,
> increasingly, demonstrate their examples by including pre-, post-, and
> invariant
> assertions.

So what is your proposal?


-- 
-- Stephe

Re: AdaYY; Assertions?

[Bryce Bardin]

Christoph Grein wrote:
> 
> Florian Weimer wrote:
> > Lao Xiao Hai <laoxhai@ix.netcom.com> writes:
>   Old Little (Hai?)
> >
> > > Richard Riehle
> >
> > Split personality? ;-)

My guess (Pinyin):  Lao2 Xiao3 Hai2
         (English): Old  (Little) Child
 
Maybe "Little old child"?

Re: AdaYY; Assertions?

[Florian Weimer]

Bryce Bardin <bbardin@home.com> writes:

> Christoph Grein wrote:
> > 
> > Florian Weimer wrote:
> > > Lao Xiao Hai <laoxhai@ix.netcom.com> writes:
> >   Old Little (Hai?)
> > >
> > > > Richard Riehle
> > >
> > > Split personality? ;-)
> 
> My guess (Pinyin):  Lao2 Xiao3 Hai2
>          (English): Old  (Little) Child
>  
> Maybe "Little old child"?

Well, 'Lao' is probably a Chinese surname (according to some web page,
it's the 910th most popular surname in the U.S.), and Xiao-Hai a male
forename.

Maybe we should reopen the 'Latin and other irrelevant topics' thread,
shouldn't we? ;-)

Re: AdaYY; Assertions?

[Lao Xiao Hai]

Bryce Bardin wrote:

> My guess (Pinyin):  Lao2 Xiao3 Hai2
>          (English): Old  (Little) Child
>
> Maybe "Little old child"?

Some explanation about my nickname seems to be needed.  Sorry to
take up the bandwidth with this.

Lao Xiao Hai is the name of a character in a humorous Chinese
novel.   It translates to "old man who still behaves like a little
boy."   Connotatively, it can be read, "young at heart" by some.
There is also, Lao Won Tong, which translates to "old playboy,"
and those of you who know me realize that does not quite fit.

The nickname, Lao Xiao Hai, was given to me by the secretary of
the CEO of Beijing Green Valley Software, during one of my visits
to present some Ada seminars in China.  Some of you may recall that
Beijing Green Valley Software is an Ada company in China.  Some of
you also know that I speak, read, and write a little bit of Chinese so
I sometimes sign correspondence in Chinese characters that read,
Lao Xiao Hai.

As far as I know, Beijing Green Valley Software still has Ada projects
in place.  At one time they had hoped to be able to build exportable
software using Ada.   One of the their senior software people even
developed and validated an Ada 83 compiler for that purpose.

I have not heard anything from them for several years.   Perhaps someone
else
out there has more recent news about the state of Ada in China,
particularly
the status of Beijing Green Valley Software.

Richard Riehle
Lao Xiao Hai

Re: AdaYY; Assertions?

[Lao Xiao Hai]

Stephen Leake wrote:

> Lao Xiao Hai <laoxhai@ix.netcom.com> writes:
>
> So what is your proposal?

At this point, my proposal is the addition of a pre-, post-, and invariant
capability to the Ada language, similar to that found in Eiffel.   I fully
realize that it is easier to propose something than to figure out how to
make it work.   The general mechanism, as I see it.

Pre-conditions

These could be applied to a subprogram or a data type.   Since data types
already
have the benefit of range constraints and other features of the type model,
this might
be superfluous.  However,  some properties are not as simple as range
constraints.

What happens when a pre-condition fails.  Eiffel has two basic options:
        1) handle and leave scope (as well as potentially propogating)
        2) handle the exception and retry

I personally have a problem with the retry semantics, but it seems to be
effective
with Eiffel.  Not sure about all the implications for Ada.

I do believe that run-time is the wrong place to find a pre-condition
error.   It is too
late in the process.  However,  if the pre-condition error can be detected
at run-time
and corrective action other than an exception handler be taken, perhaps it
has some
virtue.

Post-conditions

Many of the same issues apply as for pre-conditions.   However, what to do
if a post-condition
fails could be quite different, even problematic.

Invariants

These should apply to the type/class.   Invariants should be inherited.
Eiffel allows overriding of the
invariant (they call it something else, but same general effect).

Ada poses another problem.  Should be have an invariant to applies to an
entire package rather than just
a type?   This problem originates in the Ada model of enclosing a type
declaration within a package.

Other problems

It is easy to craft a self-contradictory assertion.   It would be too much
overhead, and probably impossible,
to include some kind of theorem prover in the compiler to detect such
assertions.

Can assertions contribute to safer code?  That is debatable.  Probably some
assertions are inherently more
safe.   But to rely on assertions, for safety-critical software, might pose
some serious considerations.  I realize
that Bertrand Meyer and others who espouse the Design By Contract philosophy
have made a strong case
for the value of assertions in constructing safer software, but I believe
the jury is still out.

Given my doubts, why do I still support the idea.   It seems to me that a
conservative approach to this issue,
for Ada, can have some real benefits.  If we adhere to some of the existing
syntactic rules and some of the
existing semantics of the language, pre-, post-, and invariant conditions
can be subjected to some rigor
during the compile process.   Trivial example, complex boolean expressions
in Ada require parentheses.

I don't want to seem as if I believe this is a simple change to the
language.  Tucker seems to agree with the
general proposition, and he is much smarter about this kind of thing than
I.  There is a need for more
technical input, more ideas, more criticism, before deciding on this
course.   However, it is a serious enough
issue that it deserves our attention.

As I stated earlier, more and more textbooks are publishing algorithms,
examples of classes, and other
pseudocode fragments in which assertions are part of the code.   Ada can
benefit from being more
compatible with those examples, I believe.

Richard Riehle
Lao Xiao Hai

Re: AdaYY; Assertions?

[Robert A Duff]

Lao Xiao Hai <laoxhai@ix.netcom.com> writes:

> Pre-conditions
> 
> These could be applied to a subprogram or a data type.

I don't understand what a precondition on a type would mean?
Perhaps you meant to say "invariant"?  IMHO, invariants should apply to
types and packages.

> I personally have a problem with the retry semantics, but it seems to be
> effective
> with Eiffel.  Not sure about all the implications for Ada.

I don't like the "retry" thing in Eiffel.  It's no better than a goto
statement.  In fact, it's the worst kind of goto, because it jumps
backwards into the code, rather unexpectedly.  And Meyer's arguments in
favor of retry, based on assertions and whatnot, don't hold water.

> I do believe that run-time is the wrong place to find a pre-condition
> error.   It is too
> late in the process.  However,  if the pre-condition error can be detected
> at run-time
> and corrective action other than an exception handler be taken, perhaps it
> has some
> virtue.

The "obvious" thing to do with a precondition failure in the Ada context
is to raise an exception.  I have thought a lot about how to move this
checking to compile time -- it's not easy.  The same comments apply to
the run-time checks that already exist in Ada.

> These should apply to the type/class.   Invariants should be inherited.
> Eiffel allows overriding of the
> invariant (they call it something else, but same general effect).

I don't recall any way to override an invariant in Eiffel.  The
invariant of the parent class is automatically "and"-ed to the new
invariant (as far as I remember).

- Bob

Re: AdaYY; Assertions?

[Robert I. Eachus]

Robert A Duff wrote:
 
> The "obvious" thing to do with a precondition failure in the Ada context
> is to raise an exception.  I have thought a lot about how to move this
> checking to compile time -- it's not easy.  The same comments apply to
> the run-time checks that already exist in Ada.

And for the same reason.  Requiring an assertion to be checked and raise
an exception is not problematical, and compilers can and should check as
many as possible at compile time, with warnings.

But in the general case, it is not only not possible to check all
interesting post conditions at compile time, it should be trivially
obvious that you can't always statically determine even that the post
condition will be reached.  (And not just in the case of the halting
problem. ;-)

So I certainly favor allowing more general conditions in assertions,
rather than trying to define a compile time checkable set.  And I think
that current compilers do a pretty good job.  For example, if you need
to assert that a number is even, "pramga Assert(N mod 2 = 0);"