001    package edu.rice.cs.cunit.threadCheck.subAnnot.predicates;
002    
003    import edu.rice.cs.cunit.threadCheck.subAnnot.PredicateLink;
004    import edu.rice.cs.cunit.threadCheck.subAnnot.Predicates;
005    import edu.rice.cs.cunit.threadCheck.subAnnot.InvariantAnnotation;
006    
007    import java.lang.annotation.ElementType;
008    import java.lang.annotation.Retention;
009    import java.lang.annotation.RetentionPolicy;
010    import java.lang.annotation.Target;
011    
012    /**
013     * An annotation used to designate methods that are only allowed to be run when the
014     * method argument indexed by value is null.
015     * @author Mathias Ricken
016     */
017    @Retention(RetentionPolicy.RUNTIME)
018    @Target({ElementType.CONSTRUCTOR,ElementType.METHOD,ElementType.TYPE})
019    
020    @PredicateLink(value = Predicates.class, method = "checkNumberBoundedArgument", arguments = true)
021    public @interface NumberBoundedArgument extends InvariantAnnotation {
022        /**
023         * Mode of bounding.
024         */
025        public static enum Mode {
026            /**
027             * Number must be less than bound.
028             */
029            LESS,
030    
031            /**
032             * Number must be less than or equal to bound.
033             */
034            LESS_EQ,
035    
036            /**
037             * Number must be greater than bound.
038             */
039            GREATER,
040    
041            /**
042             * Number must be greater than or bound.
043             */
044            GREATER_EQ,
045    
046            /**
047             * Number must be less than or equal to upperBound and greater than or equal to bound.
048             */
049            IN_EQ,
050    
051            /**
052             * Number must be less than upperBound and less than bound.
053             */
054            IN,
055    
056            /**
057             * Number must be greater than or equal to upperBound or less than or equal to bound.
058             */
059            OUT_EQ,
060    
061            /**
062             * Number must be greater than upperBbound or less than bound.
063             */
064            OUT
065        }
066    
067        /**
068         * Class containing the predicate method.
069         * @return class containing the predicate method.
070         */
071        Mode mode();
072    
073        /**
074         * Index of the method argument.
075         * @return index of the method argument to be bounded
076         */
077        int index();
078    
079        /**
080         * Lower bound.
081         * @return the lower bound for the comparison.
082         */
083        double bound();
084    
085        /**
086         * Upper bound.
087         * @return the upper bound for the comparison, only used for IN_EQ, IN, OUT_EQ and OUT
088         */
089        double upperBound() default 0;
090    }