Package org.jmlspecs.jml4.ast

Interface Summary

JmlAbstractMethodDeclaration
JmlDataGroupClause
JmlTypeReference

Class Summary

DepricateJmlRangeArrayReference
JmlAllocationExpression
JmlAllRangeExpression
JmlArrayIndexRangeExpression
JmlArrayQualifiedTypeReference
JmlArrayRangeStoreRef
JmlArrayReference
JmlArrayTypeReference
JmlAssertOrAssumeStatement
JmlAssertStatement
JmlAssignableClause
JmlAssignment
JmlAssumeStatement
JmlAstUtils
JmlBooleanQuantifier
JmlCastExpression
JmlCastExpressionWithoutType
JmlClause	An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.
JmlClinit
JmlCompilationUnitDeclaration
JmlConditionalExpression
JmlConstraintClause
JmlConstructorDeclaration
JmlDivergesClause
JmlDoStatement
JmlElemtypeExpression
JmlEnsuresClause
JmlExplicitConstructorCall
JmlFieldDeclaration
JmlFieldDotStarStoreRef
JmlFieldReference
JmlForeachStatement
JmlForStatement
JmlFreshExpression
JmlGroupName	Deprecated.
JmlInDataGroupClause
JmlInformalExpression	Informal expressions are used in predicates but also in store ref lists.
JmlInitiallyClause
JmlInvariantForType
JmlKeywordExpression	Instances of this class represent various JML keywords that are used in contexts where expressions (predicates or store references) are expected.
JmlLocalDeclaration
JmlLoopAnnotations
JmlLoopInvariant
JmlLoopVariant
JmlMapsIntoClause
JmlMapsMemberRefExpr	Deprecated.
JmlMemberFieldRef	Deprecated.
JmlMessageSend
JmlMethodDeclaration
JmlMethodSpecification
JmlModifier	This class offers services for processing JML modifiers.
JmlMultiReferenceExpression
JmlName
JmlNameDotStarStoreRef	Represents a JML store ref expression of the form name.*, where name is a NameReference.
JmlNumericQuantifier
JmlOldExpression
JmlOperationOverStoreRefList
JmlParameterizedQualifiedTypeReference
JmlParameterizedSingleTypeReference
JmlQualifiedNameReference
JmlQualifiedTypeReference
JmlQuantifiedExpression
JmlQuantifier
JmlRepresentsClause
JmlRequiresClause
JmlResultReference
JmlReturnStatement
JmlSetComprehension
JmlSetStatement
JmlSignalsClause
JmlSignalsOnlyClause
JmlSingleNameReference
JmlSingleTypeReference
JmlSpecCase
JmlSpecCaseBlock
JmlSpecCaseBody
JmlSpecCaseHeader
JmlSpecCaseRest
JmlSpecCaseRestAsClauseSeq
JmlStoreRefExpression	Deprecated.
JmlStoreRefListExpression
JmlSubtypeExpression
JmlTypeBodyDeclaration
JmlTypeDeclaration
JmlTypeExpression
JmlTypeofExpression
JmlUnaryExpression	NOTE: operators taking a list of store ref, like \not_modified() are modeled as unary operators -- taking a single argument consisting of the entire list.
JmlWhileStatement
JmlWildcard