de.uka.ilkd.key.strategy.termProjection

Class AssumptionProjection

java.lang.Object

de.uka.ilkd.key.strategy.termProjection.AssumptionProjection

All Implemented Interfaces:

ProjectionToTerm

public class AssumptionProjection
extends java.lang.Object
implements ProjectionToTerm

Term projection that delivers the assumptions of a taclet application (the formulas that the \assumes clause of the taclet refers to).

Field Summary

Fields

Modifier and Type	Field and Description
private int	no

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AssumptionProjection(int no)

Method Summary

Modifier and Type	Method and Description
static ProjectionToTerm	create(int no)
Term	toTerm(RuleApp app, PosInOccurrence pos, Goal goal)

Methods inherited from class java.lang.Object

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

Field Detail

no

private final int no

Constructor Detail

AssumptionProjection

private AssumptionProjection(int no)

Method Detail

create

public static ProjectionToTerm create(int no)

toTerm

public Term toTerm(RuleApp app,
                   PosInOccurrence pos,
                   Goal goal)

Specified by:

toTerm in interface ProjectionToTerm