Package | Description |
---|---|
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation |
Modifier and Type | Method and Description |
---|---|
protected SLExpression |
JMLBuiltInPropertyResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
JMLBuiltInPropertyResolver.canHandleReceiver(SLExpression receiver) |
protected SLExpression |
JMLBuiltInPropertyResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.add(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.antivalence(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.arrayRef(SLExpression receiver,
java.lang.String fullyQualifiedName,
SLExpression rangeFrom,
SLExpression rangeTo) |
SLExpression |
JmlTermFactory.bsum(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars) |
SLExpression |
JmlTermFactory.cast(KeYJavaType type,
SLExpression result) |
SLExpression |
JmlTermFactory.commentary(java.lang.String desc,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars,
Term heapAtPre) |
SLExpression |
JmlTermFactory.createIndexOf(Term seq,
Term elem) |
SLExpression |
JmlTermFactory.createIntersect(Term t,
JavaInfo javaInfo) |
SLExpression |
JmlTermFactory.createInv(Term selfVar,
KeYJavaType targetType)
Need to handle this one differently from INV_FOR
since here also static invariants may occur.
|
SLExpression |
JmlTermFactory.createPairwiseDisjoint(ImmutableList<Term> list) |
SLExpression |
JmlTermFactory.createSeqDef(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<? extends QuantifiableVariable> declVars) |
SLExpression |
JmlTermFactory.createSkolemExprBool(java.lang.String jmlKeyWord) |
SLExpression |
JmlTermFactory.createSkolemExprBool(org.antlr.runtime.Token jmlKeyWord)
Create a nullary predicate (wrapped in SLExpression) for currently unsupported JML expressions of type boolean.
|
SLExpression |
JmlTermFactory.createSkolemExprLong(java.lang.String text) |
SLExpression |
JmlTermFactory.createSkolemExprObject(java.lang.String jmlKeyWord) |
SLExpression |
JmlTermFactory.createUnion(JavaInfo javaInfo,
Term t) |
SLExpression |
JmlTermFactory.createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
SLExpression |
JmlTermFactory.dlKeyword(java.lang.String name,
ImmutableList<SLExpression> list) |
SLExpression |
JmlTermFactory.empty(JavaInfo javaInfo) |
SLExpression |
JmlTermFactory.eq(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.equivalence(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.exists(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.forall(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.fresh(ImmutableList<SLExpression> list,
java.util.Map<LocationVariable,Term> atPres) |
SLExpression |
JmlTermFactory.index() |
SLExpression |
JmlTermFactory.invFor(SLExpression param) |
SLExpression |
JmlTermFactory.ite(SLExpression result,
SLExpression a,
SLExpression b) |
SLExpression |
JmlTermFactory.neq(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.quantifiedMax(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedMin(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedNumOf(Term t1,
Term t2,
KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedProduct(KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedSum(KeYJavaType javaType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.reach(Term t,
SLExpression e1,
SLExpression e2,
SLExpression e3) |
SLExpression |
JmlTermFactory.reachLocs(Term t,
SLExpression e1,
SLExpression e2,
SLExpression e3) |
SLExpression |
JmlTermFactory.seqConcat(Term seq1,
Term seq2) |
SLExpression |
JmlTermFactory.seqConst(ImmutableList<SLExpression> exprList) |
SLExpression |
JmlTermFactory.seqGet(Term seq,
Term idx) |
SLExpression |
JmlTermFactory.shiftLeft(SLExpression result,
SLExpression e) |
SLExpression |
JmlTermFactory.shiftRight(SLExpression a,
SLExpression e) |
SLExpression |
JmlTermFactory.skolemExprHelper(KeYJavaType type,
TermServices services,
java.lang.String shortName) |
SLExpression |
JmlTermFactory.skolemExprHelper(java.lang.String jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
JmlTermFactory.skolemExprHelper(java.lang.String jmlKeyWord,
PrimitiveType type) |
SLExpression |
JmlTermFactory.skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
JmlTermFactory.skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
PrimitiveType type) |
SLExpression |
JmlTermFactory.staticInfFor(KeYJavaType kjt) |
SLExpression |
JmlTermFactory.substract(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.translateArrayReference(SLExpression receiver,
SLExpression rangeFrom,
SLExpression rangeTo) |
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(java.lang.String text,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(org.antlr.runtime.Token t,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateSequenceReference(SLExpression receiver,
SLExpression rangeFrom,
SLExpression rangeTo) |
SLExpression |
JmlTermFactory.translateToJDLTerm(java.lang.String functName,
ImmutableList<SLExpression> list) |
SLExpression |
JmlTermFactory.translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list) |
SLExpression |
JmlTermFactory.unsignedShiftRight(SLExpression left,
SLExpression right) |
SLExpression |
JmlTermFactory.values(KeYJavaType t) |
Modifier and Type | Method and Description |
---|---|
Term |
JmlTermFactory.createLocSet(ImmutableList<SLExpression> exprList) |
SLExpression |
JmlTermFactory.dlKeyword(java.lang.String name,
ImmutableList<SLExpression> list) |
SLExpression |
JmlTermFactory.fresh(ImmutableList<SLExpression> list,
java.util.Map<LocationVariable,Term> atPres) |
SLExpression |
JmlTermFactory.seqConst(ImmutableList<SLExpression> exprList) |
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(java.lang.String text,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateMapExpressionToJDL(org.antlr.runtime.Token t,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
JmlTermFactory.translateToJDLTerm(java.lang.String functName,
ImmutableList<SLExpression> list) |
SLExpression |
JmlTermFactory.translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SLExpression> |
SLParameters.getParameters() |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JavaIntegerSemanticsHelper.buildAddExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildCastExpression(KeYJavaType resultType,
SLExpression a) |
SLExpression |
JavaIntegerSemanticsHelper.buildDivExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildLeftShiftExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildModExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildMulExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildPromotedAndExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildPromotedNegExpression(SLExpression a) |
SLExpression |
JavaIntegerSemanticsHelper.buildPromotedOrExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildPromotedUnaryPlusExpression(SLExpression a) |
SLExpression |
JavaIntegerSemanticsHelper.buildPromotedXorExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildRightShiftExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildSubExpression(SLExpression a,
SLExpression b) |
SLExpression |
JavaIntegerSemanticsHelper.buildUnaryMinusExpression(SLExpression a) |
SLExpression |
JavaIntegerSemanticsHelper.buildUnsignedRightShiftExpression(SLExpression a,
SLExpression b) |
protected boolean |
SLMethodResolver.canHandleReceiver(SLExpression receiver) |
protected boolean |
SLAttributeResolver.canHandleReceiver(SLExpression receiver) |
protected boolean |
SLTypeResolver.canHandleReceiver(SLExpression receiver) |
protected abstract boolean |
SLExpressionResolver.canHandleReceiver(SLExpression receiver) |
protected SLExpression |
SLMethodResolver.doResolving(SLExpression receiver,
java.lang.String methodName,
SLParameters parameters) |
protected SLExpression |
SLAttributeResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
protected SLExpression |
SLTypeResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
protected abstract SLExpression |
SLExpressionResolver.doResolving(SLExpression receiver,
java.lang.String name,
SLParameters parameters)
Resolves property calls on explicit receivers.
|
boolean |
JavaIntegerSemanticsHelper.isIntegerTerm(SLExpression a) |
SLExpression |
SLResolverManager.resolve(SLExpression receiver,
java.lang.String name,
SLParameters parameters)
Resolves arbitrary property calls.
|
SLExpression |
SLExpressionResolver.resolve(SLExpression receiver,
java.lang.String name,
SLParameters parameters) |
Constructor and Description |
---|
SLParameters(ImmutableList<SLExpression> parameters) |
Copyright © 2003-2019 The KeY-Project.