edu.ucsb.ccs.jcontractor.transformation
Class InvariantCheckTransformation

java.lang.Object
  |
  +--edu.ucsb.ccs.jcontractor.transformation.Transformation
        |
        +--edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
              |
              +--edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation
                    |
                    +--edu.ucsb.ccs.jcontractor.transformation.InvariantCheckTransformation

public class InvariantCheckTransformation

extends ContractCheckTransformation

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

Version:

$Id: InvariantCheckTransformation.java,v 1.7 2002/05/22 06:29:12 parkera Exp $

Author:

Parker Abercrombie

See Also:

ContractCheckTransformation

Constructor Summary

InvariantCheckTransformation()

Method Summary

void	transformMethod(org.apache.bcel.generic.MethodGen mg) Insert code to check the invariant of a method, and throw an InvariantViolationError if it fails.

Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractCheckTransformation

acceptClass, createPushExceptionMessage, transformClass

Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation

canCheckEntryInvariant, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInvariant, canHavePostcondition, canHavePrecondition, canReferenceOld, contractsCheckable, getContractClassName, getContractClassName, getInvariantMethodName, getInvariantMethodSignature, getPostconditionMethodName, getPostconditionMethodSignature, getPreconditionMethodName, getPreconditionMethodSignature, isContractClass, isContractMethod, isInvariantMethod, isPostconditionMethod, isPreconditionMethod

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

InvariantCheckTransformation

public InvariantCheckTransformation()

Method Detail

transformMethod

public void transformMethod(org.apache.bcel.generic.MethodGen mg)

Insert code to check the invariant of a method, and throw an InvariantViolationError if it fails. This method assumes that an invariant method exists in this class. (InvariantMethodTransformation should have been run on the method to ensure this.)

Overrides:

transformMethod in class Transformation

Parameters:

mg - the method to transform. Has no effect if mg cannot have an invariant check. If the invariant can be checked at exit, but not entry, then code is inserted to do just that.