de.uka.ilkd.key.symbolic_execution.po

Class TruthValuePOExtension

java.lang.Object

de.uka.ilkd.key.symbolic_execution.po.TruthValuePOExtension

All Implemented Interfaces:

POExtension

public class TruthValuePOExtension
extends java.lang.Object
implements POExtension

Implementation of POExtension to support truth value evaluation.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
TruthValuePOExtension()

Method Summary

Modifier and Type	Method and Description
boolean	isPOSupported(ProofOblInput po) Checks if the given ProofOblInput is supported.
protected Term	labelPostTerm(Services services, Term term) Labels all predicates in the given Term and its children with a FormulaTermLabel.
Term	modifyPostTerm(InitConfig proofConfig, Services services, Term postTerm) Modifies the post condition.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TruthValuePOExtension

public TruthValuePOExtension()

Method Detail

isPOSupported

public boolean isPOSupported(ProofOblInput po)

Checks if the given ProofOblInput is supported.

Specified by:

isPOSupported in interface POExtension

Parameters:

po - The ProofOblInput to check.

Returns:

true is supported, false is not supported.

modifyPostTerm

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

Modifies the post condition.

Specified by:

modifyPostTerm in interface POExtension

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.

labelPostTerm

protected Term labelPostTerm(Services services,
                             Term term)

Labels all predicates in the given Term and its children with a FormulaTermLabel.

Parameters:

services - The Services to use.

term - The Term to label.

Returns:

The labeled Term.