de.uka.ilkd.key.taclettranslation.assumptions

Interface TacletSetTranslation

All Known Implementing Classes:

DefaultTacletSetTranslation

public interface TacletSetTranslation

This interface provides the mechanism of translating taclets to formulae. The resulting formulae can be used for example for building assumptions for external proofers. CAUTION: The correctness of a single formula, i.d. the universal validity, depends on the particular taclet.

Method Summary

Modifier and Type	Method and Description
ImmutableList<TacletFormula>	getNotTranslated() Returns all taclet that have not been translated.
ImmutableList<TacletFormula>	getTranslation(ImmutableSet<Sort> sorts) Builds the translation of the taclets given by calling the method setTacletSet().
void	update() Updates the translation, i.d. the given list of taclets is being translated again.

Method Detail

getTranslation

ImmutableList<TacletFormula> getTranslation(ImmutableSet<Sort> sorts)

Builds the translation of the taclets given by calling the method setTacletSet().

Parameters:

sorts - this sorts are used for the instantiation of generic types.

Returns:

returns the resulting formulae of the taclets. Each formula of the resulting set is associated with one taclet.

getNotTranslated

ImmutableList<TacletFormula> getNotTranslated()

Returns all taclet that have not been translated. The reason can be got by TacletFormula.getStatus().

Returns:

a list of taclets.

update

void update()

Updates the translation, i.d. the given list of taclets is being translated again.