From the JML Ref Manual:
Some syntax from the Universe type system (see section 18. Universe Type
System) is included in level 0. However, readonly is considered to be in
level X, as is the semantics of the Universe type system. The rep and peer
modifiers are included in level 0 because, in some form, they are
important
to the semantics of several level 0 features
[Mueller-Poetzsch-Heffter-Leavens03] [Mueller-Poetzsch-Heffter-Leavens06].
The \rep and rep ownership-modifiers (see section 18.2 Rep and Peer).
The \peer and peer ownership-modifiers (see section 18.2 Rep and Peer).