de.uka.ilkd.key.taclettranslation

Interface TacletFormula

All Known Implementing Classes:

AssumptionFormula, LemmaFormula

public interface TacletFormula

Represents the formula of a taclet.
It provides methods to get the formula and its corresponding taclet.
The setting of the formula and the taclet is dedicated to the constructor of the implementing class. This ensures that the relationship between both is not changed afterwards.

Method Summary

Modifier and Type	Method and Description
Term	getFormula(TermServices services)
java.util.Collection<Term>	getInstantiations() It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated.
java.lang.String	getStatus()
Taclet	getTaclet()

Method Detail

getTaclet

Taclet getTaclet()

Returns:

the taclet of the instance.

getFormula

Term getFormula(TermServices services)

Parameters:

services - TODO

Returns:

the formula of the instance if the taclet is translatable otherwise null. If the translation of the taclet consists of several instantiations (e.g. the taclet has some generic sorts) the returned term is a conjunction of these instantiations.

getStatus

java.lang.String getStatus()

Returns:

if the taclet can not be translated the reason why. Otherwise a empty string.

getInstantiations

java.util.Collection<Term> getInstantiations()

It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated. This method returns the set of resulting formulas.