org.jmlspecs.annotation
Annotation Type InvariantDefinitions

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

Optional Element Summary

Invariant[]

value

value

public abstract Invariant[] value

Default:

{}