+
Point of view
All features
expanded class XML_DTD_PUBLIC_REPOSITORY
require
-
valid_public_id: not public_id.is_empty
-
valid_url: valid_url(a_url)
-
not_registered: not is_registered(public_id)
ensure
require
-
valid_public_id: not public_id.is_empty
require
- not public_id.is_empty
- not is_registered(public_id) implies a_url /= Void
ensure