Assertions in the Next Ada Standard

Assertions in the Next Ada Standard

[Richard Riehle]

I raised this question several months ago and it seems
to have failed to catch any sustained interest.  The subject
came up again in a phone conversation with ARG member,
Randy Brukardt.

According to Randy, we need a well-crafted proposal to present
to the next ARG meeting in February.  I seem to recall that some
people were already working on this.   Has there been any progress?
Will the proposal be ready for the next ARG meeting?

I am willing to participate in the proposal development process,
and I am sure there are others who would do so.   However, I
understand that someone has already started it, and there is no
point in having multiple conflicting proposals.

I am hoping to see something like pre-conditions, post-conditions,
and invariants in the next revision of Ada.  I would be pleased if
we simply adopted the wording already used in Eiffel:  require,
ensure, and invariant, but I am not intractable about the terminology.

So, who is working on the proposal for this?

Richard Riehle

Re: Assertions in the Next Ada Standard

[Dale Stanbrough]

Richard Riehle wrote:

> I am hoping to see something like pre-conditions, post-conditions,
> and invariants in the next revision of Ada.  I would be pleased if
> we simply adopted the wording already used in Eiffel:  require,
> ensure, and invariant, but I am not intractable about the terminology.
> 
> So, who is working on the proposal for this?
> 
> Richard Riehle

I think another valuable one would be "assume" which is an 
assertion that allows the compiler to invoke any code
optimisation it can.

Dale

Re: Assertions in the Next Ada Standard

[Robert A Duff]

Dale Stanbrough <dstanbro@bigpond.net.au> writes:

> I think another valuable one would be "assume" which is an 
> assertion that allows the compiler to invoke any code
> optimisation it can.

I think that's equivalent to an assertion, plus a pragma Suppress on the
assertion check.

- Bob

Re: Assertions in the Next Ada Standard

[FGD]

Richard Riehle wrote:

> I am hoping to see something like pre-conditions, post-conditions,
> and invariants in the next revision of Ada.  I would be pleased if
> we simply adopted the wording already used in Eiffel:  require,
> ensure, and invariant, but I am not intractable about the terminology.

Though I'm not familiar with Eiffel and its use of those idioms, but 
this sounds like an attractive proposal. However, if you allow me to 
play Devil's advocate, could you give a concrete example where this has 
significant benefits.

For suprograms, this doesn't seem essential because of Ada's strong 
typing. It may however be very useful for loops and related constructs. 
But I can find *weak* replacements within Ada. For invariants, enclose 
loops in a block statement, e.g.

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

This also allows for catching exceptions locally, or use pragma Suppress 
to allow optimizations. For require and ensure, enclose the loop in an 
inlined procedure similar to the above. These replacements are weak 
because Ada types cannot conveniently represent assertions such as X /= 
0 or X > Y for variable X and Y. Perhaps some type improvements could do 
the job instead?

There is one place where I can see some genuine benefits. It would be 
possible to specify exception conditions in declarative parts, e.g. 
(improvised syntax)

     function "/" (L, R : Integer_Type) return Integer_Type;
     for "/" require R /= 0;

     function "*" (L, R : Matrix) return Matrix;
     for "*" require L.Columns = R.Rows;
     for "*" ensure return.Rows = L.Rows;
     for "*" ensure return.Columns = R.Columns;

Or perhaps type improvements could do the job:

     -- Disconnected ranges?

     subtype Nonzero_Integer_Type is Integer_Type
         range Integer_Type'First .. -1 | 1 .. Integer_Type'Last;

     function "/"
         (L : Integer_Type;
          R : Nonzero_Integer_Type)
         return Integer_Type

     -- Dummy discriminants?

     function "*"
         (L : Matrix(Rows => M, Columns => L);
          R : Matrix(Rows => L, Columns => N))
         return Matrix(Rows => M, Columns => N);

Perhaps I'm missing something, how does Eiffel use these?

-- Frank

Re: Assertions in the Next Ada Standard

[Wes Groleau]

>      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

Re: Assertions in the Next Ada Standard

[Nick Roberts]

"Dale Stanbrough" <dstanbro@bigpond.net.au> wrote in message
news:dstanbro-07F79B.20222311012002@mec2.bigpond.net.au...

> Richard Riehle wrote:
>
> > I am hoping to see something like pre-conditions, post-conditions,
> > and invariants in the next revision of Ada.  I would be pleased if
> > we simply adopted the wording already used in Eiffel:  require,
> > ensure, and invariant, but I am not intractable about the terminology.
> >
> > So, who is working on the proposal for this?
> >
> > Richard Riehle
>
> I think another valuable one would be "assume" which is an
> assertion that allows the compiler to invoke any code
> optimisation it can.


A counter-argument to the addition of any of these facilities being added
can be illustrated in the following procedure:


   subtype Must_Be_True is Boolean range True..True;


   procedure P (...) is
      ...
      [invar.]: constant ... := [i. expr.]; --D
      [a. name]: constant Must_Be_True := [assumption]; --D
   begin
      if [debug] and then not [pre-conditions] then raise [excep.]; end
if; --D
      ...
      if [debug] and then not [post-conditions] then raise [excep.]; end
if; --D
      if [debug] and then not [invar.] /= [i. expr.] then raise [excep.];
end if; --D
   end P;


This procedure demonstrates how pre-conditions, post-conditions, invariants,
and assumptions can all be programmed in existing Ada. For efficiency,
certain assumptions may be made of the compiler, in terms of static
evaluation and/or dead code removal (but these would effectively be required
for the efficient implementation of the proposed pragmas).

A procedure such as P could be made a 'wrapper' to another Q (which does the
real work). P could then be replaced by Q when debugging is completed.
Alternatively, a simple text modification tool could be used to remove all
lines containing "--D".

It may seem like an extreme form of Blimpism to argue against the suggested
pragmas, but I have found in real code that I often wanted to code quite com
plicated test routines into subprograms for debugging purposes. I can't
believe I'm the only one who has found this. The proposed pragmas would be
of little advantage in these cases (they can only take an expression).

Sometimes, what sounds like a great idea turns out not to be so brilliant
when you closely look at it. And sometimes, it turns out that a bigger idea
subsumes it anyway. (Read on... ;-)

One little thing that (I think there is wide agreement on) would be most
welcome would be a 'raise ... when ...;' statement:


   procedure P (...) is
      ...
      [invar.]: constant ... := [i. expr.]; --D
      [a. name]: constant Must_Be_True := [assumption]; --D
   begin
      raise [excep.] when [debug] and then not [pre-conditions]; --D
      ...
      raise [excep.] when [debug] and then not [post-conditions]; --D
      raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; --D
   end P;


However, a major new feature that I would like to see introduced at the next
revision would be a provision for 'separation of concerns'. As a 'straw
man', this might work something like as follows.

Each declarative item which is or can contain a subprogram requires a
completion in Ada 95. In the case of a subprogram, the completion (the body)
is permitted to be the declaration also. My proposed facility would permit
multiple completions for a subprogram (separately declared). The facility
would always apply to a library unit: if the unit is a package, all the
subprograms in the package would be permitted multiple completions.

For example, the declaration of a library procedure P might be declared:


   procedure P ([parameters]);


A new kind of library-level declaration would allow a set of different
'aspects' to be declared, together with a pattern for the way in which they
are applied to subprograms. E.g.:


   procedure P ([parameters]) is separate (Debugging.Before, Main_Function,
Debugging.After);


This declares that P has three separate completions, named Debugging.Before,
Main_Function, Debugging.After. There is also a fourth optional completion,
Debugging, which is a kind of 'parent' to Debugging.Before and
Debugging.After. Whenever P is called, all three declared completions will
be called, in the order declared. The fourth completion, Debugging, will
also be called, before those for Debugging.Before and Debugging.After. The
completions would look similar to current Ada subunits:


   separate (Main_Function)
   procedure P ([parameters]) is
      ...
   begin
      ...
   end P;


A completion for Debugging allows for shared declarations, and an
initialisation:


   separate (Debugging)
   procedure P ([parameters]) is
      [invar.]: constant ... := [i. expr.];
      [a. name]: constant Must_Be_True := [assumption];
   begin
      null;
   end P;


This body will be executed before those for Debugging.Before and
Debugging.After (to provide a set of common declarations for them, and
possibly an initialisation).

Finally, we must separately complete the final two outstanding bodies:



   separate (Debugging.Before)
   procedure P ([parameters]) is
   begin
      raise [excep.] when [debug] and then not [pre-conditions];
   end P;


   separate (Debugging.After)
   procedure P ([parameters]) is
   begin
      raise [excep.] when [debug] and then not [post-conditions];
      raise [excep.] when [debug] and then not [invar.] /= [i. expr.];
   end P;


Things get a little more complex with packages. Here we define a pattern
that applies to all the subprograms the package contains implicitly. E.g.:


   package My_Stuff.Utilities is
      procedure P (...);
      procedure Q (...);
      ...
   end;


   package My_Stuff.Utilities is separate (Debugging.Before, Main_Function,
Debugging.After);


There are now three bodies required to fully complete this package, one for
each of the three aspects. I have also chosen to make the package a child,
to illustrate naming within hierarchies. Within each of the package bodies,
the completions of the given aspect of each of the package's subprograms
must be given. E.g.:


   separate (Main_Function)
   package My_Stuff.Utilities body is

      procedure P (...) is
         ...
      begin
         ... -- implementation of P's main functionality
      end;

      procedure Q (...) is separate;

   end;


I have made the completion of Q a normal subunit, to illustrate the naming
scheme:


   separate (My_Stuff.Utilities.Main_Function)
   procedure Q (...) is
      ...
   end Q;


There would then be:


   separate (Debugging)
   package My_Stuff.Utilities is
      -- any declarations common to Debugging.Before and Debugging.After
   begin
      -- any initialisation code
   end;


   separate (Debugging.Before)
   package My_Stuff.Utilities is

      procedure P (...) is
      begin
         raise [excep.] when [debug] and then not [pre-conditions];
      end P;

      procedure Q (...) is null;

   end;


   separate (Debugging.After)
   package My_Stuff.Utilities is

      procedure P (...) is
      begin
         raise [excep.] when [debug] and then not [post-conditions];
         raise [excep.] when [debug] and then not [invar.] /= [i. expr.];
      end P;

      procedure Q (...) is null;

   end;


I have invented a new form of null procedure, which would probably be handy.
(A bit analogous to the new form of null record declaration for types.)

Finally, each completion would be permitted to be a completion by renaming,
as normal. In many cases, this would greatly facilitate code re-use (if the
design is good).


Obviously there are a lot of details to fill in on this one. But hopefully
it can be seen how it solves the problem of the separation of debugging
code, as well as helping to solve the problems of code separation in a much
wider way.

--
Best wishes,
Nick Roberts

Re: Assertions in the Next Ada Standard

[Darren New]

Nick Roberts wrote:
> This procedure demonstrates how pre-conditions, post-conditions, invariants,
> and assumptions can all be programmed in existing Ada. 

Except for the inheritance rules. It's a bit more complicated than you
can do with in-line code, in exactly the same way that throwing
exceptions and returning error-code values are different.

(Note that you also forgot to check the invariant upon entry. Except for
routines that initialize limited variables. Etc.)

-- 
Darren New 
San Diego, CA, USA (PST). Cryptokeys on demand.
  The opposite of always is sometimes.
   The opposite of never is sometimes.

Re: Assertions in the Next Ada Standard

[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

Re: Assertions in the Next Ada Standard

[Richard Riehle]

FGD wrote:

> Richard Riehle wrote:
>
> > I am hoping to see something like pre-conditions, post-conditions,
> > and invariants in the next revision of Ada.  I would be pleased if
> > we simply adopted the wording already used in Eiffel:  require,
> > ensure, and invariant, but I am not intractable about the terminology.

> For suprograms, this doesn't seem essential because of Ada's strong
> typing. It may however be very useful for loops and related constructs.
> But I can find *weak* replacements within Ada. For invariants, enclose
> loops in a block statement, e.g.

I have snipped the corresponding code for sake of economy.

For greatest benefit, the pre-conditions, post-conditions and invariants
would be declared in the package specification.   The does not preclude
declaring some in subprograms, but that is not my focus, at present.

Taking the invariant, first.    At present, there is no construct in Ada
that
is package-wide or type-wide except the type declaration itself.   All that
one can do with a type declaration is declare a range or a set of
operations.
OK, one can do a little more, but that is beside the point.

For a type, an invariant declaration simply adds some additional rules
for that type.    For example, one cannot declare a discontinous range
for a numeric type, but an invariant might state that a value of that
numeric type cannot ever be zero.   This would be stated (asserted)
in the package specfication.   For other types, boolean expressions
could be declared that would further constrain a type with a more
rigorous invariant.

I will address the problem with this a little later in this posting.

Pre-conditions and post-conditions would be part of the declaration of
each subprogram.   Post-conditions are particularly worthwhile because
there is, for access to composite type parameters,  potential for
side-effects
that might be unknown to the client of a specification.   A post-condition
can guarantee there are no unchecked side-effects.

Pre-conditions might be less useful given many of the controls already
in place for parameter lists in subprograms.    However, one might declare
a pre-condition that prevents a subprogram from executing if some
combination of parameters is invalid.

Now to the problems.   First, there is the danger that one might be able to
construct a self-cancelling boolean expresssion as an assertion.  We
are not very sophisticated in the automated theorem proving in the
world of computer science, even though there is some progress.   The
person who constructs an assertion might be tempted to rely on it
to the exclusion of more careful inspection.     Second,  in an inheritance
scheme, what do we do about either inheriting or overriding a assertion.
This problem is non-trivial.   I am not sure I have the answer,  and that
is why there is a need for more people thinking about this than we have
so far.

In a later post, one beyond this one in chronology, Dr. Dewar makes a
good point.   He announces that within in his customer base, there has
been very little interest in this feature.   Given some of the other
postings
I have seen so far, I am not surprised since it does not seem to be a
well-understood concept within the larger Ada community.  Certainly,
many who frequent this forum do understand it and I would expect
people such as Robert Duff to weigh in with well-reasoned criticisms.
The fact that there is very little demand for assertions might be said
of other seldom used and little understood features already in the language.

I would like to see us engage in dialogue about this idea in terms of
its intrinsic merits and and potential for harm rather than depend on the
immediate demand of the day-to-day current Ada practitioner.

Richard Riehle

Re: Assertions in the Next Ada Standard

[FGD]

Ah! I see now that your proposal is deeper than what I originally 
thought it was. I see also that it does addresses some very real issues 
of Ada.

As you point out yourself, when it comes to incorporating them in the 
current Ada framework, invariants and pre-/post-conditions are quite 
different. Invariants are connected to types whereas conditions pertain 
to subprograms and their parameters. Consider dividing it in two related 
proposals to avoid opposition to one reject the other.

  Invariants constitute a "type improvement" as I would have said in my 
first reply. As such they are desirable, they provide a nice way of 
defining disconnected ranges and imposing constraints on type 
discriminants for example. Safety is an issue, but we know enough to 
work around it. The sublanguage of assertions should be constrained so 
that it cannot describe conditions which are not polytime---we know how 
to do that. More severe restrictions will probably be imposed, and very 
severe restrictions should apply if some kind of non-static assertions 
are to be allowed. Since the sublanguage of assertions should contain 
boolean variables and all propositional connectives, the problem of 
deciding whether or not a particular assertion is ever true is 
NP-complete. Thus one cannot reasonably expect compile time warnings for 
all such conditions. Some may object to that, but I consider this to be 
the programmer's problem.

 From my perspective, invariants have many merits. The most important is 
that it provides a uniform way of implementing all the type improvements 
I ever thought of in a uniform way. I'm still not sure about 
pre-/post-conditions. Right now, it seems to me that the associated 
complexities outnumber the benefits and I'm still curious about 
practical applications...

-- Frank

Re: Assertions in the Next Ada Standard

[Ed Falis]

FGD wrote:


>  From my perspective, invariants have many merits. The most important is 
> that it provides a uniform way of implementing all the type improvements 
> I ever thought of in a uniform way. I'm still not sure about 
> pre-/post-conditions. Right now, it seems to me that the associated 
> complexities outnumber the benefits and I'm still curious about 
> practical applications...

In the Eiffel model, the purpose of pre and post conditions is to 
establish the contract between caller and callee.  The practical benefit 
is that if a precondition is violated, then client code is where you 
look to find the problem;  if the postcondition is violated the service 
code is where you start.  An additional advantage of this approach is 
the elimination of code in services that would check explicitly for 
violations of the preconditions during deployment (the usual model is to 
enable pre and post condition checking during development, and to 
disable it during deployment).

- Ed

Re: Assertions in the Next Ada Standard

[Darren New]

Richard Riehle wrote:
> For a type, an invariant declaration simply adds some additional rules
> for that type.    For example, one cannot declare a discontinous range
> for a numeric type, but an invariant might state that a value of that
> numeric type cannot ever be zero.   This would be stated (asserted)
> in the package specfication.   For other types, boolean expressions
> could be declared that would further constrain a type with a more
> rigorous invariant.

Actually, if you wanted to follow the Eiffel model for this, the
invariant would be that the values of the type have to obey the
invariants unless you're running the body of a primitive operation of
that type. That is, if you had something like

type x is new integer;
invariant x /= 0; -- Or whatever syntax
procedure increment(value : in out x) is
begin
  value := value + 1;
  if value = 0 then value = 1; end if;
end increment;

then it would be legal to call increment with a value of -1, and the
first line of increment would not cause an exception.

> Pre-conditions and post-conditions would be part of the declaration of
> each subprogram.   Post-conditions are particularly worthwhile because
> there is, for access to composite type parameters,  potential for
> side-effects
> that might be unknown to the client of a specification.   A post-condition
> can guarantee there are no unchecked side-effects.

It's really, really difficult to rule out side-effects with
post-conditions. Indeed, some of the hardest post-conditions are those
of side-effects. For example, you do a Put on a file, and the
postcondition is very unlikely to be able to express what that actually
does in terms of future Gets.
 
> Pre-conditions might be less useful given many of the controls already
> in place for parameter lists in subprograms.    However, one might declare
> a pre-condition that prevents a subprogram from executing if some
> combination of parameters is invalid.

That's generally what they're good for, yes. Like, don't pop empty
stacks, don't real closed files, and stuff like that. Most any
subprogram that raises an exception specific to the package would be
using preconditions instead.
 
> Now to the problems.   First, there is the danger that one might be able to
> construct a self-cancelling boolean expresssion as an assertion. 

Not sure what a "self-cancelling" boolean expression is. You mean a
tautology? Or a negation of a tautology?

> We
> are not very sophisticated in the automated theorem proving in the
> world of computer science, even though there is some progress.

Actually, "we" are. It's just a very difficult problem, with lots of NP
stuff involved.

>   The
> person who constructs an assertion might be tempted to rely on it
> to the exclusion of more careful inspection. 

Indeed. That's part of the point of doing it, at least for
preconditions. If your precondition is "don't pop an empty stack", then
you don't have to implement pop to handle the case of an empty stack.
This is actually a good thing.

Well, not that the person won't "inspect", but that the implementation
will be more straightforward.

>    Second,  in an inheritance
> scheme, what do we do about either inheriting or overriding a assertion.
> This problem is non-trivial.   I am not sure I have the answer,  and that
> is why there is a need for more people thinking about this than we have
> so far.

This is pretty well considered in Eiffel, actually. Indeed, the strength
of Eiffel's "DbC" assertions over those of just inlining boolean checks
is that they *do* get inherited in the "right way".
 
-- 
Darren New 
San Diego, CA, USA (PST). Cryptokeys on demand.
  The opposite of always is sometimes.
   The opposite of never is sometimes.

Re: Assertions in the Next Ada Standard

[Robert A Duff]

Darren New <dnew@san.rr.com> writes:

> >    Second,  in an inheritance
> > scheme, what do we do about either inheriting or overriding a assertion.
> > This problem is non-trivial.   I am not sure I have the answer,  and that
> > is why there is a need for more people thinking about this than we have
> > so far.
> 
> This is pretty well considered in Eiffel, actually. Indeed, the strength
> of Eiffel's "DbC" assertions over those of just inlining boolean checks
> is that they *do* get inherited in the "right way".

The right way for Eiffel, perhaps.  But Ada makes has a distinction
between class-wide and specific types, which is not present in Eiffel,
so the Eiffel rules don't quite translate over to Ada.  I think you
really want *two* preconditions on a dispatching procedure: one that
applies to non-dispatching calls, and one that applies to dispatching
calls.  This is so the specific type can provide a stronger contract
than is provided by the whole class.  Same for post-cond.

The Eiffel rules are certainly a good starting point.  But it would
require some thought to translate them into the Ada world.

- Bob

Re: Assertions in the Next Ada Standard

[Darren New]

Robert A Duff wrote:
> The Eiffel rules are certainly a good starting point.  But it would
> require some thought to translate them into the Ada world.

No question. My point was that DbC *should* be more than what you could
do with just a macro preprocessor translator into inline asserts. The
right answer for Ada, with tasks, protected types, tagged types, limited
types, etc is likely to be far more complex than for a language as
simple as Eiffel.

Unfortunately, I don't have enough experience with Ada to have a good
idea of all the pitfalls I'd run into if I tried to work something out
myself. :-)

-- 
Darren New 
San Diego, CA, USA (PST). Cryptokeys on demand.
  The opposite of always is sometimes.
   The opposite of never is sometimes.

Re: Assertions in the Next Ada Standard

[Mark Lundquist]

"Richard Riehle" <richard@adaworks.com> wrote in message
news:3C3FE630.BDB27416@adaworks.com...
<[..snip..]
> The fact that there is very little demand for assertions might be said
> of other seldom used and little understood features already in the
language.

Good point.

>
> I would like to see us engage in dialogue about this idea in terms of
> its intrinsic merits and and potential for harm rather than depend on the
> immediate demand of the day-to-day current Ada practitioner.

Re: Assertions in the Next Ada Standard

[Richard Riehle]

I appreciate the thoughtful contributions regarding
assertions in next Ada standard.   It was my understanding
someone was drafting a proposal for this and I was
hoping to see some comment from whoever that might
be.

Meanwhile, I clipped the following from a discussion about
the assertion mechanism in Java from a discussion on comp.object.


------------------ quote from comp.object -------------------------
The documentation at Sun recommends NOT using assertions
to check argument values on public methods.  You should
still continue to do this kind of thing with if statement
and throw IllegalArgumentException.

--------------------<quote from Sun>---------------------
    3.Why not provide a full-fledged design-by-contract
      facility with preconditions, postconditions and class
      invariants, like the one in the Eiffel programming
      language?

     We considered providing such a facility, but were unable
     to convince ourselves that it is possible to graft it
     onto the Java programming language without massive changes
     to the Java platform libraries, and massive inconsistencies
     between old and new libraries. Further, we were not
     convinced that such a facility would preserve the
     simplicity that is Java's hallmark. On balance, we came to
     the conclusion that a simple boolean assertion facility was
     a fairly straight-forward solution and far less risky. It's
     worth noting that adding a boolean assertion facility to
     the language doesn't preclude adding a full-fledged design-
     by-contract facility at some time in the future.
-----------------<end of quote from Sun>-------------------
----------------- end of quote from comp.object ---------------



> Richard Riehle