Docjar: A Java Source and Docuemnt Enginecom.*    java.*    javax.*    org.*    all    new    plug-in

Quick Search    Search Deep

Class PreconditionMethodTransformation  view PreconditionMethodTransformation download

  extended byedu.ucsb.ccs.jcontractor.transformation.Transformation
      extended byedu.ucsb.ccs.jcontractor.transformation.ContractTransformation
          extended byedu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation
              extended byedu.ucsb.ccs.jcontractor.transformation.PreconditionMethodTransformation

public class PreconditionMethodTransformation
extends ContractMethodTransformation

A transformation to prepare precondition methods. For each non-contract method in a class, the transformation searches for a precondition method. The precondition method is modified to call the superclass precondition method before evaluation, and inlined versions of preconditions inherited from interfaces, and the external precondition defined in a contract class are added. The superclass precondition is logical or-ed with the interface conditions, and the subclass precondition. The subclass precondition is constructed by and-ing the in-class precondition with the external precondition. If no postcondition method was found, a default postcondition method is added to the class. The default method just calls the super class method. The precondition method in its final form looks something like this:

   return    <interface1 contract>
          || <interface2 contract>
          ||         ...
          || <interfaceN contract>
          || <super contract>
          || (<subclass contract>
              && <external contract>)
For methods that cannot have inherited contracts (static and private methods, for example), only the in-class contract and the external contract are taken into account.

$Id:,v 1.8 2002/07/14 07:54:46 parkera Exp $

Field Summary
Fields inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation
Constructor Summary
Method Summary
protected  boolean checkValidity_Precondition(org.apache.bcel.generic.MethodGen method, org.apache.bcel.generic.MethodGen contract)
protected  void checkValidity(org.apache.bcel.generic.MethodGen method, org.apache.bcel.generic.MethodGen contract)
          Determine if the precondition method is valid.
protected  void prepareMethodBody(org.apache.bcel.generic.MethodGen contractMethod, org.apache.bcel.generic.MethodGen mg)
          Prepare the body of a precondition method.
 void transformClass()
          Does nothing.
 void transformMethod(org.apache.bcel.generic.MethodGen mg)
          Prepare the precondition method for a normal method.
Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation
acceptClass, combineContracts_and_Postcondition, combineContracts_and_Precondition, combineContracts_and, combineContracts_or_Postcondition, combineContracts_or_Precondition, combineContracts_or, createContractMethod, getExternalContract, getInterfaceContracts, getSuperClassContract_Precondition, getSuperClassContract, redirectClassReference
Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
append, canCheckEntryInvariant, canCheckExitInvariant_Precondition, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInheritedContract_Precondition, canHaveInheritedContract, canHaveInvariant_Precondition, canHaveInvariant, canHavePostcondition_Precondition, canHavePostcondition, canHavePrecondition_Precondition, canHavePrecondition, canReferenceOld_Precondition, canReferenceOld, contractsCheckable_Precondition, contractsCheckable, createLoadArguments_Postcondition, createLoadArguments_Precondition, createLoadArguments, entryInvariantCheckable_Precondition, findMethod, findMethod, findMethodIndex, getContractClassName_Postcondition, getContractClassName_Postcondition, getContractClassName_Precondition, getContractClassName_Precondition, getContractClassName, getContractClassName, getInvariantMethodName_Postcondition, getInvariantMethodName_Precondition, getInvariantMethodName, getInvariantMethodSignature_Postcondition, getInvariantMethodSignature_Precondition, getInvariantMethodSignature, getPostconditionMethodName_Postcondition, getPostconditionMethodName_Precondition, getPostconditionMethodName, getPostconditionMethodSignature_Postcondition, getPostconditionMethodSignature_Precondition, getPostconditionMethodSignature, getPreconditionMethodName_Postcondition, getPreconditionMethodName_Precondition, getPreconditionMethodName, getPreconditionMethodSignature_Postcondition, getPreconditionMethodSignature_Precondition, getPreconditionMethodSignature, hasExternalContract, hasInterfaceContract, hasSuperClassContract, isContractClass_Postcondition, isContractClass_Precondition, isContractClass, isContractMethod_Postcondition, isContractMethod_Precondition, isContractMethod, isInvariantMethod_Precondition, isInvariantMethod, isPostconditionMethod_Postcondition, isPostconditionMethod, isPreconditionMethod_Precondition, isPreconditionMethod, postconditionCheckable_Precondition, preconditionCheckable_Precondition, prepend, prependToConstructor_Precondition, prependToConstructor, replaceInstruction, replaceInstruction, replaceReturnInstructions_Precondition, replaceReturnInstructions
Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation
acceptClass_Precondition, getTransformer_Postcondition, getTransformer, setTransformer_Postcondition, setTransformer_Precondition, setTransformer, transform_Precondition, transform, transformClass_Precondition, transformMethod_Precondition
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail


public PreconditionMethodTransformation()
Method Detail


public void transformMethod(org.apache.bcel.generic.MethodGen mg)
                     throws AbortTransformationException
Prepare the precondition method for a normal method. If the precondition method already exists, modify it to include a call to the super class precondition. If it does not exist, insert a default precondition method into methods. No action is taken the precondition is not checkable.

Specified by:
transformMethod in class Transformation


protected void prepareMethodBody(org.apache.bcel.generic.MethodGen contractMethod,
                                 org.apache.bcel.generic.MethodGen mg)
Prepare the body of a precondition method. If the method was just created (its body is empty), it will be given a default body. Otherwise, a call to the superclass contract method will be prepended, and any external and interface contracts will be inlined. The superclass condition, external, interface, and subclass condition will be logical or-ed. The subclass contract is formed by and-ing the in-class contract with the external contract.


protected void checkValidity(org.apache.bcel.generic.MethodGen method,
                             org.apache.bcel.generic.MethodGen contract)
                      throws AbortTransformationException
Determine if the precondition method is valid. The method is considered valid if it meets the following constraints:
  1. contract may not be abstract. It never makes sense to have an abstract contract. Either provide an implementation or don't declare a contract.
  2. contract may not be a native method. Contracts must be written in Java.
  3. If method is not private, contract must be protected. The contract to a non-private method should be accessible to subclasses, but no others.
  4. If method is private, contract must also be private. If this were not the case, contract would inherit, while method would not. Thus, if a subclass declared a new method with the same name as method, contract would be applied to it, which is incorrect.
  5. If method is static, contract must also be static. Conversly, if method is not static, contract may not be static. One reason for this rule is that method could not call contract if it were static and contract were not. Another reason is that static methods do not inherit in the same way as non-static methods (subclasses hide them, instead of override them). A method and its contract should inherit together.
  6. If method is final, contract must also be final. Likewise, if method is not final, contract cannot be final. The reason behind this rule is that if a method has been frozen by declaring it final, its contract must also be frozen (it wouldn't do to have subclasses changing the contract). Also, it is illegal to freeze the contract without also freezing the method. Subclasses must always be allowed to weaken the precondition.


protected boolean checkValidity_Precondition(org.apache.bcel.generic.MethodGen method,
                                             org.apache.bcel.generic.MethodGen contract)


public void transformClass()
Does nothing. This transformation operates only on methods.

Specified by:
transformClass in class Transformation