de.uka.ilkd.key.rule.conditions

Class ContainsAssignmentCondition

java.lang.Object

de.uka.ilkd.key.rule.VariableConditionAdapter

de.uka.ilkd.key.rule.conditions.ContainsAssignmentCondition

All Implemented Interfaces:

VariableCondition

public class ContainsAssignmentCondition
extends VariableConditionAdapter

This variable condition can be used to check whether an assignment expression occurs as a subexpression of a schemavariable instantiation,

Author:

Dominic Scheurer

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	ContainsAssignmentCondition.ContainsAssignment Visitor iterating over an expression and returning true if an assignment statement has been found.

Field Summary

Fields

Modifier and Type	Field and Description
private SchemaVariable	expression
private boolean	negated

Constructor Summary

Constructors

Constructor and Description
ContainsAssignmentCondition(SchemaVariable x, boolean negated) creates an instance of the variable condition

Method Summary

Modifier and Type	Method and Description
boolean	check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, Services services) checks if the condition for a correct instantiation is fulfilled
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.rule.VariableConditionAdapter

check

Methods inherited from class java.lang.Object

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

Field Detail

expression

private final SchemaVariable expression

negated

private final boolean negated

Constructor Detail

ContainsAssignmentCondition

public ContainsAssignmentCondition(SchemaVariable x,
                                   boolean negated)

creates an instance of the variable condition

Parameters:

x - the schemavariable whose instantiation is to be checked

negated - true iff the check should ensure the absence of an assignment statement

Throws:

java.lang.IllegalArgumentException - if the given schemavariable is not a ProgramSV

Method Detail

check

public boolean check(SchemaVariable var,
                     SVSubstitute instCandidate,
                     SVInstantiations instMap,
                     Services services)

checks if the condition for a correct instantiation is fulfilled

Specified by:

check in class VariableConditionAdapter

Parameters:

var - the template Variable to be instantiated

instMap - 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:

true iff condition is fulfilled

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object