private abstract class JMLTranslator.JMLBoundedNumericalQuantifierTranslationMethod extends JMLTranslator.JMLQuantifierTranslationMethod
services
Modifier | Constructor and Description |
---|---|
private |
JMLBoundedNumericalQuantifierTranslationMethod() |
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. |
private JMLBoundedNumericalQuantifierTranslationMethod()
private boolean isBoundedNumerical(Term a, LogicVariable lv)
private Term lowerBound(Term a, LogicVariable lv)
a
if it matches the pattern.a
- guard to be disectedlv
- variable bound by quantifierprivate Term upperBound(Term a, LogicVariable lv)
a
if it matches the pattern.a
- guard to be disectedlv
- variable bound by quantifierpublic SLExpression translate(SLTranslationExceptionManager excManager, java.lang.Object... params) throws SLTranslationException
JMLTranslator.JMLQuantifierTranslationMethod
translate
in interface JMLTranslationMethod
translate
in class JMLTranslator.JMLQuantifierTranslationMethod
SLTranslationException
@Deprecated public SLExpression translateQuantifiers(java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2)
translateQuantifiers
in class JMLTranslator.JMLQuantifierTranslationMethod
public SLExpression translateGeneralizedQuantifiers(KeYJavaType declsType, boolean nullable, java.lang.Iterable<LogicVariable> qvs, Term t1, Term t2, KeYJavaType resultType) throws SLTranslationException
translateGeneralizedQuantifiers
in class JMLTranslator.JMLQuantifierTranslationMethod
SLTranslationException
protected abstract Term translateUnboundedNumericalQuantifier(KeYJavaType declsType, boolean nullable, ImmutableList<QuantifiableVariable> qvs, Term range, Term body)
protected boolean isGeneralized()
isGeneralized
in class JMLTranslator.JMLQuantifierTranslationMethod
public abstract Term translateBoundedNumericalQuantifier(QuantifiableVariable qv, Term lo, Term hi, Term body)
@Deprecated public Term combineQuantifiedTerms(Term t1, Term t2)
combineQuantifiedTerms
in class JMLTranslator.JMLQuantifierTranslationMethod
@Deprecated public Term translateQuantifier(QuantifiableVariable qv, Term t)
translateQuantifier
in class JMLTranslator.JMLQuantifierTranslationMethod