edu.ucsb.ccs.jcontractor.transformation
Class InvariantMethodTransformation

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.InvariantMethodTransformation

public class InvariantMethodTransformation

extends ContractMethodTransformation

A transformation to prepare invariant methods. For each class, the transformation searches for an invariant method. The invariant method is modified to call the superclass invariant method before evaluation, and inlined version of invariants inherited from interfaces, and the external invariant defined in a contract class are added. All of these are logical and-ed, so that the invariant may be strengthened, but not weakened. If no invariant method was found, a default invariant method is added to the class. The invariant method in its final form looks something like this:

   return    <interface1 contract>
          && <interface2 contract>
          &&         ...
          && <interfaceN contract>
          && <super contract>
          && <in-class contract>
          && <external contract>
 

Version:

$Id: InvariantMethodTransformation.java,v 1.10 2002/07/14 07:49:30 parkera Exp $

Author:

Parker Abercrombie

Constructor Summary

InvariantMethodTransformation()

Method Summary

void	transformClass() Prepare the invariant method for the current class.
void	transformMethod(org.apache.bcel.generic.MethodGen mg) Does nothing.

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

InvariantMethodTransformation

public InvariantMethodTransformation()

Method Detail

transformClass

public void transformClass()
                    throws AbortTransformationException

Prepare the invariant method for the current class. If it does not exist, insert a default invariant method into the method set. Then modify the invariant to include a call to the superclass invariant, and inline the external invariant, and the invariants that are inherited from interfaces.

Overrides:

transformClass in class Transformation

Throws:

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

See Also:

#checkValidity(JavaClass, MethodGen)

transformMethod

public void transformMethod(org.apache.bcel.generic.MethodGen mg)

Does nothing. This transformation operates only on methods.

Overrides:

transformMethod in class Transformation