Annotation Type EnsuresCalledMethods


  • @PostconditionAnnotation(qualifier=CalledMethods.class)
    @Target({METHOD,CONSTRUCTOR})
    public @interface EnsuresCalledMethods
    Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions.

    Consider the following method:

     @EnsuresCalledMethods(value = "#1", methods = "m")
     public void callM(T t) { ... }
     

    This method guarantees that t.m() is always called before the method returns.

    • Required Element Summary

      Required Elements 
      Modifier and Type Required Element Description
      java.lang.String[] methods
      The methods guaranteed to be invoked on the expressions.
      java.lang.String[] value
      The Java expressions to which the qualifier applies.
    • Element Detail

      • value

        java.lang.String[] value
        The Java expressions to which the qualifier applies.
        Returns:
        the Java expressions to which the qualifier applies
        See Also:
        EnsuresQualifier
      • methods

        @QualifierArgument("value")
        java.lang.String[] methods
        The methods guaranteed to be invoked on the expressions.
        Returns:
        the methods guaranteed to be invoked on the expressions