The version of the Z notation used here is the ZSL language developed by Xiaoping Jia at dePaul University. Since the type checker only interprets lines beginning with a tab character, it is easy to write a combination HTML and ZSL file.
Restriction has two flavours for role and attribute.
Roles are multi-valued and concepts may be described by the arity of roles, so we get the minumum and maximum restriction combinators applying to roles only. Since attributes are just single-valued roles, their interpretations are functions instead of relations. The extension of a value restriction is all those objects that have the specified role filled with an object in the extension of the specified concept. This section describes description graphs. The definition is recursive, so we must first describe DescrGraph as a given set, then redefine it when we have all the pieces in place.