de.uka.ilkd.key.strategy.feature

Class SeqContainsExecutableCodeFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.SeqContainsExecutableCodeFeature

All Implemented Interfaces:

Feature

public class SeqContainsExecutableCodeFeature
extends BinaryFeature

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	PROGRAMS
static Feature	PROGRAMS_OR_QUERIES
private TermFeature	tf

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SeqContainsExecutableCodeFeature(boolean considerQueries)

Method Summary

Modifier and Type	Method and Description
private boolean	containsExec(java.util.Iterator<SequentFormula> it, Services services)
protected boolean	filter(RuleApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

tf

private final TermFeature tf

PROGRAMS

public static final Feature PROGRAMS

PROGRAMS_OR_QUERIES

public static final Feature PROGRAMS_OR_QUERIES

Constructor Detail

SeqContainsExecutableCodeFeature

private SeqContainsExecutableCodeFeature(boolean considerQueries)

Method Detail

filter

protected boolean filter(RuleApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

containsExec

private boolean containsExec(java.util.Iterator<SequentFormula> it,
                             Services services)