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 monitor of
014     * the field specified by class and field name is owned by some thread, regardless which it is.
015     *
016     * @author Mathias Ricken
017     */
018    @Retention(RetentionPolicy.RUNTIME)
019    @Target({ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE})
020    
021    @PredicateLink(value = Predicates.class, method = "checkSynchronizedField")
022    public @interface SynchronizedField extends InvariantAnnotation {
023        /**
024         * The class that contains the field whose monitor some thread has to own.
025         *
026         * @return class containing the field
027         */
028        Class fieldClass();
029    
030        /**
031         * The name of the field whose monitor sine thread has to own.
032         *
033         * @return name of the field
034         */
035        String fieldName();
036    
037        //
038        // nested interfaces
039        //
040    
041        /**
042         * An annotation used to designate methods that are only allowed to be run when the monitor of
043         * the field specified by class name and field name is owned by some thread, regardless which it is.
044         *
045         * @author Mathias Ricken
046         */
047        @Retention(RetentionPolicy.RUNTIME)
048        @Target({ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE})
049        
050        @PredicateLink(value = Predicates.class, method = "checkSynchronizedFieldByName")
051        public @interface ByName extends InvariantAnnotation {
052            /**
053             * The name of the class that contains the field whose monitor some thread has to own.
054             *
055             * @return class containing the field
056             */
057            String fieldClassName();
058    
059            /**
060             * The name of the field whose monitor the thread some to own.
061             *
062             * @return name of the field
063             */
064            String fieldName();
065        }
066    }