Package org.checkerframework.framework.testchecker.util

Annotation Interface EnsuresOddIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=Odd.class) @InheritedAnnotation public @interface EnsuresOddIf
A conditional postcondition annotation to indicate that a method ensures certain expressions to be Odd given a certain result (either true or false).

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
     
    boolean
    result
     

  • Element Details

    • result

      boolean result

    • expression

      String[] expression