All Packages from edu.ucsb.ccs.jaqual.* to edu.ucsb.ccs.jcontractor.*

Home >> All >> edu >> ucsb >> ccs

•

Package Samples:

• edu.ucsb.ccs.jcontractor.test: This is the main package of the jContractor system.
• edu.ucsb.ccs.jaqual.standard: This is the main package of the JaQuaL library.
• edu.ucsb.ccs.jaqual.test
• edu.ucsb.ccs.jaqual
• edu.ucsb.ccs.jbcd.transformation
• edu.ucsb.ccs.jbcd
• edu.ucsb.ccs.jcontractor.transformation
• edu.ucsb.ccs.jcontractor.extras
• edu.ucsb.ccs.jcontractor.examples.list
• edu.ucsb.ccs.jcontractor.examples.wordcount
• edu.ucsb.ccs.jcontractor.examples.heap
• edu.ucsb.ccs.jcontractor

Classes:

• ContractCheckTransformation: A transformation to insert a call to the contract method into a non-contract method. The details of inserting the check are left to descendents (whether to insert the check at the beginning or end of the method, for example). This class defines the buildContractCheck(MethodGen, MethodGen, InstructionList, String, String) method, that creates an instruction list that will call a contract method, and throw an exception if the method returns false. The Assertion Evaluation Rule states that when a function is called while evaluating a contract, the contracts of that function should not be evaluated. ...
• jContractorRuntime: This class is used internally by jContractor, and should never be used by others. This class is used to maintain state information while contracts are checked. In particular, it keeps track of which threads are evaluating contracts so that the assertion evaluation rule can be implemented. It also provides a mechanism for storing cloned objects to check OLD references. One final implementation note: jContractorRuntime is a "magic" class in the jContractor system. Because contract checking code calls the methods of this class, this class cannot have contracts of its own. If it did, then they would ...
• jInstrument: Utility to read in class files and instrument class methods to enforce jContractor contracts. Instrumented class files are written to a destination directory which defaults to the current working directory. The program may be run from the command line by passing the names of files to instrument as arguments, or by invoking the instrumentClassFile(String) method. If specified, the instrumentation file controls the instrumentation level of each class in the system. The available instrumentation levels are: None - No contracts checked. Pre - Preconditions checked. Post - Preconditions and postconditions ...
• jInstrumentTask: Ant task definition for jInstrument. Parameters: Attribute Description Required --------- ----------- -------- none A package that is not to be no instrumented. (Nested element.) pre A package to be instrumented with no precondition checks. (Nested element.) post A package to be instrumented with no pre and postcondition checks. (Nested element.) all A package to be instrumented with no all checks (pre, post, invariant). (Nested element.) srcdir A directory containing Java class yes files to instrument. All classes in this directory and all subdirectories will be processed. destdir The directory ...
• jContractor: Main entry point into the jContractor system. This class can be run stand alone to run another program with contract checking enabled. jContractor will substitute its own class loader for the default class loader, and modify the bytecode of loaded classes to enforce contracts at runtime. The runInstrumented(String, String []) method may be used to programatically run a class with contracts enabled. If specified, the instrumentation file controls the instrumentation level of each class in the system. The available instrumentation levels are: None - No contracts checked. Pre - Preconditions checked. ...
• jContractorTask: Ant task definition for jContractor. This task accepts all the options that the Java task does. (Note, however, that jContractor has never been tested with a Jar, and probably wouldn't work in this case.) Parameters: Attribute Description Required --------- ----------- -------- none A package that is not to be no instrumented. (Nested element.) pre A package to be instrumented with no precondition checks. (Nested element.) post A package to be instrumented with no pre and postcondition checks. (Nested element.) all A package to be instrumented with no all checks (pre, post, invariant). (Nested ...
• PreconditionMethodTransformation: 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 ...
• 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. The transformation is only neccessary when an exit condition needs to be checked, so it only modifies methods for which either the postcondition or the exit invariant is checkable. The transformation also saves the method's return value to a local variable, and makes the index of this variable available to subsequent transformations (AppendReturnTransformation, in particular, needs it). The index is saved ...
• InstrumentationFilter: Interface for instrumentation filters, which control the level to which classes are instrumented. The available levels are none, pre, post, and all. An instrumentation filter is used to determine the level of processing given to each class that is instrumented. Often, several instrumentation filters will be combined, and will need to take precedence over others. For example, if one says that all classes in edu.ucsb.ccs.jcontractor are to be instrumented to the precondition level, and another filter says that edu.ucsb.ccs.jcontractor.jContractor is to be instrumented to the postcondition level, ...
• PostconditionMethodTransformation: 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 ...
• AppendReturnTransformation: A transformation to append code to load the method's result from a local variable, and return. This must be done after processing with ReplaceReturnInstructionTransformation. This transformation requires that ReplaceReturnInstructionTransformation has saved the method's return value to a local variable, and placed the index of this variable into the shared data table. This transformation is only required where ReplaceReturnInstructionTransformation is required, so it transforms only methods for which either the postcondition or exit invariant is checkable. Before: After: ----------- -------------- ...
• InvariantMethodTransformation: A transformation to prepare invariant methods. For each class, the transformation searches for an invariant method. The invariant method is modified to call the superclass invariant method before evaluation, and inlined version of invariants inherited from interfaces, and the external invariant defined in a contract class are added. All of these are logical and-ed, so that the invariant may be strengthened, but not weakened. If no invariant method was found, a default invariant method is added to the class. The invariant method in its final form looks something like this: return <interface1 ...
• PackageLevelInstrumentationFilter: An instrumentation filter that assigns instrumentation level by package (or class, if desired). The filter is given a package name, a class name, and an instrumentation level. The class name may be "*" to match any class in the package or a subpackage. Note that this differs a little from how Java import statements work. The filter level is how many levels down the package is, so "edu.*" has filter level 1, and "edu.ucsb.ccs.*" has filter level 3. This way, more specific filters override more general filters. To match classes in the default package, but no other packages, use the "magic" package ...
• PreconditionCheckTransformation: A transformation to insert code to check the precondition of each method by calling method_Precondition . This transformation requires that PreconditionMethodTransformation has already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. One note on constructors: Because call to the super class constructor is required to be the first statement of the constructor, preconditions are checked immediatly after the super class constructor call, not at method entry. This transformation depends on: PreconditionMethodTransformation
• LockCloneTransformation: Transformation to disable contract checking while in the clone() method. clone() is used to implement OLD references, and checking contracts on method called from clone() could require more calls to clone() . This leads to infinite recursion, which would be bad. To prevent this scenario, jContractor does not check contracts on any methods called from clone() . Note: Strictly speaking, all that is required is to not check contracts that refer to OLD. However, just supressing all contract checks is much easier to implement.
• LoadContractClassTransformation: A transformation that loads the contract class for the transformed class into the Repository so that it will be available to subsequent transformations. The contract class has a "_CONTRACT" suffix (as in "MyClass" and "MyClass_CONTRACT"), and defines contracts for another class. Before inserting code to check the contracts, the contract class needs to be accessible in the Repository. This transformation should be run before transformations requiring access to the contract class. The transformation does not modify the current class or any of it's methods.
• InvariantCheckTransformation: A transformation to insert code to check the invariant of each method by calling _Invariant . This transformation requires that InvariantMethodTransformation and ReplaceReturnInstructionsTransformation have already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. In most methods, the invariant is checked at both entry and exit. This transformation depends on: InvariantMethodTransformation ReplaceReturnInstructionsTransformation
• ClassTransformer: A ClassTransformer executes a complex transformation on a JavaClass object. The complex transform is made up of simpler transforms that are carried out in sequence on the class itself and on each method. Transformations are stored as a list, and are executed in the order that they appear. The list may be modified with insert(Transformation) and append(Transformation) . Use the transform(JavaClass) method to apply the transformations to a class.
• PostconditionCheckTransformation: A transformation to insert code to check the postcondition of each method by calling method_Postcondition . This transformation requires that PostconditionMethodTransformation and ReplaceReturnInstructionsTransformation have already been run. The contract check is built by ContractCheckTransformation. See that class for all the gory details. This transformation depends on: PreconditionMethodTransformation ReplaceReturnInstructionsTransformation
• ClassTransformer: A ClassTransformer executes a complex transformation on a JavaClass object. The complex transform is made up of simpler transforms that are carried out in sequence on the class itself and on each method. Transformations are stored as a list, and are executed in the order that they appear. The list may be modified with insert(Transformation) and append(Transformation) . Use the transform(JavaClass) method to apply the transformations to a class.
• ContractTransformation: 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.
• ContractMethodTransformation: Superclass for transformations that modify contract methods. Contract methods need to be modified to check superclass contracts, external contracts, and contracts inherited from interfaces. This class provides methods to check these contracts, and to combine contract checks by and-ing or or-ing them together. This transformation depends on: LoadContractClassTransformation
• Assertion: Abstract description of an assertion that can be evaluated on an element of a collection. Assertions can be (fairly) easily defined inline using anonymous classes: // Make sure that Vector `v' contains only Integers. ForAll.in(collection).ensure(new Assertion() { public boolean eval(Object o) { return (o instanceof Integer); } });
• ReplaceOldReferencesTransformation: Transformation to replace references to OLD in postconditions. The old state is saved on a stack in jContractorRuntime, so the postcondition needs to pop the saved state, and store it to a local variable (storing to the OLD instance variable wouldn't be thread safe). Each reference to the OLD instance variable needs to be changed to a reference to the local variable.
• Operator: Interface for an object that transforms other objects. Using the ForAll quantifier, Operators allow you to easily apply some function to all the elements in a Collection. Operators are similar to Assertions, but an Assertion simply evaluates to a boolean leaving it's argument unchanged. An Operator performs some operation on the argument.

Home | Contact Us | Privacy Policy | Terms of Service