jml2b.languages
Interface ILanguage

All Known Implementing Classes:

JavaLanguage

public interface ILanguage

This interface allows to define a new language, it has to be implement by a plugin defining a new language.

Author:

L. Burdy

Method Summary

java.lang.String	displayGoal(Goal g, boolean applySubstitution) Displays a goal in the lemma view.
ITranslatable	formulaFactory(Formula f) Returns a formula corresponding to the initial but converted in a translatable subclass of formula.
ITranslationResult	load(JpoInputStream s) Load a terminal formula from a jpo file.
ITranslatable	quantifiedVarFactory(QuantifiedVarForm qvf) Returns quantified variables corresponding to the initial ones but translatable.
void	save(IOutputStream s, ITranslationResult result) Saves the result of a translation in a jpo file.
void	save(IOutputStream s, TerminalForm f) Saves a terminal formula in a jpo file.
ITranslatable	typeFactory(Type t) Returns a type corresponding to the initial one but converted in a translatable type.

Method Detail

formulaFactory

public ITranslatable formulaFactory(Formula f)

Returns a formula corresponding to the initial but converted in a translatable subclass of formula. The result has to be a subtype of formula.

Parameters:

f - The formula to convert

Returns:

the converted formula

typeFactory

public ITranslatable typeFactory(Type t)

Returns a type corresponding to the initial one but converted in a translatable type.

Parameters:

t - The type to convert

Returns:

the converted type

quantifiedVarFactory

public ITranslatable quantifiedVarFactory(QuantifiedVarForm qvf)

Returns quantified variables corresponding to the initial ones but translatable.

Parameters:

qvf - The quantified variables to convert

Returns:

the converted quantified variables

displayGoal

public java.lang.String displayGoal(Goal g,
                                    boolean applySubstitution)

Displays a goal in the lemma view.

Parameters:

g - The goal to display

Returns:

the string to print in the lemma view that correspond to the goal.

save

public void save(IOutputStream s,
                 TerminalForm f)
          throws java.io.IOException,
                 LanguageException

Saves a terminal formula in a jpo file.

Parameters:

s - The jpo file

f - The formula to save

Throws:

java.io.IOException

LanguageException

save

public void save(IOutputStream s,
                 ITranslationResult result)
          throws java.io.IOException

Saves the result of a translation in a jpo file.

Parameters:

s - The jpo file

result - The result to save

Throws:

java.io.IOException

load

public ITranslationResult load(JpoInputStream s)
                        throws java.io.IOException

Load a terminal formula from a jpo file.

Parameters:

s - The jpo file

Returns:

Throws:

java.io.IOException