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 $
| 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 java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
PreconditionMethodTransformation
public PreconditionMethodTransformation()
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.
- Specified by:
transformMethod in class Transformation
prepareMethodBody
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.
checkValidity
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:
-
contract may not be abstract. It never makes
sense to have an abstract contract. Either provide an
implementation or don't declare a contract.
-
contract may not be a native method.
Contracts must be written in Java.
- If
method is not private,
contract must be protected. The contract to
a non-private method should be accessible to subclasses,
but no others.
- 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.
- 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.
- 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.
checkValidity_Precondition
protected boolean checkValidity_Precondition(org.apache.bcel.generic.MethodGen method,
org.apache.bcel.generic.MethodGen contract)
transformClass
public void transformClass()
- Does nothing. This transformation operates only on methods.
- Specified by:
transformClass in class Transformation
JAVADOC | 
SOURCE | 
DOWNLOAD | NESTED | FIELD | CONSTR | METHOD