jml2b.languages.java
Class JavaLanguage

java.lang.Object
  jml2b.languages.java.JavaLanguage

All Implemented Interfaces:

ILanguage

public class JavaLanguage

extends java.lang.Object

implements ILanguage

Author:

L. Burdy

Constructor Summary

JavaLanguage()

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.

Methods inherited from class java.lang.Object

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

Constructor Detail

JavaLanguage

public JavaLanguage()

Method Detail

formulaFactory

public ITranslatable formulaFactory(Formula f)

Description copied from interface: ILanguage

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

Specified by:

formulaFactory in interface ILanguage

Parameters:

f - The formula to convert

Returns:

the converted formula

typeFactory

public ITranslatable typeFactory(Type t)

Description copied from interface: ILanguage

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

Specified by:

typeFactory in interface ILanguage

Parameters:

t - The type to convert

Returns:

the converted type

quantifiedVarFactory

public ITranslatable quantifiedVarFactory(QuantifiedVarForm qvf)

Description copied from interface: ILanguage

Returns quantified variables corresponding to the initial ones but translatable.

Specified by:

quantifiedVarFactory in interface ILanguage

Parameters:

qvf - The quantified variables to convert

Returns:

the converted quantified variables

displayGoal

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

Description copied from interface: ILanguage

Displays a goal in the lemma view.

Specified by:

displayGoal in interface ILanguage

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

Description copied from interface: ILanguage

Saves a terminal formula in a jpo file.

Specified by:

save in interface ILanguage

Parameters:

s - The jpo file

f - The formula to save

Throws:

java.io.IOException

save

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

Description copied from interface: ILanguage

Saves the result of a translation in a jpo file.

Specified by:

save in interface ILanguage

Parameters:

s - The jpo file

result - The result to save

Throws:

java.io.IOException

load

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

Description copied from interface: ILanguage

Load a terminal formula from a jpo file.

Specified by:

load in interface ILanguage

Parameters:

s - The jpo file

Returns:

Throws:

java.io.IOException