public class ContractsUtils
extends java.lang.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 | 
|---|---|
java.util.Set<ContractsUtils.ConditionalPostcondition> | 
getConditionalPostconditions(javax.lang.model.element.ExecutableElement methodElement)
Returns a set of triples  
(expr, (result, annotation)) of conditional postconditions
 on the method methodElement. | 
java.util.List<ContractsUtils.Contract> | 
getContracts(javax.lang.model.element.ExecutableElement element)  | 
static ContractsUtils | 
getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)
Returns an instance of the  
ContractsUtils class. | 
java.util.Set<ContractsUtils.Postcondition> | 
getPostconditions(javax.lang.model.element.ExecutableElement methodElement)
Returns the set of postconditions on the method  
methodElement. | 
java.util.Set<ContractsUtils.Precondition> | 
getPreconditions(javax.lang.model.element.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 java.util.List<ContractsUtils.Contract> getContracts(javax.lang.model.element.ExecutableElement element)
public java.util.Set<ContractsUtils.Precondition> getPreconditions(javax.lang.model.element.Element element)
element.public java.util.Set<ContractsUtils.Postcondition> getPostconditions(javax.lang.model.element.ExecutableElement methodElement)
methodElement.public java.util.Set<ContractsUtils.ConditionalPostcondition> getConditionalPostconditions(javax.lang.model.element.ExecutableElement methodElement)
(expr, (result, annotation)) of conditional postconditions
 on the method methodElement.