edu.ucsb.ccs.jcontractor.transformation
Class PreconditionMethodTransformation

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

Version:

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

Author:

Parker Abercrombie

Constructor Summary

PreconditionMethodTransformation()

Method Summary

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

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

PreconditionMethodTransformation

public PreconditionMethodTransformation()

Method Detail

transformMethod

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.

Overrides:

transformMethod in class Transformation

Parameters:

mg - the method to operate on. The precondition 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