edu.ucsb.ccs.jcontractor.transformation
Class PreconditionCheckTransformation

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.PreconditionCheckTransformation

public class PreconditionCheckTransformation

extends ContractCheckTransformation

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

Version:

$Id: PreconditionCheckTransformation.java,v 1.9 2002/05/12 00:09:16 parkera Exp $

Author:

Parker Abercrombie

See Also:

ContractCheckTransformation

Constructor Summary

PreconditionCheckTransformation()

Method Summary

void	transformMethod(org.apache.bcel.generic.MethodGen mg) Insert code to check the precondition of a method, and throw a PreconditionViolationError 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

PreconditionCheckTransformation

public PreconditionCheckTransformation()

Method Detail

transformMethod

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

Insert code to check the precondition of a method, and throw a PreconditionViolationError if it fails. This method assumes that a precondition method exists for the method being transformed. (PreconditionMethodTransformation should have been run to ensure this.)

Overrides:

transformMethod in class Transformation

Parameters:

mg - the method to transform. Has no effect if mg cannot have a precondition check.

See Also:

ContractTransformation.canCheckPrecondition(MethodGen)