org.checkerframework.framework.util

Class ContractsUtils.Postcondition

java.lang.Object

org.checkerframework.framework.util.ContractsUtils.Contract

org.checkerframework.framework.util.ContractsUtils.Postcondition

Enclosing class:

ContractsUtils

public static class ContractsUtils.Postcondition
extends ContractsUtils.Contract

A postcondition 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
Postcondition(java.lang.String expression, javax.lang.model.element.AnnotationMirror annotation, javax.lang.model.element.AnnotationMirror contractAnnotation) Create a postcondition 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

Postcondition

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

Create a postcondition contract.

Parameters:

expression - the Java expression that should have a type qualifier

annotation - the type qualifier that expression should have

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