org.checkerframework.framework.util

Class Contract.Postcondition

java.lang.Object

org.checkerframework.framework.util.Contract

org.checkerframework.framework.util.Contract.Postcondition

Enclosing class:

Contract

public static class Contract.Postcondition
extends Contract

A postcondition 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, expression, kind

Constructor Summary

Constructors

Constructor and Description
Postcondition(String expression, AnnotationMirror annotation, AnnotationMirror contractAnnotation) Create a postcondition contract.

Method Summary

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

create, equals, hashCode, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

Postcondition

public Postcondition(String expression,
                     AnnotationMirror annotation,
                     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