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

Quick Search    Search Deep

Class PostconditionMethodTransformation  view PostconditionMethodTransformation 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.PostconditionMethodTransformation

public class PostconditionMethodTransformation
extends ContractMethodTransformation

A transformation to prepare postcondition methods. For each non-contract method in a class, the transformation searches for a postcondition method. The postcondition method is modified to call the superclass postcondition method before evaluation, and inlined versions of postconditions inherited from interfaces, and the external postcondition defined in a contract class are added. All of these are logical and-ed, so that the postcondition may be strengthened, but not weakened. 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 postcondition method in its final form looks something like this:

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

$Id:,v 1.11 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 postcondition method is valid.
protected  boolean prepareMethodBody_Precondition(org.apache.bcel.generic.MethodGen contractMethod, org.apache.bcel.generic.MethodGen mg)
protected  void prepareMethodBody(org.apache.bcel.generic.MethodGen contractMethod, org.apache.bcel.generic.MethodGen mg)
          Prepare the body of a postcondition method.
 void transformClass()
          Does nothing.
 void transformMethod(org.apache.bcel.generic.MethodGen mg)
          Prepare the postcondition method for a non-contract 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 PostconditionMethodTransformation()
Method Detail


public void transformMethod(org.apache.bcel.generic.MethodGen mg)
                     throws AbortTransformationException
Prepare the postcondition method for a non-contract method. If it does not exist, insert a default postcondition method into the method set. Then modify the postcondition to include a call to the super class postcondition, and inline the external postcondition, and the postconditions that are inherited from interfaces. No action is taken the postcondition 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 postcondition method. If the method was just created (its body is empty), it will be given a default body. 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 and-ed.


protected boolean prepareMethodBody_Precondition(org.apache.bcel.generic.MethodGen contractMethod,
                                                 org.apache.bcel.generic.MethodGen mg)


protected void checkValidity(org.apache.bcel.generic.MethodGen method,
                             org.apache.bcel.generic.MethodGen contract)
                      throws AbortTransformationException
Determine if the postcondition 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 strengthen the postcondition.


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