JML specification of
Collection
JML specification of
Iterator