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

Class JMLTranslator.JMLQuantifierTranslationMethod

java.lang.Object

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

All Implemented Interfaces:

JMLTranslationMethod

Direct Known Subclasses:

JMLTranslator.JMLBoundedNumericalQuantifierTranslationMethod

Enclosing class:

JMLTranslator

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

Field Summary

Fields

Modifier and Type	Field and Description
protected Services	services

Constructor Summary

Constructors

Modifier	Constructor and Description
private	JMLQuantifierTranslationMethod()

Method Summary

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)

Methods inherited from class java.lang.Object

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

Field Detail

services

protected Services services

Constructor Detail

JMLQuantifierTranslationMethod

private JMLQuantifierTranslationMethod()

Method Detail

translate

public SLExpression translate(SLTranslationExceptionManager excManager,
                              java.lang.Object... params)
                       throws SLTranslationException

Add implicit "non-null" and "created" guards for reference types, "in-bounds" guards for integer types. Then, translateToTerm the quantifier.

Specified by:

translate in interface JMLTranslationMethod

Parameters:

quantName -

declVars -

expr -

preTerm -

bodyTerm -

nullable -

services -

Returns:

Throws:

SLTranslationException

translateQuantifiers

public SLExpression translateQuantifiers(java.lang.Iterable<LogicVariable> qvs,
                                         Term t1,
                                         Term t2)
                                  throws SLTranslationException

Throws:

SLTranslationException

translateGeneralizedQuantifiers

public SLExpression translateGeneralizedQuantifiers(KeYJavaType declsType,
                                                    boolean nullable,
                                                    java.lang.Iterable<LogicVariable> qvs,
                                                    Term t1,
                                                    Term t2,
                                                    KeYJavaType resultType)
                                             throws SLTranslationException

Throws:

SLTranslationException

combineQuantifiedTerms

public abstract Term combineQuantifiedTerms(Term t1,
                                            Term t2)
                                     throws SLTranslationException

Throws:

SLTranslationException

translateQuantifier

public abstract Term translateQuantifier(QuantifiableVariable qv,
                                         Term t)
                                  throws SLTranslationException

Throws:

SLTranslationException

isGeneralized

protected abstract boolean isGeneralized()