001    package edu.rice.cs.cunit.threadCheck;
002    
003    import java.lang.annotation.Retention;
004    import java.lang.annotation.RetentionPolicy;
005    import java.lang.annotation.Target;
006    import java.lang.annotation.ElementType;
007    
008    /**
009     * Meta-annotation that specifies what Boolean operation is used to combine the predicate annotations
010     * contained in the annotation that is annotated by this meta-annotation.
011     *
012     * The @Combine meta-annotation lets the Thread Checker know that the annotation interface annotated with
013     * it is intended to be processed by the Thread Checker. If an annotation interface is intended to be
014     * a Thread Checker annotation and it contains annotations or arrays of annotations as members, then
015     * the annotations used must also be Thread Checker annotations, and the annotation interface must be
016     * annotated with the @Combine meta-annotation.
017     *
018     * An annotation interface annotated with @Combine may not contain members that are not annotations or
019     * arrays of annotations, and those annotation interfaces must themselves be Thread Checker annotations.
020     * 
021     * The @PredicateLink and @Combine meta-annotations are mutually exclusive.
022     * @author Mathias Ricken
023     */
024    @Retention(RetentionPolicy.RUNTIME)
025    @Target({ElementType.ANNOTATION_TYPE})
026    public @interface Combine {
027        /**
028         * Boolean operation used to combine the results of other predicates.
029         */
030        public static enum Mode {
031            /**
032             * Combine results of predicates using AND.
033             */
034            AND,
035    
036            /**
037             * Combine results of predicates using OR.
038             */
039            OR,
040    
041            /**
042             * Results in TRUE when one and only one of the operands is TRUE. It follows the true meaning of
043             * "exclusive or".
044             *
045             * (a XOR b XOR c) is therefore equivalent to
046             * (a AND (NOT b) AND (NOT c)) OR ((NOT a) AND b AND (NOT c)) OR ((NOT a) AND (NOT b) AND c)
047             */
048            XOR,
049    
050            /**
051             * Invert result of predicate result. This is intended to be applied to only one predicate annotation.
052             */
053            NOT,
054    
055            /**
056             * Implication. This is intended to be applied to exactly one array of two predicate annotation.
057             * It is necessary to have an array of two predicate annotations, because implication is defined
058             * only with two operands, and without the array, we would not be able to guarantee consistent
059             * ordering as required by the non-commutable implication operation.
060             */
061            IMPLIES
062        }
063    
064        /**
065         * Class containing the predicate method.
066         * @return class containing the predicate method.
067         */
068        Mode value() default Mode.OR;
069    
070        /**
071         * Whether the method arguments should be passed as well, after the value of "this" and
072         * before the annotation values.
073         * @return true if method arguments should be passed
074         */
075        boolean arguments() default false;
076    }