de.uka.ilkd.key.speclang.jml.translation

Class JMLTranslator.JMLEqualityTranslationMethod

java.lang.Object

de.uka.ilkd.key.speclang.jml.translation.JMLTranslator.JMLEqualityTranslationMethod

All Implemented Interfaces:

JMLTranslationMethod

Enclosing class:

JMLTranslator

private abstract class JMLTranslator.JMLEqualityTranslationMethod
extends java.lang.Object
implements JMLTranslationMethod

Constructor Summary

Constructors

Modifier	Constructor and Description
private	JMLEqualityTranslationMethod()

Method Summary

Modifier and Type	Method and Description
protected SLExpression	buildEqualityTerm(SLExpression a, SLExpression b, SLTranslationExceptionManager excManager, Services services)
protected Term	buildEqualityTerm(Term a, Term b, SLTranslationExceptionManager excManager1, Services services)
protected void	checkSLExpressions(SLExpression expr1, SLExpression expr2, SLTranslationExceptionManager excManager, java.lang.String eqSymb)

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.speclang.jml.translation.JMLTranslationMethod

translate

Constructor Detail

JMLEqualityTranslationMethod

private JMLEqualityTranslationMethod()

Method Detail

checkSLExpressions

protected void checkSLExpressions(SLExpression expr1,
                                  SLExpression expr2,
                                  SLTranslationExceptionManager excManager,
                                  java.lang.String eqSymb)
                           throws SLTranslationException

Throws:

SLTranslationException

buildEqualityTerm

protected SLExpression buildEqualityTerm(SLExpression a,
                                         SLExpression b,
                                         SLTranslationExceptionManager excManager,
                                         Services services)
                                  throws SLTranslationException

Throws:

SLTranslationException

buildEqualityTerm

protected Term buildEqualityTerm(Term a,
                                 Term b,
                                 SLTranslationExceptionManager excManager1,
                                 Services services)
                          throws SLTranslationException

Throws:

SLTranslationException