org.checkerframework.framework.util

Class ContractsUtils

java.lang.Object

org.checkerframework.framework.util.ContractsUtils

public class ContractsUtils
extends Object

A utility class to handle pre- and postconditions.

Author:

Stefan Heule

See Also:

PreconditionAnnotation, RequiresQualifier, PostconditionAnnotation, EnsuresQualifier, EnsuresQualifierIf

Field Summary

Fields

Modifier and Type	Field and Description
protected GenericAnnotatedTypeFactory<?,?,?,?>	factory
protected static ContractsUtils	instance

Method Summary

Modifier and Type	Method and Description
Set<Pair<String,Pair<Boolean,String>>>	getConditionalPostconditions(ExecutableElement methodElement) Returns a set of triples (expr, (result, annotation)) of conditional postconditions on the method methodElement.
static ContractsUtils	getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory) Returns an instance of the ContractsUtils class.
Set<Pair<String,String>>	getPostconditions(ExecutableElement methodElement) Returns a set of pairs (expr, annotation) of postconditions on the method methodElement.
Set<Pair<String,String>>	getPreconditions(Element element) Returns a set of pairs (expr, annotation) of preconditions on the element element.

Methods inherited from class java.lang.Object

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

Field Detail

instance

protected static ContractsUtils instance

factory

protected GenericAnnotatedTypeFactory<?,?,?,?> factory

Method Detail

getInstance

public static ContractsUtils getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)

Returns an instance of the ContractsUtils class.

getPreconditions

public Set<Pair<String,String>> getPreconditions(Element element)

Returns a set of pairs (expr, annotation) of preconditions on the element element.

getPostconditions

public Set<Pair<String,String>> getPostconditions(ExecutableElement methodElement)

Returns a set of pairs (expr, annotation) of postconditions on the method methodElement.

getConditionalPostconditions

public Set<Pair<String,Pair<Boolean,String>>> getConditionalPostconditions(ExecutableElement methodElement)

Returns a set of triples (expr, (result, annotation)) of conditional postconditions on the method methodElement.