Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: REQUIRED | OPTIONAL DETAIL: ELEMENT

org.jmlspecs.annotation
Annotation Type Invariant

@Retention(value=RUNTIME)
@Documented
public @interface Invariant

Optional Element Summary
 java.lang.String header
           
 boolean redundantly
           
 java.lang.String value
           
 

header

public abstract java.lang.String header
Default:
""

redundantly

public abstract boolean redundantly
Default:
false

value

public abstract java.lang.String value
Default:
""
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: REQUIRED | OPTIONAL DETAIL: ELEMENT