de.uka.ilkd.key.rule

Class IfFormulaInstDirect

java.lang.Object

de.uka.ilkd.key.rule.IfFormulaInstDirect

All Implemented Interfaces:

IfFormulaInstantiation

public class IfFormulaInstDirect
extends java.lang.Object
implements IfFormulaInstantiation

Instantiation of an if-formula that has to be proven by an explicit if-goal

Field Summary

Fields

Modifier and Type	Field and Description
private SequentFormula	cf Simply the formula

Constructor Summary

Constructors

Constructor and Description
IfFormulaInstDirect(SequentFormula p_cf)

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object p_obj)
SequentFormula	getConstrainedFormula()
int	hashCode()
java.lang.String	toString()
java.lang.String	toString(Services services)

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

cf

private SequentFormula cf

Simply the formula

Constructor Detail

IfFormulaInstDirect

public IfFormulaInstDirect(SequentFormula p_cf)

Method Detail

getConstrainedFormula

public SequentFormula getConstrainedFormula()

Specified by:

getConstrainedFormula in interface IfFormulaInstantiation

Returns:

the cf this is pointing to

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object p_obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString(Services services)

Specified by:

toString in interface IfFormulaInstantiation