TopLevelFindFeature.TopLevelWithoutUpdate (KeY API Documentation)

private abstract static class TopLevelFindFeature.TopLevelWithoutUpdate
extends TopLevelFindFeature

Field Summary
- Fields inherited from class de.uka.ilkd.key.strategy.feature.TopLevelFindFeature
  ANTEC, ANTEC_OR_SUCC, ANTEC_OR_SUCC_WITH_UPDATE, ANTEC_WITH_UPDATE, SUCC, SUCC_WITH_UPDATE
- Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature
  TOP_COST, ZERO_COST

Constructors
Modifier	Constructor and Description
`private`	`TopLevelWithoutUpdate()`

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method and Description
`protected boolean`	`checkPosition(PosInOccurrence pos)`
`protected abstract boolean`	`matches(PosInOccurrence pos)`

Methods inherited from class de.uka.ilkd.key.strategy.feature.TopLevelFindFeature
filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature
filter

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

Constructor Detail
- TopLevelWithoutUpdate
```
private TopLevelWithoutUpdate()
```

protected abstract boolean matches(PosInOccurrence pos)

Class TopLevelFindFeature.TopLevelWithoutUpdate