Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

edu.ucsb.ccs.jcontractor.transformation
Class ContractTransformation

java.lang.Object
  |
  +--edu.ucsb.ccs.jcontractor.transformation.Transformation
        |
        +--edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
Direct Known Subclasses:
AppendReturnTransformation, ContractCheckTransformation, ContractMethodTransformation, LoadContractClassTransformation, LockCloneTransformation, RemoveContractMethodsTransformation, ReplaceOldReferencesTransformation, ReplaceReturnInstructionsTransformation, SaveOldStateTransformation
public abstract class ContractTransformation
extends Transformation

Abstract super class for contract transformations. This class defines methods that determine the names and signatures of contract methods, and defines the rules about which methods may have which sorts of contracts, and when contracts are checked. Logic about the naming conventions used by jContractor, and about the rules of when contracts can be checked is encapsulated in this class.

This class also defines several utility methods that are useful for working with InstructionLists.

Version:
$Id: ContractTransformation.java,v 1.18 2002/07/14 07:47:00 parkera Exp $
Author:
Parker Abercrombie

Constructor Summary
ContractTransformation()
           
 
Method Summary
 boolean canCheckEntryInvariant(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method should have a invariant check at its entry point.
 boolean canCheckExitInvariant(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method should have a invariant check at its exit point.
 boolean canCheckPostcondition(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method should have a postcondition check.
 boolean canCheckPrecondition(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method should have a precondition check.
 boolean canHaveInvariant(org.apache.bcel.classfile.JavaClass javaclass)
          Determine whether or not a class can have an invariant.
 boolean canHavePostcondition(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method can have a postcondition, taking instrumentation level into account.
 boolean canHavePrecondition(org.apache.bcel.generic.MethodGen mg)
          Determine whether or not this method can have a precondition, taking instrumentation level into account.
 boolean canReferenceOld(org.apache.bcel.generic.MethodGen mg)
          Determine if the postcondition for a non-contract method can refer to OLD.
 boolean contractsCheckable(org.apache.bcel.classfile.JavaClass javaclass)
          Determine whether or not contracts should be checked on the methods in a class.
 java.lang.String getContractClassName(org.apache.bcel.classfile.JavaClass javaclass)
          Get the name of the external contract class that cooresponds to the given class.
 java.lang.String getContractClassName(java.lang.String classname)
          Get the name of the external contract class that cooresponds to the given class name.
 java.lang.String getInvariantMethodName(org.apache.bcel.classfile.JavaClass javaclass)
          Get the name of the invariant method for a class.
 java.lang.String getInvariantMethodSignature(org.apache.bcel.classfile.JavaClass javaclass)
          Get the signature of the invariant method for a class.
 java.lang.String getPostconditionMethodName(org.apache.bcel.generic.MethodGen m)
          Get the name of the postcondition method for a non-contract method.
 java.lang.String getPostconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
          Get the signature of the method that defines the postcondition for a non-contract method.
 java.lang.String getPreconditionMethodName(org.apache.bcel.generic.MethodGen method)
          Get the name of the precondition method for a non-contract method.
 java.lang.String getPreconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
          Get the signature of the method that defines the precondition for a non-contract method.
 boolean isContractClass(org.apache.bcel.classfile.JavaClass javaclass)
          Determine if a class defines contracts for another class.
 boolean isContractMethod(org.apache.bcel.generic.MethodGen m)
          Determine if a method defines a contract (precondition, postcondition, or invariant).
 boolean isInvariantMethod(org.apache.bcel.generic.MethodGen m)
          Determine if a method defines a class invariant.
 boolean isPostconditionMethod(org.apache.bcel.generic.MethodGen m)
          Determine if a method defines a postcondition.
 boolean isPreconditionMethod(org.apache.bcel.generic.MethodGen m)
          Determine if a method defines a precondition.
 
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

ContractTransformation

public ContractTransformation()
Method Detail

canHavePrecondition

public boolean canHavePrecondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method can have a precondition, taking instrumentation level into account. All methods in classes that are instrumented to the InstrumentationFilter.PRE level or greater can have preconditions except: Note that their is a subtle difference between a method that can have a precondition, and a method on which a precondition can be checked. The difference arises in abstract methods, which can have preconditions, but the contracts can only be checked in implementation classes. canCheckPrecondition(MethodGen) answers the checkabilty question.

Returns:
true if the method can have a precondition.
See Also:
InstrumentationFilter, canCheckPrecondition(MethodGen)

canHavePostcondition

public boolean canHavePostcondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method can have a postcondition, taking instrumentation level into account. All methods in classes that are instrumented to the InstrumentationFilter.POST level or greater can have postconditions except: Note that their is a subtle difference between a method that can have a postcondition, and a method on which a postcondition can be checked. The difference arises in abstract methods, which can have contracts, but the contracts can only be checked in implementation classes. canCheckPostcondition(MethodGen) answers the checkabilty question.

Returns:
true if the postcondition should be checked.
See Also:
InstrumentationFilter, canCheckPostcondition(MethodGen)

canHaveInvariant

public boolean canHaveInvariant(org.apache.bcel.classfile.JavaClass javaclass)
Determine whether or not a class can have an invariant. Only classes that that are instrumented to the InstrumentationFilter.ALL level can have invariant checks.

Parameters:
javaclass - a class to test.
Returns:
true if the class can have invariant checks.
See Also:
InstrumentationFilter, canCheckExitInvariant(MethodGen), canCheckEntryInvariant(MethodGen)

contractsCheckable

public boolean contractsCheckable(org.apache.bcel.classfile.JavaClass javaclass)
Determine whether or not contracts should be checked on the methods in a class. This check is independent of the methods defined in the class. Contracts are checkable in all classes except:

Parameters:
javaclass - a class to check.
Returns:
true if contracts may be checked on javaclass (ie true if javaclass is not a contract class).
See Also:
isContractClass(JavaClass)

canCheckPrecondition

public boolean canCheckPrecondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a precondition check. Preconditions may be checked for all methods except: Note that abstract methods may have preconditions, but the conditions can only be checked when the method is implemented in a subclass.

Returns:
true if the precondition should be checked.
See Also:
canHavePrecondition(MethodGen)

canCheckPostcondition

public boolean canCheckPostcondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a postcondition check. Postconditions should be checked on all methods that have postconditions, except: Note that abstract methods may have postconditions, but the conditions can only be checked when the method is implemented in a subclass.

Returns:
true if the postcondition should be checked.
See Also:
canHavePostcondition(MethodGen)

canCheckEntryInvariant

public boolean canCheckEntryInvariant(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a invariant check at its entry point. Entry invariants may be checked for all methods except:

Returns:
true if the entry invariant should be checked.
See Also:
canCheckExitInvariant(MethodGen)

canCheckExitInvariant

public boolean canCheckExitInvariant(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a invariant check at its exit point. Exit invariants may be checked for all methods except:

Returns:
true if the exit invariant should be checked.
See Also:
canCheckEntryInvariant(MethodGen)

canReferenceOld

public boolean canReferenceOld(org.apache.bcel.generic.MethodGen mg)
Determine if the postcondition for a non-contract method can refer to OLD. All postconditions are allowed to refer to the old state, except postconditions on: * The state is saved by calling clone() to make a copy of the object. Given this implementation, clone() itself if unable to refer to the old state.

Parameters:
mg - a non-contract method to examine.
Returns:
true if the m's postcondition is allowed to refer to OLD. False if the postcondition is not allowed to refer to OLD, or if the postcondition is not checkable.

isContractClass

public boolean isContractClass(org.apache.bcel.classfile.JavaClass javaclass)
Determine if a class defines contracts for another class. Such classes have names that end with "_CONTRACT" as in "MyClass_CONTRACT".

Parameters:
javaclass - a class to test.
Returns:
true if javaclass is a contract class.

isContractMethod

public boolean isContractMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a contract (precondition, postcondition, or invariant).

Parameters:
m - a method to test.
Returns:
true if m defines a contract.
See Also:
isPreconditionMethod(MethodGen), isPostconditionMethod(MethodGen), isInvariantMethod(MethodGen)

isPreconditionMethod

public boolean isPreconditionMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a precondition.

Parameters:
m - a method to test.
Returns:
true if m defines a precondition (m's name ends with "_Precondition").

isPostconditionMethod

public boolean isPostconditionMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a postcondition.

Parameters:
m - a method to test.
Returns:
true if m defines a postcondition (m's name ends with "_Postcondition").

isInvariantMethod

public boolean isInvariantMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a class invariant.

Parameters:
m - a method to test.
Returns:
true if m defines a class invariant (m's name is "_Invariant").
See Also:
isInvariantMethod(MethodGen)

getPreconditionMethodName

public java.lang.String getPreconditionMethodName(org.apache.bcel.generic.MethodGen method)
Get the name of the precondition method for a non-contract method. The precondition method name is determined by appending "_Precondition" to the method name. Constructors are a special case, because they are all named "". The precondition for a constructor is the class name with a "_Precondition" suffix.

Examples: 

   public class MyClass () {
     MyClass () { ... }
     boolean MyClass_Precondition () { ... }

     void foo () { ... }
     boolean foo_Precondition () { ... }
   }

Parameters:
method - a non-contract method. The name of the precondition method that goes with this method will be returned.
Returns:
the name of the precondition method that goes with method.
See Also:
getPreconditionMethodSignature(MethodGen)

getPreconditionMethodSignature

public java.lang.String getPreconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
Get the signature of the method that defines the precondition for a non-contract method. The argument list is same as the for the non-contract method, and the return type of the postcondition is boolean.

Examples: 

   public class MyClass () {
     MyClass () { ... }
     boolean MyClass_Precondition () { ... }

     MyClass (int x) { ... }
     boolean MyClass_Precondition (int x) { ... }

     void foo (Object o1, Object o2) { ... }
     boolean foo_Precondition (Object o1, Object o2) { ... }
   }
Signatures are returned in the format used by BCEL. Examples: 
   getPreconditionMethodSignature("MyClass()") --> "()Z"
   getPreconditionMethodSignature("MyClass(int)") --> "(I)Z"
   getPreconditionMethodSignature("foo(Object, Object")) -->
    "(Ljava/lang/Object;Ljava/lang/Object;)Z"

Returns:
the signature of the method that defines the postcondition for m.
See Also:
getPreconditionMethodName(MethodGen)

getPostconditionMethodName

public java.lang.String getPostconditionMethodName(org.apache.bcel.generic.MethodGen m)
Get the name of the postcondition method for a non-contract method. The postcondition method name is determined by appending "_Postcondition" to the method name. Constructors are a special case, because they are all named "". The postcondition for a constructor is the class name with a "_Precondition" suffix.

Examples: 

   public class MyClass () {
     MyClass () { ... }
     boolean MyClass_Postcondition (Void RESULT) { ... }

     int foo () { ... }
     boolean foo_Postcondition (int RESULT) { ... }
   }

Returns:
the name of the postcondition method that goes with method.
See Also:
getPostconditionMethodSignature(MethodGen)

getPostconditionMethodSignature

public java.lang.String getPostconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
Get the signature of the method that defines the postcondition for a non-contract method. The argument list for the postcondition method begins the same as the argument list for the non-contract method, but adds an argument of the method's return type to the end of the list. If the method returns void or is a constructor, then the last argument should be of type java.lang.Void. The return type of the postcondition is boolean.

Examples: 

   public class MyClass () {
     MyClass () { ... }
     boolean MyClass_Postcondition (Void RESULT) { ... }

     MyClass (int x) { ... }
     boolean MyClass_Postcondition (int x, Void RESULT) { ... }

     int foo (Object o1, Object o2) { ... }
     boolean foo_Precondition (Object o1, Object o2, int RESULT) { ... }
   }
Signatures are returned in the format used by BCEL. Examples: 
   getPostconditionMethodSignature("MyClass()") --> "(Ljava/lang/Void;)Z"
   getPostconditionMethodSignature("MyClass(int)") --> "(ILjava/lang/Void;)Z"
   getPostconditionMethodSignature("foo(Object, Object")) --gt;
    "(Ljava/lang/Object;Ljava/lang/Object;I)Z"

Returns:
the signature of the method that defines the postcondition for m.
See Also:
getPostconditionMethodName(MethodGen)

getInvariantMethodName

public java.lang.String getInvariantMethodName(org.apache.bcel.classfile.JavaClass javaclass)
Get the name of the invariant method for a class. The invariant method is always called "_Invariant".

Parameters:
javaclass - the class to get the invariant method name for. This argument is not actually used, because all invariant methods have the same name, but should be included in case things change in the future.
Returns:
the name of the invariant method, "_Invariant".

getInvariantMethodSignature

public java.lang.String getInvariantMethodSignature(org.apache.bcel.classfile.JavaClass javaclass)
Get the signature of the invariant method for a class. The signature is that of a method that takes no arguments and returns a boolean.

Parameters:
javaclass - the class to get the invariant method signature for. This argument is not actually used, because all invariant methods have the same signature, but should be included in case things change in the future.
Returns:
the signature of the invariant method, "()Z".

getContractClassName

public java.lang.String getContractClassName(org.apache.bcel.classfile.JavaClass javaclass)
Get the name of the external contract class that cooresponds to the given class. The contract class has the same name as the non-contract class, with a "_CONTRACT" suffix. Examples: 
   class MyClass { ... }
   class MyClass_CONTRACT { ... }

   class Foo extends MyClass { ... }
   class Foo_CONTRACT { ... }

Parameters:
javaclass - the class whose contract class name is to be determined.
Returns:
the name of the contract class that defines contracts for javaclass.

getContractClassName

public java.lang.String getContractClassName(java.lang.String classname)
Get the name of the external contract class that cooresponds to the given class name. The contract class has the same name as the non-contract class, with a "_CONTRACT" suffix. Examples: 
   class MyClass { ... }
   class MyClass_CONTRACT { ... }

   class Foo extends MyClass { ... }
   class Foo_CONTRACT { ... }

Parameters:
classname - the name of the class class whose contract class name is to be determined.
Returns:
the name of the contract class that defines contracts for the class named classname.
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD