org.jmlspecs.annotation
Annotation Type InitiallyDefinitions

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

Optional Element Summary

Initially[]

value

value

public abstract Initially[] value

Default:

{}