public abstract class Contract extends Object
Modifier and Type | Class and Description |
---|---|
static class |
Contract.ConditionalPostcondition
Represents a conditional postcondition that must be verified by
BaseTypeVisitor or
one of its subclasses. |
static class |
Contract.Kind
Enumerates the kinds of contracts.
|
static class |
Contract.Postcondition
A postcondition contract.
|
static class |
Contract.Precondition
A precondition contract.
|
Modifier and Type | Field and Description |
---|---|
AnnotationMirror |
annotation
The annotation on the type of expression, according to this contract.
|
AnnotationMirror |
contractAnnotation
The annotation that expressed this contract; used for diagnostic messages.
|
String |
expressionString
The expression for which the condition must hold, such as
"foo" in
@RequiresNonNull("foo") . |
Contract.Kind |
kind
The kind of contract: precondition, postcondition, or conditional postcondition.
|
Modifier and Type | Method and Description |
---|---|
static Contract |
create(Contract.Kind kind,
String expressionString,
AnnotationMirror annotation,
AnnotationMirror contractAnnotation,
Boolean ensuresQualifierIf)
Creates a new Contract.
|
boolean |
equals(@Nullable Object o) |
int |
hashCode() |
String |
toString() |
public final String expressionString
"foo"
in
@RequiresNonNull("foo")
.
An annotation like @RequiresNonNull({"a", "b", "c"})
would be represented by
multiple Contracts.
public final AnnotationMirror annotation
public final AnnotationMirror contractAnnotation
public final Contract.Kind kind
public static Contract create(Contract.Kind kind, String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation, Boolean ensuresQualifierIf)
kind
- precondition, postcondition, or conditional postconditionexpressionString
- the Java expression that should have a type qualifierannotation
- the type qualifier that expressionString
should havecontractAnnotation
- the pre- or post-condition annotation that the programmer wrote;
used for diagnostic messagesensuresQualifierIf
- the ensuresQualifierIf field, for a conditional postcondition