org.checkerframework.framework.util

Class Contract

java.lang.Object

org.checkerframework.framework.util.Contract

Direct Known Subclasses:

Contract.ConditionalPostcondition, Contract.Postcondition, Contract.Precondition

public abstract class Contract
extends Object

A contract represents an annotation on an expression. It is a precondition, postcondition, or conditional postcondition.

See Also:

Contract.Precondition, Contract.Postcondition, Contract.ConditionalPostcondition

Nested Class Summary

Nested Classes

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.

Field Summary

Fields

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	expression 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.

Method Summary

Modifier and Type	Method and Description
static Contract	create(Contract.Kind kind, String expression, AnnotationMirror annotation, AnnotationMirror contractAnnotation, Boolean ensuresQualifierIf) Creates a new Contract.
boolean	equals(@Nullable Object o)
int	hashCode()
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

expression

public final String expression

The expression for which the condition must hold, such as "foo" in @RequiresNonNull("foo").

An annotation like @RequiresNonNull({"a", "b", "c"}) would be represented by multiple Contracts.

annotation

public final AnnotationMirror annotation

The annotation on the type of expression, according to this contract.

contractAnnotation

public final AnnotationMirror contractAnnotation

The annotation that expressed this contract; used for diagnostic messages.

kind

public final Contract.Kind kind

The kind of contract: precondition, postcondition, or conditional postcondition.

Method Detail

create

public static Contract create(Contract.Kind kind,
                              String expression,
                              AnnotationMirror annotation,
                              AnnotationMirror contractAnnotation,
                              Boolean ensuresQualifierIf)

Creates a new Contract.

Parameters:

kind - precondition, postcondition, or conditional postcondition

expression - the Java expression that should have a type qualifier

annotation - the type qualifier that expression should have

contractAnnotation - the pre- or post-condition annotation that the programmer wrote; used for diagnostic messages

ensuresQualifierIf - the ensuresQualifierIf field, for a conditional postcondition

Returns:

a new contract

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object