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.RetentionPolicy;
008    import java.lang.annotation.Retention;
009    
010    /**
011     * This annotation combines other invariant annotations using Boolean implication.
012     * The value array has to contain exactly two invariant annotations.
013     *
014     * Note that this is not compatible with standard Java, but requires xajavac.
015     * For more information about xajavac, see http://ricken.us/research/xajavac
016     *
017     * @author Mathias Ricken
018     */
019    @Retention(RetentionPolicy.RUNTIME)
020    @PredicateLink(value= Predicates.class, method="checkImplies", arguments=true)
021    public @interface Implies extends InvariantAnnotation {
022        public abstract InvariantAnnotation[] value();
023    }