JDK-4449383 : Support For 'Design by Contract', beyond "a simple assertion facility"
  • Type: Enhancement
  • Component: specification
  • Sub-Component: language
  • Affected Version: 1.3.0,6u10
  • Priority: P5
  • Status: Closed
  • Resolution: Won't Fix
  • OS: generic,solaris_10
  • CPU: generic,sparc
  • Submitted: 2001-04-23
  • Updated: 2011-10-31
  • Resolved: 2011-10-31
Related Reports
Duplicate :  
Description
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) 
======================================================================

Comments
EVALUATION Proposals for new features in the Java programming language are no longer being accepted or maintained in the bug database at http://bugs.sun.com/. This also applies to proposals for new features in the Java Virtual Machine (that is, in the abstract JVM, as opposed to a JVM implementation like HotSpot). All proposals for new features should be made through the "JDK Enhancement - Proposal & Roadmap Process" described at http://openjdk.java.net/jeps/1. Consequently, this specific request to change the Java programming language will not be considered further. The bug database continues to accept and maintain submissions about technical errors in the design and specification of the Java programming language and the Java Virtual Machine.
31-10-2011

EVALUATION DBC is an excellent feature. By way of history, Oak had 'assertions' whereby field values could be constrained and the constraints were enforced at entry and exit of every public and protected method of the class. Methods could have their own pre- and post-conditions too, which were inherited but not redefinable in a subclass. Proving that a method in a subclass has a weaker pre-condition (c.f. contravariance) and a stronger post-condition (c.f. covariance) than the overridden method in a superclass is non-trivial. It is not too late for DBC in Java. It is not a showstopper that the core API has no contracts, nor is the inclusion of contracts in Javadoc particularly hard. The performance hit for class invariants which are enforced all the time (as opposed to just public method entry/exit) is a concern, but many implementation techniques exist. However, just because DBC could happen in the future does not mean it will happen now. Given the existence of assert(), it is hard to justify DBC in JDK7 in place of other, new, language features. As such, I am deferring this RFE. DBC is a perfect candidate for development by the OpenJDK community; a starting point is a source-level mapping from: int foo() pre ASSUME_EXPR post ENSURE_EXPR { BODY } to: int foo() { assert ASSUME_EXPR; try { BODY } finally { assert ENSURE_EXPR; } } (though this doesn't let the post-condition examine the return value)
30-11-2007

WORK AROUND Name: krC82822 Date: 04/23/2001 Develop software in Eiffel. ======================================================================
02-10-2004

EVALUATION I don't expect full design by contract to be supported in the foreseeable future. The decision was made, in the context of the assert statement, not to take that route. ###@###.### 2002-09-24
24-09-2002