org.checkerframework.framework.util

Class ContractsUtils.Precondition

java.lang.Object

org.checkerframework.framework.util.ContractsUtils.Contract

org.checkerframework.framework.util.ContractsUtils.Precondition

Enclosing class:

ContractsUtils

public static class ContractsUtils.Precondition
extends ContractsUtils.Contract

A precondition contract.

Nested Class Summary

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

ContractsUtils.Contract.Kind

Field Summary

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

annotation, contractAnnotation, expression, kind

Constructor Summary

Constructors

Constructor and Description
Precondition(java.lang.String expression, javax.lang.model.element.AnnotationMirror annotation, javax.lang.model.element.AnnotationMirror contractAnnotation) Create a precondition contract.

Method Summary

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

equals, hashCode

Methods inherited from class java.lang.Object

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

Constructor Detail

Precondition

public Precondition(java.lang.String expression,
                    javax.lang.model.element.AnnotationMirror annotation,
                    javax.lang.model.element.AnnotationMirror contractAnnotation)

Create a precondition contract.

Parameters:

expression - the Java expression that should have a type qualifier

annotation - the type qualifier that expression should have

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