org.checkerframework.framework.util

Class Contract.Precondition

java.lang.Object

org.checkerframework.framework.util.Contract

org.checkerframework.framework.util.Contract.Precondition

Enclosing class:

Contract

public static class Contract.Precondition
extends Contract

A precondition contract.

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.framework.util.Contract

Contract.ConditionalPostcondition, Contract.Kind, Contract.Postcondition, Contract.Precondition

Field Summary

Fields inherited from class org.checkerframework.framework.util.Contract

annotation, contractAnnotation, expressionString, kind

Constructor Summary

Constructors

Constructor and Description
Precondition(String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation) Create a precondition contract.

Method Summary

Methods inherited from class org.checkerframework.framework.util.Contract

create, equals, hashCode, toString, viewpointAdaptDependentTypeAnnotation

Methods inherited from class java.lang.Object

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

Constructor Detail

Precondition

public Precondition(String expressionString,
                    AnnotationMirror annotation,
                    AnnotationMirror contractAnnotation)

Create a precondition contract.

Parameters:

expressionString - the Java expression that should have a type qualifier

annotation - the type qualifier that expressionString should have

contractAnnotation - the precondition annotation that the programmer wrote; used for diagnostic messages