edu.ucsb.ccs.jcontractor.transformation
Class PostconditionMethodTransformation

java.lang.Object
  |
  +--edu.ucsb.ccs.jcontractor.transformation.Transformation
        |
        +--edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
              |
              +--edu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation
                    |
                    +--edu.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.

Version:

$Id: PostconditionMethodTransformation.java,v 1.11 2002/07/14 07:54:46 parkera Exp $

Author:

Parker Abercrombie

Constructor Summary

PostconditionMethodTransformation()

Method Summary

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

Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

canCheckEntryInvariant, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInvariant, canHavePostcondition, canHavePrecondition, canReferenceOld, contractsCheckable, getContractClassName, getContractClassName, getInvariantMethodName, getInvariantMethodSignature, getPostconditionMethodName, getPostconditionMethodSignature, getPreconditionMethodName, getPreconditionMethodSignature, isContractClass, isContractMethod, isInvariantMethod, isPostconditionMethod, isPreconditionMethod

Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation

getTransformer, setTransformer, transform

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PostconditionMethodTransformation

public PostconditionMethodTransformation()

Method Detail

transformMethod

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.

Overrides:

transformMethod in class Transformation

Parameters:

mg - the method to operate on. The postcondition method cooresponding to this method will be transformed or created.

Throws:

AbortTransformationException - if the precondition method is invalid, as defined by checkValidity(MethodGen, MethodGen).

See Also:

#checkValidity(MethodGen, MethodGen)

transformClass

public void transformClass()

Does nothing. This transformation operates only on methods.

Overrides:

transformClass in class Transformation