public class ContractsUtils extends Object
PreconditionAnnotation
,
RequiresQualifier
,
PostconditionAnnotation
,
EnsuresQualifier
,
EnsuresQualifierIf
Modifier and Type | Class and Description |
---|---|
static class |
ContractsUtils.ConditionalPostcondition
Represents a conditional postcondition that must be verified by
BaseTypeVisitor or one of its subclasses. |
static class |
ContractsUtils.PreOrPostcondition
Represents a pre- or postcondition that must be verified by
BaseTypeVisitor or one of its subclasses. |
Modifier and Type | Field and Description |
---|---|
protected GenericAnnotatedTypeFactory<?,?,?,?> |
factory |
protected static ContractsUtils |
instance |
Modifier and Type | Method and Description |
---|---|
Set<ContractsUtils.ConditionalPostcondition> |
getConditionalPostconditions(ExecutableElement methodElement)
Returns a set of triples
(expr, (result, annotation)) of
conditional postconditions on the method methodElement . |
static ContractsUtils |
getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)
Returns an instance of the
ContractsUtils class. |
Set<ContractsUtils.PreOrPostcondition> |
getPostconditions(ExecutableElement methodElement)
Returns a set of pairs
(expr, annotation) of postconditions on
the method methodElement . |
Set<ContractsUtils.PreOrPostcondition> |
getPreconditions(Element element)
Returns a set of pairs
(expr, annotation) of preconditions on the
element element . |
protected static ContractsUtils instance
protected GenericAnnotatedTypeFactory<?,?,?,?> factory
public static ContractsUtils getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)
ContractsUtils
class.public Set<ContractsUtils.PreOrPostcondition> getPreconditions(Element element)
(expr, annotation)
of preconditions on the
element element
.public Set<ContractsUtils.PreOrPostcondition> getPostconditions(ExecutableElement methodElement)
(expr, annotation)
of postconditions on
the method methodElement
.public Set<ContractsUtils.ConditionalPostcondition> getConditionalPostconditions(ExecutableElement methodElement)
(expr, (result, annotation))
of
conditional postconditions on the method methodElement
.