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 $
| 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 |
PostconditionMethodTransformation
public PostconditionMethodTransformation()
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.
- 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 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.
prepareMethodBody_Precondition
protected boolean prepareMethodBody_Precondition(org.apache.bcel.generic.MethodGen contractMethod,
org.apache.bcel.generic.MethodGen mg)
checkValidity
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:
-
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 strengthen the postcondition.
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