private abstract class JMLTranslator.JMLQuantifierTranslationMethod extends java.lang.Object implements JMLTranslationMethod
Modifier | Constructor and Description |
---|---|
private |
JMLQuantifierTranslationMethod() |
Modifier and Type | Method and Description |
---|---|
abstract Term |
combineQuantifiedTerms(Term t1,
Term t2) |
protected abstract boolean |
isGeneralized() |
SLExpression |
translate(SLTranslationExceptionManager excManager,
java.lang.Object... params)
Add implicit "non-null" and "created" guards for reference types,
"in-bounds" guards for integer types.
|
SLExpression |
translateGeneralizedQuantifiers(KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
abstract Term |
translateQuantifier(QuantifiableVariable qv,
Term t) |
SLExpression |
translateQuantifiers(java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2) |
protected Services services
public SLExpression translate(SLTranslationExceptionManager excManager, java.lang.Object... params) throws SLTranslationException
translate
in interface JMLTranslationMethod
quantName
- declVars
- expr
- preTerm
- bodyTerm
- nullable
- services
- SLTranslationException
public SLExpression translateQuantifiers(java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2) throws SLTranslationException
SLTranslationException
public SLExpression translateGeneralizedQuantifiers(KeYJavaType declsType, boolean nullable, java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2, KeYJavaType resultType) throws SLTranslationException
SLTranslationException
public abstract Term combineQuantifiedTerms(Term t1, Term t2) throws SLTranslationException
SLTranslationException
public abstract Term translateQuantifier(QuantifiableVariable qv, Term t) throws SLTranslationException
SLTranslationException
protected abstract boolean isGeneralized()