de.uka.ilkd.key.rule

Interface VariableCondition

All Known Implementing Classes:

AbstractOrInterfaceType, AlternativeVariableCondition, ApplyUpdateOnRigidCondition, ArrayComponentTypeCondition, ArrayLengthCondition, ArrayTypeCondition, ConstantCondition, ContainsAssignmentCondition, DifferentFields, DifferentInstantiationCondition, DropEffectlessElementariesCondition, DropEffectlessStoresCondition, EnumConstantCondition, EnumTypeCondition, EqualUniqueCondition, FieldTypeToSortCondition, FinalReferenceCondition, FreeLabelInVariableCondition, IsThisReference, JavaTypeToSortCondition, LocalVariableCondition, MetaDisjointCondition, NewJumpLabelCondition, ObserverCondition, SimplifyIfThenElseUpdateCondition, StaticFieldCondition, StaticMethodCondition, StaticReferenceCondition, SubFormulaCondition, TermLabelCondition, TypeComparisonCondition, TypeCondition, VariableConditionAdapter

public interface VariableCondition

The instantiations of a schemavariable can be restricted on rule scope by attaching conditions on these variables. Such a condition is realized by a class which implements this interface. The usual place where to put these implementations is inside package de.uka.ilkd.key.rule.conditions. For variable conditions that know only black and white answers there exists a convenience class VariableConditionAdapter.

Method Summary

Modifier and Type	Method and Description
MatchConditions	check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions matchCond, Services services) checks if the condition for a correct instantiation is fulfilled

Method Detail

check

MatchConditions check(SchemaVariable var,
                      SVSubstitute instCandidate,
                      MatchConditions matchCond,
                      Services services)

checks if the condition for a correct instantiation is fulfilled

Parameters:

var - the SchemaVariable to be instantiated

instCandidate - the SVSubstitute (e.g. Term, ProgramElement) to be mapped to var

matchCond - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed

services - the program information object

Returns:

modified match results if the condition can be satisfied, or null otherwise