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

Class JMLTranslator.JMLBoundedNumericalQuantifierTranslationMethod

java.lang.Object

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

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

All Implemented Interfaces:

JMLTranslationMethod

Enclosing class:

JMLTranslator

private abstract class JMLTranslator.JMLBoundedNumericalQuantifierTranslationMethod
extends JMLTranslator.JMLQuantifierTranslationMethod

Field Summary

Fields inherited from class de.uka.ilkd.key.speclang.jml.translation.JMLTranslator.JMLQuantifierTranslationMethod

services

Constructor Summary

Constructors

Modifier	Constructor and Description
private	JMLBoundedNumericalQuantifierTranslationMethod()

Method Summary

Modifier and Type	Method and Description
Term	combineQuantifiedTerms(Term t1, Term t2) Deprecated.
private boolean	isBoundedNumerical(Term a, LogicVariable lv)
protected boolean	isGeneralized()
private Term	lowerBound(Term a, LogicVariable lv) Extracts lower bound from a if it matches the pattern.
SLExpression	translate(SLTranslationExceptionManager excManager, java.lang.Object... params) Add implicit "non-null" and "created" guards for reference types, "in-bounds" guards for integer types.
abstract Term	translateBoundedNumericalQuantifier(QuantifiableVariable qv, Term lo, Term hi, Term body) Creates a term for a bounded numerical quantifier (e.g., sum).
SLExpression	translateGeneralizedQuantifiers(KeYJavaType declsType, boolean nullable, java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2, KeYJavaType resultType)
Term	translateQuantifier(QuantifiableVariable qv, Term t) Deprecated.
SLExpression	translateQuantifiers(java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2) Deprecated.
protected abstract Term	translateUnboundedNumericalQuantifier(KeYJavaType declsType, boolean nullable, ImmutableList<QuantifiableVariable> qvs, Term range, Term body)
private Term	upperBound(Term a, LogicVariable lv) Extracts upper bound from a if it matches the pattern.

Methods inherited from class java.lang.Object

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

Constructor Detail

JMLBoundedNumericalQuantifierTranslationMethod

private JMLBoundedNumericalQuantifierTranslationMethod()

Method Detail

isBoundedNumerical

private boolean isBoundedNumerical(Term a,
                                   LogicVariable lv)

lowerBound

private Term lowerBound(Term a,
                        LogicVariable lv)

Extracts lower bound from a if it matches the pattern.

Parameters:

a - guard to be disected

lv - variable bound by quantifier

Returns:

lower bound term (or null)

upperBound

private Term upperBound(Term a,
                        LogicVariable lv)

Extracts upper bound from a if it matches the pattern.

Parameters:

a - guard to be disected

lv - variable bound by quantifier

Returns:

upper bound term (or null)

translate

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

Description copied from class: JMLTranslator.JMLQuantifierTranslationMethod

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

Overrides:

translate in class JMLTranslator.JMLQuantifierTranslationMethod

Throws:

SLTranslationException

translateQuantifiers

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

Deprecated.

Overrides:

translateQuantifiers in class JMLTranslator.JMLQuantifierTranslationMethod

translateGeneralizedQuantifiers

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

Overrides:

translateGeneralizedQuantifiers in class JMLTranslator.JMLQuantifierTranslationMethod

Throws:

SLTranslationException

translateUnboundedNumericalQuantifier

protected abstract Term translateUnboundedNumericalQuantifier(KeYJavaType declsType,
                                                              boolean nullable,
                                                              ImmutableList<QuantifiableVariable> qvs,
                                                              Term range,
                                                              Term body)

isGeneralized

protected boolean isGeneralized()

Specified by:

isGeneralized in class JMLTranslator.JMLQuantifierTranslationMethod

translateBoundedNumericalQuantifier

public abstract Term translateBoundedNumericalQuantifier(QuantifiableVariable qv,
                                                         Term lo,
                                                         Term hi,
                                                         Term body)

Creates a term for a bounded numerical quantifier (e.g., sum).

combineQuantifiedTerms

@Deprecated
public Term combineQuantifiedTerms(Term t1,
                                               Term t2)

Deprecated.

Should not be called.

Specified by:

combineQuantifiedTerms in class JMLTranslator.JMLQuantifierTranslationMethod

translateQuantifier

@Deprecated
public Term translateQuantifier(QuantifiableVariable qv,
                                            Term t)

Deprecated.

Should not be called.

Specified by:

translateQuantifier in class JMLTranslator.JMLQuantifierTranslationMethod