Design by Contract Tool for Java - JMSAssert^TM

Design by Contract  (DBC)  pioneered by  Bertrand Meyer is  widely acknowledged to be a powerful  technique  for  writing  reliable  software.  The  three  key  elements  of  DBC  are preconditions,  postconditions  and  class  invariant. Unfortunately, Java^TM does not directly support DBC. However, JMSAssert brings the benefits of DBC to Java.

Here is how, in a nutshell, you will use JMSAssert.  
  

	The Java program that requires rigorous specification will be annotated at the source level by  using  certain  markers  within  JavadocTM comments.  The three  essential elements  of   DBC  are  precondition,  postcondition  and   class  invariant.  To  use JMSAssert,  you  need  to  first specify  these  elements  (any or all of them)  within Javadoc comments using special tags.
	The  next step is to run  JMSAssert on the Java source code;  this process results in the  automatic  creation of  certain contract files that contain code in JMScriptTM, a Java-based scripting language developed by  Man Machine Systems.  The generated JMScript  code actually represents  triggers that are called  by the assertion runtime to enforce the  explicitly stated  contractual obligations  on the part of suppliers and consumers.
	Finally,  you have to run  the  test driver with assertions enabled.  Invoking the Java runtime with  additional command line parameters does this.  The Java runtime starts up the  JMScript engine and an additional parameter in the command line enables the specified assertions.

 
For a detailed guide to JMSAssert see the document Design by Contract^TM for Java Using JMSAssert^TM which is available online as well as a help file accompanying the product.

JMSAssert is currently available on Windows^TM platforms only.  JDK Versions supported: 1.2.0 to 1.3.1.

Another   great  Java-based  tool   that  supports   Design  by  Contract  is  Reto Kramer's iContract^TM.