de.uka.ilkd.key.rule.tacletbuilder

Class AntecSuccTacletGoalTemplate

java.lang.Object

de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate

de.uka.ilkd.key.rule.tacletbuilder.AntecSuccTacletGoalTemplate

public class AntecSuccTacletGoalTemplate
extends TacletGoalTemplate

Field Summary

Fields

Modifier and Type	Field and Description
private Sequent	replacewith sequent that replaces another one

Constructor Summary

Constructors

Constructor and Description
AntecSuccTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Sequent replacewith)
AntecSuccTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Sequent replacewith, ImmutableSet<SchemaVariable> pvs) creates new Goaldescription

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
ImmutableSet<QuantifiableVariable>	getBoundVariables() rertieves and returns all variables that are bound in the goal template
int	hashCode()
Sequent	replaceWith() a Taclet may replace a Sequent by another.
java.lang.Object	replaceWithExpressionAsObject() a Taclet may replace parts of sequent.
java.lang.String	toString() toString

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate

addedProgVars, name, rules, sequent, setName

Methods inherited from class java.lang.Object

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

Field Detail

replacewith

private Sequent replacewith

sequent that replaces another one

Constructor Detail

AntecSuccTacletGoalTemplate

public AntecSuccTacletGoalTemplate(Sequent addedSeq,
                                   ImmutableList<Taclet> addedRules,
                                   Sequent replacewith,
                                   ImmutableSet<SchemaVariable> pvs)

creates new Goaldescription

Parameters:

addedSeq - new Sequent to be added

addedRules - IList contains the new allowed rules at this branch

replacewith - the Sequent that replaces another one

AntecSuccTacletGoalTemplate

public AntecSuccTacletGoalTemplate(Sequent addedSeq,
                                   ImmutableList<Taclet> addedRules,
                                   Sequent replacewith)

Method Detail

replaceWith

public Sequent replaceWith()

a Taclet may replace a Sequent by another. The new Sequent is returned. this Sequent.

Returns:

Sequent being paramter in the rule goal replacewith(Seq)

getBoundVariables

public ImmutableSet<QuantifiableVariable> getBoundVariables()

rertieves and returns all variables that are bound in the goal template

Overrides:

getBoundVariables in class TacletGoalTemplate

Returns:

all variables that occur bound in this goal template

replaceWithExpressionAsObject

public java.lang.Object replaceWithExpressionAsObject()

Description copied from class: TacletGoalTemplate

a Taclet may replace parts of sequent.

Overrides:

replaceWithExpressionAsObject in class TacletGoalTemplate

Returns:

Sequent being paramter in the rule goal replacewith(Seq)

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class TacletGoalTemplate

hashCode

public int hashCode()

Overrides:

hashCode in class TacletGoalTemplate

toString

public java.lang.String toString()

toString

Overrides:

toString in class TacletGoalTemplate