Class Contract.ConditionalPostcondition

Enclosing class:

public static class Contract.ConditionalPostcondition extends Contract
Represents a conditional postcondition that must be verified by BaseTypeVisitor or one of its subclasses. Automatically extracted from annotations with meta-annotation @ConditionalPostconditionAnnotation, such as EnsuresNonNullIf.
  • Field Details

    • resultValue

      public final boolean resultValue
      The return value for the annotated method that ensures that the conditional postcondition holds. For example, given
       @EnsuresNonNullIf(expression="foo", result=false) boolean method()
      foo is guaranteed to be @NonNull after a call to method() that returns false.
  • Constructor Details

    • ConditionalPostcondition

      public ConditionalPostcondition(String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation, boolean resultValue)
      Create a new conditional postcondition.
      expressionString - the Java expression that should have a type qualifier
      annotation - the type qualifier that expressionString should have
      contractAnnotation - the postcondition annotation that the programmer wrote; used for diagnostic messages
      resultValue - whether the condition is the method returning true or false
  • Method Details