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.Contract
A contract represents an annotation on an expression, along with the kind: precondition,
postcondition, or conditional postcondition.
|
static class |
ContractsUtils.Postcondition |
static class |
ContractsUtils.Precondition |
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 . |
List<ContractsUtils.Contract> |
getContracts(ExecutableElement element) |
static ContractsUtils |
getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)
Returns an instance of the
ContractsUtils class. |
Set<ContractsUtils.Postcondition> |
getPostconditions(ExecutableElement methodElement)
Returns the set of postconditions on the method
methodElement . |
Set<ContractsUtils.Precondition> |
getPreconditions(Element element)
Returns the set of preconditions on the element
element . |
protected static ContractsUtils instance
protected GenericAnnotatedTypeFactory<?,?,?,?> factory
public static ContractsUtils getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)
ContractsUtils
class.public List<ContractsUtils.Contract> getContracts(ExecutableElement element)
public Set<ContractsUtils.Precondition> getPreconditions(Element element)
element
.public Set<ContractsUtils.Postcondition> getPostconditions(ExecutableElement methodElement)
methodElement
.public Set<ContractsUtils.ConditionalPostcondition> getConditionalPostconditions(ExecutableElement methodElement)
(expr, (result, annotation))
of conditional postconditions
on the method methodElement
.