Name: krC82822 Date: 04/23/2001


java version "1.2.2" and 1.3
Classic VM (build JDK-1.2.2_007, native threads, symcjit)

This request should not be considered a duplicate of Bug ID
4071460, entitled "Please add assert capability to the Java Language". I am,
herein, requesting support for the principles of 'Design by Contract' (DBC),
as described in chapter 11 of Bertrand Meyer's 'Object-Oriented Software
Construction, Volume II", where Meyer clearly states that DBC is not the
simple "assert" mechanism of C/C++ (which is essentially identical to
the "simple assertion facility" being included with the merlin-beta release of
Java). I find it a shame that all the requests for DBC support were considered
satisfied/closed by the addition of this "simple assertion facility". We don't
want a "simple assertion facility", we want full support for DBC : a software
reliability mechanism that is both extremely powerful and incredibly elegant.

  Description of DBC, by Bertrand Meyer:
"Design by Contract, summarized in the following lines, states:

that one should not write a class without a specification - a contract. The
contract lists the internal consistency conditions that the class will maintain
(the invariant) and, for each operation, the correctness conditions that are
the responsibility of the client (the precondition) and those which the
operation promises to establish in return (the postcondition).

Writing a class without its contract would be similar to producing an
engineering component (electrical circuit, VLSI chip, bridge, engine...)
without a spec. No professional engineer would even consider the idea.

Main DBC features:

Notion of "assertion" : An expression that can be evaluated as true or false.

Notion of "class invariant" : consistency constraints placed on every instance
of a class whenever it is "externally visible" (basically, after creation and
in between every client method invocation). For example, a Person class with
and age attribute may have the assertion "age >= 0" as part of it's invariant.

Notion of "method precondition" : An assertion attached to a method, which must
be guranteed by every client prior to any call to that method. For example, a
method setSSN(String ssn) of our Person class may have the
precondition "ssn.length() == 7".

Notion of "method postcondition" : An assertion attached to a method, which
must be guaranteed by the method's body on return from any call to the method
in which the precondition was satisfied on entry. For example, method setSSN
(String ssn) of our Person class may have the postcondition "getSSN().equals
(ssn)".

"check" or "assert" construct : a language construct that would take an
assertion as input, effectively allowing a programmer to state that he believes
the assertion to hold. For example, "check(ssn.length() == 7)" or "assert
(ssn.length() == 7)". Note that this is not even 1/3 of the facilities of DBC!

So, the elements of a contract are specified using assertions. These assertions
appear as parts of one of three language constructs : invariant, precondition,
postcondition. These are optional constructs. It is up to the runtime system
(when monitoring of the relevant DBC construct is "turned on" via a compilation
option) to verify that the relevant assertions hold at the relevant times (for
example, it should verify that the invariants of a method's precondition hold
before execution of that method). This way, code is not cluttered up with lots
of mindless statement of the following form.

        if (! some_precondition_assertion)
                throw new PreconditionException();

Method bodies can then stay focused on the main task of the routine.

So please, give us the ability to specify precise, unambiguous, and enforceable
details about the behavior of Java objects, that we may increase the quality of
software developed using this language.

(Review ID: 121146)
======================================================================