de.uka.ilkd.key.rule

Class NotFreeIn

java.lang.Object

de.uka.ilkd.key.rule.NotFreeIn

public class NotFreeIn
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private SchemaVariable	first
private SchemaVariable	second

Constructor Summary

Constructors

Constructor and Description
NotFreeIn(SchemaVariable first, SchemaVariable second) constructs a pair of variables given two SchemaVariables.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
SchemaVariable	first() returns the first SchemaVariable of the pair.
int	hashCode()
SchemaVariable	second() returns the second SchemaVariable of the pair.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

first

private SchemaVariable first

second

private SchemaVariable second

Constructor Detail

NotFreeIn

public NotFreeIn(SchemaVariable first,
                 SchemaVariable second)

constructs a pair of variables given two SchemaVariables. The first SchemaVariable has to occur bound in the Taclet, while the second one can stand for a an arbitrary term of formula, in order to model a pair of the not-free-in relation of an Taclet.

Method Detail

first

public SchemaVariable first()

returns the first SchemaVariable of the pair. This SchemaVariable has to be matched to a QuantifiableVariable

second

public SchemaVariable second()

returns the second SchemaVariable of the pair.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object