de.uka.ilkd.key.proof.init

Interface POExtension

All Known Implementing Classes:

TruthValuePOExtension

public interface POExtension

Instances of this interface are used to customize and extend the behavior of a ProofOblInput.

Implementations are instantiated once via ProofInitServiceUtil#createOperationPOExtension(ProofOblInput) and reused all the time. This means that POExtension are singletons and should not have a state.

Author:

Martin Hentschel

Method Summary

Modifier and Type	Method and Description
boolean	isPOSupported(ProofOblInput po) Checks if the given ProofOblInput is supported.
Term	modifyPostTerm(InitConfig proofConfig, Services services, Term postTerm) Modifies the post condition.

Method Detail

isPOSupported

boolean isPOSupported(ProofOblInput po)

Checks if the given ProofOblInput is supported.

Parameters:

po - The ProofOblInput to check.

Returns:

true is supported, false is not supported.

modifyPostTerm

Term modifyPostTerm(InitConfig proofConfig,
                    Services services,
                    Term postTerm)

Modifies the post condition.

Parameters:

proofConfig - The InitConfig to use.

services - The Services to use.

postTerm - The post condition to modify.

Returns:

The modified post condition or the original post condition if no modifications were performed.