A C E F G I J L M N O P R S T U V

A

AbortTransformationException - exception edu.ucsb.ccs.jcontractor.transformation.AbortTransformationException.

An exception that will be thrown by a Transformation when an error occurs that requires that the ClassTransformer abort all subsequent transformations.

AbortTransformationException(String) - Constructor for class edu.ucsb.ccs.jcontractor.transformation.AbortTransformationException

Create a new exception with the specified error message.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.RemoveContractMethodsTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.InstrumentedFlagTransformation

Determine if this transform should be applied to a class.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.LockCloneTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.LoadContractClassTransformation

Determine if the current class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.MarkInstrumentedTransformation

Determine if this transform should be applied to a class.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation

Determine if a class should be transformed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation

Determine if a class should be processed.

acceptClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation

Determine if the current class should be processed.

addFilter(InstrumentationFilter) - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Add a filter to the composite filter.

ALL - Static variable in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Instrumentation level for checking all contracts: preconditions, postconditions, and invariants.

append(Transformation) - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Add a Transformation at the end of the transformation list.

AppendReturnTransformation - class edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation.

A transformation to append code to load the method's result from a local variable, and return.

AppendReturnTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation

appliesTo(String) - Method in class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter

Always returns true, this filter applies to all classes.

appliesTo(String) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Determine if this filter applies to a given class.

appliesTo(String) - Method in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Determine if this filter applies to a given class.

appliesTo(String) - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Always returns true.

Assertion - interface edu.ucsb.ccs.jaqual.Assertion.

Abstract description of an assertion that can be evaluated on an element of a collection.

C

canCheckAssertion() - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

Determine if the current thread can evaluate an assertion.

canCheckEntryInvariant(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method should have a invariant check at its entry point.

canCheckExitInvariant(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method should have a invariant check at its exit point.

canCheckPostcondition(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method should have a postcondition check.

canCheckPrecondition(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method should have a precondition check.

canHaveInvariant(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not a class can have an invariant.

canHavePostcondition(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method can have a postcondition, taking instrumentation level into account.

canHavePrecondition(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not this method can have a precondition, taking instrumentation level into account.

canReferenceOld(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if the postcondition for a non-contract method can refer to OLD.

checkpoint() - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

classpath - Static variable in class edu.ucsb.ccs.jcontractor.jContractorClassLoader

Shared reference to the class path;

ClassTransformer - class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer.

A ClassTransformer executes a complex transformation on a JavaClass object.

ClassTransformer(InstrumentationFilter) - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Create an empty ClassTransformer.

clearArgs() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Clear the arguments that will be passed to the task that jContractor invokes.

CompositeInstrumentationFilter - class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter.

An instrumentation filter that combines other instrumentation filters.

CompositeInstrumentationFilter() - Constructor for class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Create a new filter.

CONTENT - Static variable in class edu.ucsb.ccs.jaqual.standard.Equal

Constant for comparison by value.

ContractCheckTransformation - class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation.

A transformation to insert a call to the contract method into a non-contract method.

ContractCheckTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation

ContractMethodTransformation - class edu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation.

Superclass for transformations that modify contract methods.

ContractMethodTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ContractMethodTransformation

contractsCheckable(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine whether or not contracts should be checked on the methods in a class.

ContractTransformation - class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation.

Abstract super class for contract transformations.

ContractTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

createAll() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Create a <all package="..."/> tag.

createAll() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Create a <all package="..."/> tag.

createArg() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Creates a nested arg element.

createNone() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Create a <none package="..."/> tag.

createNone() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Create a <none package="..."/> tag.

createPost() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Create a <post package="..."/> tag.

createPost() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Create a <post package="..."/> tag.

createPre() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Create a <pre package="..."/> tag.

createPre() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Create a <pre package="..."/> tag.

createPushExceptionMessage(MethodGen, String) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation

Build an exception message string, and push it onto the stack.

E

edu.ucsb.ccs.jaqual - package edu.ucsb.ccs.jaqual

This is the main package of the JaQuaL library.

edu.ucsb.ccs.jaqual.standard - package edu.ucsb.ccs.jaqual.standard

This package defines several standard assertions to be used with the JaQuaL library.

edu.ucsb.ccs.jcontractor - package edu.ucsb.ccs.jcontractor

This is the main package of the jContractor system.

edu.ucsb.ccs.jcontractor.extras - package edu.ucsb.ccs.jcontractor.extras

This package provides a few extra programs and classes that go along with jContractor.

edu.ucsb.ccs.jcontractor.transformation - package edu.ucsb.ccs.jcontractor.transformation

This package defines a fairly generic framework for transforming Java bytecode, and specific transformations for jContractor.

Elements - class edu.ucsb.ccs.jaqual.Elements.

Quantifier to find a subset of a collection that matches certain criteria.

Elements(Collection) - Constructor for class edu.ucsb.ccs.jaqual.Elements

Create a new elements quantifier.

Elements(Object[]) - Constructor for class edu.ucsb.ccs.jaqual.Elements

Create a new Elements quantifier for an array.

ensure(Assertion) - Method in class edu.ucsb.ccs.jaqual.ForAll

Evaluate the quantifier on all objects in the collection.

Equal - class edu.ucsb.ccs.jaqual.standard.Equal.

An assertion to test for equality.

Equal(byte) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare bytes.

Equal(char) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare characters.

Equal(double) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare double precision numbers, using Double.MIN_VALUE as the tolerance.

Equal(double, double) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare double precision numbers.

Equal(float) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare floating point numbers, using Float.MIN_VALUE as the tolerance.

Equal(float, double) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare floating point numbers.

Equal(int) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare integers.

Equal(long) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare longs.

Equal(Object) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare Objects by content.

Equal(Object, int) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare Objects.

Equal(short) - Constructor for class edu.ucsb.ccs.jaqual.standard.Equal

Create an assertion to compare shorts.

eval(Object) - Method in interface edu.ucsb.ccs.jaqual.Assertion

Evaluate the assertion on an object.

eval(Object) - Method in class edu.ucsb.ccs.jaqual.standard.InstanceOf

Test an object to see if it is an instance of the target class.

eval(Object) - Method in class edu.ucsb.ccs.jaqual.standard.Equal

Test an object to see if it is equal to the target value.

eval(Object) - Method in class edu.ucsb.ccs.jaqual.standard.InRange

Determine if a value is in the allowed range.

eval(Object) - Method in class edu.ucsb.ccs.jaqual.standard.Not

Test an object by applying the inner assertion, and negating the result.

EXCLUSIVE - Static variable in class edu.ucsb.ccs.jaqual.standard.InRange

Constant to indicate the bound is exclusive.

execute() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Execute jInstrument to instrument each class file in the directory specified by srcdir.

execute() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Execute jContractor to instrument and run the class named classname, with the specified command line arguments.

execute(Object) - Method in interface edu.ucsb.ccs.jaqual.Operator

Execute the operator on an object.

execute(Operator) - Method in class edu.ucsb.ccs.jaqual.ForAll

Execute an operator on all objects in the collection.

Exists - class edu.ucsb.ccs.jaqual.Exists.

Exists quantifier.

Exists(Collection) - Constructor for class edu.ucsb.ccs.jaqual.Exists

Create a new Exists quantifier.

Exists(Object[]) - Constructor for class edu.ucsb.ccs.jaqual.Exists

Create a new Exists quantifier for an array.

F

ForAll - class edu.ucsb.ccs.jaqual.ForAll.

A forall quantifier.

ForAll(Collection) - Constructor for class edu.ucsb.ccs.jaqual.ForAll

Create a new ForAll quantifier.

ForAll(Object[]) - Constructor for class edu.ucsb.ccs.jaqual.ForAll

Create a new ForAll quantifier for an array.

G

getClassname() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Get the name of the class that jContractor will invoke.

getClassName() - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get the name of the class matched by this filter.

getConstantPoolGen() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the ConstantPoolGen object that is to be used to build the constant pool for the current class.

getContractClassName(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the name of the external contract class that cooresponds to the given class.

getContractClassName(String) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the name of the external contract class that cooresponds to the given class name.

getCurrentClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the class that the transformer is transforming.

getDestdir() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Get the destination directory of instrumented class files.

getDestination() - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Get the destination directory of files written by instrumentClassFile(String).

getFilter() - Method in class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Get a PackageLevelInstrumentationFilter with the criteria set in this wrapper.

getFilterLevel() - Method in class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter

Get the filter level.

getFilterLevel() - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get the level of this filter.

getFilterLevel() - Method in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Get the filter level of this filter.

getFilterLevel() - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Get the filter level; always returns zero.

getFilters() - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Get the filters in the composite filter as a linked list.

getInstructionFactory() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the instruction factory that should be used to create instructions.

getInstrumentationFilter() - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Get the instrumentation filter that determines which classes are instrumented and to what level.

getInstrumentationFilter() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the instrumentation filter that determines which classes are instrumented and to what level.

getInstrumentationLevel() - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get the instrumentation level assigned to classes that match the filter criteria.

getInstrumentationLevel() - Method in class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Get the instrumentation level assigned to classes that match the filter criteria.

getInstrumentationLevel(String) - Method in class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter

Get the instrumentation level for a class.

getInstrumentationLevel(String) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get the instrumentation level to assign to a class that matches the filter criteria.

getInstrumentationLevel(String) - Method in class edu.ucsb.ccs.jcontractor.InstrumentationFilter_CONTRACT

Dummy method implementation.

getInstrumentationLevel(String) - Method in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Get the instrumentation level for a class.

getInstrumentationLevel(String) - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Get the instrumentation level for a class.

getInvariantMethodName(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the name of the invariant method for a class.

getInvariantMethodSignature(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the signature of the invariant method for a class.

getMethod(String, String) - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Retrieve a method from the set.

getMethodSet() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the method set that holds working copies of the methods in the current class.

getPackage() - Method in class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Get the filter's package attribute.

getPackageName() - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get the name of the package matched by this filter.

getPostconditionMethodName(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the name of the postcondition method for a non-contract method.

getPostconditionMethodSignature(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the signature of the method that defines the postcondition for a non-contract method.

getPreconditionMethodName(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the name of the precondition method for a non-contract method.

getPreconditionMethodSignature(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Get the signature of the method that defines the precondition for a non-contract method.

getSharedInfo() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the shared data table.

getSrcdir() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Get the source directory.

getStrip() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Get the value of the strip mode flag.

getTransformer() - Method in class edu.ucsb.ccs.jcontractor.transformation.Transformation

Get the transformer to which this transformation belongs.

getVerbose() - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Get the value of the verbose flag.

getVerbose() - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Get the value of the verbose flag.

getVerbose() - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Get the value of the verbose flag.

I

implies(boolean, boolean) - Static method in class edu.ucsb.ccs.jcontractor.jContractor

Deprecated. Use edu.ucsb.ccs.jaqual.Logical.implies instead.

implies(boolean, boolean) - Static method in class edu.ucsb.ccs.jaqual.Logical

Implication operator.

in(Collection) - Static method in class edu.ucsb.ccs.jaqual.ForAll

Create a new ForAll quantifier.

in(Collection) - Static method in class edu.ucsb.ccs.jaqual.Exists

Create a new Exists quantifier.

in(Collection) - Static method in class edu.ucsb.ccs.jaqual.Elements

Create a new elements quantifier.

INCLUSIVE - Static variable in class edu.ucsb.ccs.jaqual.standard.InRange

Constant to indicate the bound is inclusive.

InRange - class edu.ucsb.ccs.jaqual.standard.InRange.

An assertion to determine if a number falls in a given range.

InRange(double, double, double) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls in the interval [minVal, maxVal].

InRange(double, double, double, int) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls in the interval [minVal, maxVal].

InRange(double, double, double, int, int) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls in the interval [minVal, maxVal].

InRange(long, long) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls in the interval [minVal, maxVal].

InRange(long, long, int) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls between `minVal' and `maxVal'.

InRange(long, long, int, int) - Constructor for class edu.ucsb.ccs.jaqual.standard.InRange

Create an assertion to test that a value falls between `minVal' and `maxVal'.

insert(Transformation) - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Insert a transformation at the beginning of the list.

InstanceOf - class edu.ucsb.ccs.jaqual.standard.InstanceOf.

Assertion to check if an object is an instance of a certain class type.

InstanceOf(Class) - Constructor for class edu.ucsb.ccs.jaqual.standard.InstanceOf

Create a new assertion.

InstrumentationException - exception edu.ucsb.ccs.jcontractor.InstrumentationException.

An exception that is thrown by jInstrument if it is unable to instrument a class.

InstrumentationException(String) - Constructor for class edu.ucsb.ccs.jcontractor.InstrumentationException

InstrumentationFilter - interface edu.ucsb.ccs.jcontractor.InstrumentationFilter.

Interface for instrumentation filters, which control the level to which classes are instrumented.

InstrumentationFilter_CONTRACT - class edu.ucsb.ccs.jcontractor.InstrumentationFilter_CONTRACT.

Contract class for InstrumentationFilter.

InstrumentationFilter_CONTRACT() - Constructor for class edu.ucsb.ccs.jcontractor.InstrumentationFilter_CONTRACT

instrumentClass(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Instrument a class to enforce jContractor contracts.

instrumentClassFile(String) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Instrument a class file to enforce jContractor contracts, and write the instrumented file to the directory specified by destination.

InstrumentedFlagTransformation - class edu.ucsb.ccs.jcontractor.transformation.InstrumentedFlagTransformation.

A transformation to insert a flag constant into the constant pool of a class to mark the class as instrumented.

InstrumentedFlagTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.InstrumentedFlagTransformation

InvariantCheckTransformation - class edu.ucsb.ccs.jcontractor.transformation.InvariantCheckTransformation.

A transformation to insert code to check the invariant of each method by calling _Invariant.

InvariantCheckTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.InvariantCheckTransformation

InvariantMethodTransformation - class edu.ucsb.ccs.jcontractor.transformation.InvariantMethodTransformation.

A transformation to prepare invariant methods.

InvariantMethodTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.InvariantMethodTransformation

InvariantViolationError - error edu.ucsb.ccs.jcontractor.InvariantViolationError.

An error that will be thrown when a class invariant is violated.

InvariantViolationError(String) - Constructor for class edu.ucsb.ccs.jcontractor.InvariantViolationError

Construction a new exception with an informative message to tell what went wrong.

isContractClass(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if a class defines contracts for another class.

isContractMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if a method defines a contract (precondition, postcondition, or invariant).

isInstrumented(JavaClass) - Static method in class edu.ucsb.ccs.jcontractor.jInstrument

Determine if a class has been instrumented.

isInvariantMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if a method defines a class invariant.

isPostconditionMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if a method defines a postcondition.

isPreconditionMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

Determine if a method defines a precondition.

J

jContractor - class edu.ucsb.ccs.jcontractor.jContractor.

Main entry point into the jContractor system.

JCONTRACTOR_FLAG_CONSTANT - Static variable in class edu.ucsb.ccs.jcontractor.jInstrument

The prefix of a constant that will be inserted into the constant pool of classes that jInstrument instruments to mark them as instrumented.

jContractor() - Constructor for class edu.ucsb.ccs.jcontractor.jContractor

jContractorClassLoader - class edu.ucsb.ccs.jcontractor.jContractorClassLoader.

A class loader than uses jInstrument to instrument classes are they are loaded.

jContractorClassLoader() - Constructor for class edu.ucsb.ccs.jcontractor.jContractorClassLoader

Create a new class loader with a default instance of jInstrument.

jContractorClassLoader(jInstrument) - Constructor for class edu.ucsb.ccs.jcontractor.jContractorClassLoader

Create a class loader using the specified jInstrument to instrument classes.

jContractorRuntime - class edu.ucsb.ccs.jcontractor.jContractorRuntime.

This class is used internally by jContractor, and should never be used by others.

jContractorRuntime() - Constructor for class edu.ucsb.ccs.jcontractor.jContractorRuntime

jContractorTask - class edu.ucsb.ccs.jcontractor.extras.jContractorTask.

Ant task definition for jContractor.

jContractorTask() - Constructor for class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Create a new jContractorTask.

jInstrument - class edu.ucsb.ccs.jcontractor.jInstrument.

Utility to read in class files and instrument class methods to enforce jContractor contracts.

jInstrument() - Constructor for class edu.ucsb.ccs.jcontractor.jInstrument

Create a default instance that will check all contracts on all classes, in non-verbose mode.

jInstrumentTask - class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask.

Ant task definition for jInstrument.

jInstrumentTask() - Constructor for class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Create a new jInstrumentTask.

L

LoadContractClassTransformation - class edu.ucsb.ccs.jcontractor.transformation.LoadContractClassTransformation.

A transformation that loads the contract class for the transformed class into the Repository so that it will be available to subsequent transformations.

LoadContractClassTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.LoadContractClassTransformation

lockAssertionCheck() - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

Lock assertion checking for the current thread.

LockCloneTransformation - class edu.ucsb.ccs.jcontractor.transformation.LockCloneTransformation.

Transformation to disable contract checking while in the clone() method.

LockCloneTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.LockCloneTransformation

Logical - class edu.ucsb.ccs.jaqual.Logical.

This class defines some useful logic operators.

Logical() - Constructor for class edu.ucsb.ccs.jaqual.Logical

M

main(String[]) - Static method in class edu.ucsb.ccs.jcontractor.jInstrument

Instrument all the classes specified on the command line.

main(String[]) - Static method in class edu.ucsb.ccs.jcontractor.jContractor

Main entry point to the application.

MarkInstrumentedTransformation - class edu.ucsb.ccs.jcontractor.transformation.MarkInstrumentedTransformation.

A transformation to insert a flag constant into the constant pool of a class to mark the class as instrumented.

MarkInstrumentedTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.MarkInstrumentedTransformation

MethodSet - class edu.ucsb.ccs.jcontractor.transformation.MethodSet.

A simple container to hold MethodGen objects.

MethodSet() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Create an empty method set.

N

NONE - Static variable in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Instrumentation level constant for no instrumentation at all.

Not - class edu.ucsb.ccs.jaqual.standard.Not.

Assertion that negates another assertion.

Not(Assertion) - Constructor for class edu.ucsb.ccs.jaqual.standard.Not

Create a new assertion.

O

Operator - interface edu.ucsb.ccs.jaqual.Operator.

Interface for an object that transforms other objects.

P

PackageLevelInstrumentationFilter - class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter.

An instrumentation filter that assigns instrumentation level by package (or class, if desired).

PackageLevelInstrumentationFilter(String, int) - Constructor for class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Create a filter from a class and package string.

PackageLevelInstrumentationFilter(String, String, int) - Constructor for class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Create a new filter.

PackageLevelInstrumentationFilterType - class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType.

A type for Ant that wraps PackageLevelInstrumentationFilter.

PackageLevelInstrumentationFilterType(String, int) - Constructor for class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Create a wrapper for a filter with the specified criteria.

parseInstrumentationFile(String, CompositeInstrumentationFilter) - Static method in class edu.ucsb.ccs.jcontractor.jInstrument

Parse an instrumentation file.

parseInstrumentationList(String, int, CompositeInstrumentationFilter) - Static method in class edu.ucsb.ccs.jcontractor.jInstrument

Parse a comma separated list of packages to instrument and create instrumentation filters.

popState() - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

Recall the last saved state for a thread of execution.

POST - Static variable in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Instrumentation level for checking preconditions and postconditions.

PostconditionCheckTransformation - class edu.ucsb.ccs.jcontractor.transformation.PostconditionCheckTransformation.

A transformation to insert code to check the postcondition of each method by calling method_Postcondition.

PostconditionCheckTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.PostconditionCheckTransformation

PostconditionMethodTransformation - class edu.ucsb.ccs.jcontractor.transformation.PostconditionMethodTransformation.

A transformation to prepare postcondition methods.

PostconditionMethodTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.PostconditionMethodTransformation

PostconditionViolationError - error edu.ucsb.ccs.jcontractor.PostconditionViolationError.

An error that will be thrown when a postcondition is violated.

PostconditionViolationError(String) - Constructor for class edu.ucsb.ccs.jcontractor.PostconditionViolationError

Construction a new error with an informative message to tell what went wrong.

PRE - Static variable in interface edu.ucsb.ccs.jcontractor.InstrumentationFilter

Instrumentation level for checking preconditions only.

PreconditionCheckTransformation - class edu.ucsb.ccs.jcontractor.transformation.PreconditionCheckTransformation.

A transformation to insert code to check the precondition of each method by calling method_Precondition.

PreconditionCheckTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.PreconditionCheckTransformation

PreconditionMethodTransformation - class edu.ucsb.ccs.jcontractor.transformation.PreconditionMethodTransformation.

A transformation to prepare precondition methods.

PreconditionMethodTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.PreconditionMethodTransformation

PreconditionViolationError - error edu.ucsb.ccs.jcontractor.PreconditionViolationError.

An error that will be thrown when a precondition is violated.

PreconditionViolationError(String) - Constructor for class edu.ucsb.ccs.jcontractor.PreconditionViolationError

Construction a new error with an informative message to tell what went wrong.

pushState(Object) - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

Save the state of an object for retrieval later.

putMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Put a method into the set.

R

REFERENCE - Static variable in class edu.ucsb.ccs.jaqual.standard.Equal

Constant for comparison by reference.

releaseAssertionCheck() - Static method in class edu.ucsb.ccs.jcontractor.jContractorRuntime

Release the assertion checking lock for the current thread.

RemoveContractMethodsTransformation - class edu.ucsb.ccs.jcontractor.transformation.RemoveContractMethodsTransformation.

Transformation to remove the contract methods from a class, to decrease the size of the bytecode.

RemoveContractMethodsTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.RemoveContractMethodsTransformation

removeMethod(String, String) - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Remove a method from the set.

ReplaceOldReferencesTransformation - class edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation.

Transformation to replace references to OLD in postconditions.

ReplaceOldReferencesTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

ReplaceReturnInstructionsTransformation - class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation.

A transformation to replace all the return statements in a non-contract methods with a jump to the end of the method, so that exit condition checking code may be appended to the instruction list.

ReplaceReturnInstructionsTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation

runInstrumented(String, String[]) - Static method in class edu.ucsb.ccs.jcontractor.jContractor

Run a class with contracts enabled.

runInstrumented(String, String[], jInstrument) - Static method in class edu.ucsb.ccs.jcontractor.jContractor

Run a class with contracts enabled, using the specified instance of jInstrument.

S

SaveOldStateTransformation - class edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation.

This transformation adds code to postconditions that refer to old to call to clone an object, and push the clone onto the stack of saved instances in jContractorRuntime.

SaveOldStateTransformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation

setArgs(String) - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Set the arguments that will be passed to the class that jContractor invokes.

setClassname(String) - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Set the name of the class that jContractor will invoke.

setClassName(String) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Set the name of the class matched by this filter.

setDestdir(String) - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Set the destination directory of instrumented class files.

setDestination_Precondition(String, Void) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

setDestination(String) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Set the destination directory of files written by instrumentClassFile(String).

setInstructionFactory(InstructionFactory) - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Set the instruction factory to be used to create bytecode for the current class.

setInstrumentationFilter(InstrumentationFilter) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Set the instrumentation filter that determines which classes are instrumented and to what level.

setInstrumentationFilter(InstrumentationFilter) - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Set the instrumentation filter that determines which classes are instrumented and to what level.

setInstrumentationLevel(int) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Set the instrumentation level assigned to classes that match the filter criteria.

setInstrumentationLevel(int) - Method in class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Set the instrumentation level assigned to classes that match the filter criteria.

setPackage(String) - Method in class edu.ucsb.ccs.jcontractor.extras.PackageLevelInstrumentationFilterType

Set the filter's package attribute.

setPackageAndClass(String) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Set the package and class from a full class name (including package).

setPackageName(String) - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Set the name of the package to match.

setSrcdir(Path) - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Set the source directory.

setStrip(boolean) - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Set the value of the strip mode flag.

setTransformer(ClassTransformer) - Method in class edu.ucsb.ccs.jcontractor.transformation.Transformation

Set the transformer to which the transformation belongs.

setVerbose(boolean) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Set the value of the verbose flag.

setVerbose(boolean) - Method in class edu.ucsb.ccs.jcontractor.extras.jInstrumentTask

Set the verbose flag.

setVerbose(boolean) - Method in class edu.ucsb.ccs.jcontractor.extras.jContractorTask

Set the verbose flag.

SHARED_INFO_RESULT_INDEX_KEY - Static variable in class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation

Constant for the key with which the result index is saved in the shared data.

SimpleInstrumentationFilter - class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter.

An instrumentation filter that assign the same instrumentation level to all classes.

SimpleInstrumentationFilter(int) - Constructor for class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter

Create a filter to assign the given instrumentation level.

size() - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Get the number of filters in this composite filter.

size() - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Get the number of methods in the set.

size() - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Get the number of transformations in the transformer.

stripContracts(String) - Method in class edu.ucsb.ccs.jcontractor.jInstrument

Remove contract methods from a class file, to decrease the file size.

suchThat(Assertion) - Method in class edu.ucsb.ccs.jaqual.Exists

Evaluate the quantifier on all objects in the collection.

suchThat(Assertion) - Method in class edu.ucsb.ccs.jaqual.Elements

Find the subset of the collection that meets a given assertion.

T

toArray() - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Get an array representation of the methods in the set.

toString() - Method in class edu.ucsb.ccs.jcontractor.SimpleInstrumentationFilter

Get a string representation of the filter, for debugging.

toString() - Method in class edu.ucsb.ccs.jcontractor.PackageLevelInstrumentationFilter

Get a string representation of the filter, for debugging.

toString() - Method in class edu.ucsb.ccs.jcontractor.CompositeInstrumentationFilter

Get a string representation of the filter, for debugging.

toString() - Method in class edu.ucsb.ccs.jcontractor.transformation.MethodSet

Get a string representation of the method set.

transform() - Method in class edu.ucsb.ccs.jcontractor.transformation.Transformation

Apply the transformation to the current class (as determined by getTransformer().getCurrentClass()).

transform(JavaClass) - Method in class edu.ucsb.ccs.jcontractor.transformation.ClassTransformer

Transform a class.

Transformation - class edu.ucsb.ccs.jcontractor.transformation.Transformation.

Abstract description of a transformation that can be applied to a class.

Transformation() - Constructor for class edu.ucsb.ccs.jcontractor.transformation.Transformation

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.RemoveContractMethodsTransformation

Remove the contract methods from a class.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.InstrumentedFlagTransformation

Insert the flag constant into the constant pool.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.LockCloneTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation

Make sure that the class is valid, as regards it's OLD field.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.PreconditionMethodTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.PostconditionMethodTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.LoadContractClassTransformation

Load the contract class that goes with the current class into the Repository.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.InvariantMethodTransformation

Prepare the invariant method for the current class.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.MarkInstrumentedTransformation

Insert the flag constant into the constant pool.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation

Does nothing.

transformClass() - Method in class edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.RemoveContractMethodsTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.InstrumentedFlagTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.LockCloneTransformation

Add code to a clone() method that will suppress contract checks inside the method.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation

Add jContractorRuntime.pushState(clone()) at the beginning of the postcondition that cooresponds to mg.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceReturnInstructionsTransformation

Replace all the return statements in the method with code a jump the end of the method.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

Replace references to OLD in a postcondition method.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.PreconditionMethodTransformation

Prepare the precondition method for a normal method.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.PreconditionCheckTransformation

Insert code to check the precondition of a method, and throw a PreconditionViolationError if it fails.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.PostconditionMethodTransformation

Prepare the postcondition method for a non-contract method.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.PostconditionCheckTransformation

Insert code to check the postcondition of a method, and throw a PostconditionViolationError if it fails.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.LoadContractClassTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.InvariantMethodTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.InvariantCheckTransformation

Insert code to check the invariant of a method, and throw an InvariantViolationError if it fails.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.MarkInstrumentedTransformation

Does nothing.

transformMethod(MethodGen) - Method in class edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation

Append code to load the method's return value from a local variable and return.

U

USAGE_MESSAGE - Static variable in class edu.ucsb.ccs.jcontractor.jInstrument

Usage message to be printed if the command line arguments do not match the specification.

USAGE_MESSAGE - Static variable in class edu.ucsb.ccs.jcontractor.jContractor

Usage message to be printed if the command line arguments do not match the specification.

V

VERSION - Static variable in class edu.ucsb.ccs.jcontractor.jInstrument

Constant for the version number that is printed when the --version command line argument is given.

VERSION - Static variable in class edu.ucsb.ccs.jcontractor.jContractor

Constant for the version number that is printed when the --version command line argument is given.

A C E F G I J L M N O P R S T U V