|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: REQUIRED | OPTIONAL | DETAIL: ELEMENT |
@Retention(value=RUNTIME) public @interface Implies
This annotation combines other invariant annotations using Boolean implication. The value array has to contain exactly two invariant annotations. Note that this is not compatible with standard Java, but requires xajavac. For more information about xajavac, see http://ricken.us/research/xajavac
Required Element Summary | |
---|---|
InvariantAnnotation[] |
value
|
Element Detail |
---|
public abstract InvariantAnnotation[] value
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: REQUIRED | OPTIONAL | DETAIL: ELEMENT |