de.uka.ilkd.key.rule

Class AbstractBlockContractRule.Instantiator

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule.Instantiator

de.uka.ilkd.key.rule.AbstractBlockContractRule.Instantiator

Enclosing class:

AbstractBlockContractRule

protected static final class AbstractBlockContractRule.Instantiator
extends AbstractAuxiliaryContractRule.Instantiator

A builder for Instantiations.

Constructor Summary

Constructors

Constructor and Description
Instantiator(Term formula, Goal goal, Services services)

Method Summary

Modifier and Type	Method and Description
protected boolean	hasApplicableContracts(Services services, JavaStatement statement, Modality modality, Goal goal)

Methods inherited from class de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule.Instantiator

instantiate

Methods inherited from class java.lang.Object

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

Constructor Detail

Instantiator

public Instantiator(Term formula,
                    Goal goal,
                    Services services)

Parameters:

formula - the formula on which the rule is to be applied.

goal - the current goal.

services - services.

Method Detail

hasApplicableContracts

protected boolean hasApplicableContracts(Services services,
                                         JavaStatement statement,
                                         Modality modality,
                                         Goal goal)

Specified by:

hasApplicableContracts in class AbstractAuxiliaryContractRule.Instantiator

Parameters:

services - services.

statement - a block or loop.

modality - the current goal's modality.

goal - the current goal.

Returns:

true iff the block has applicable contracts.