edu.ucsb.ccs.jcontractor.transformation
Class PostconditionCheckTransformation

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

public class PostconditionCheckTransformation

extends ContractCheckTransformation

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

Version:

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

Author:

Parker Abercrombie

See Also:

ContractCheckTransformation

Constructor Summary

PostconditionCheckTransformation()

Method Summary

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

PostconditionCheckTransformation

public PostconditionCheckTransformation()

Method Detail

transformMethod

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

Insert code to check the postcondition of a method, and throw a PostconditionViolationError if it fails. This method assumes that a postcondition method exists for the method being transformed. (PostconditionMethodTransformation 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 the mg cannot have a postcondition check.

See Also:

ContractTransformation.canCheckPostcondition(MethodGen)