SIGNATURE UserAndGroup

-- user and group management

IMPORT
  Denotation          ONLY < : denotation**denotation->bool
  Option[user]        ONLY option: SORT
  Option[group]       ONLY option: SORT
  Set[denotation,<]   ONLY set: SORT
  Set[groupid,<]      ONLY set: SORT
  Com[option[user]]   ONLY com: SORT
  Com[option[group]]  ONLY com: SORT
  Com[set[groupid,<]] ONLY com: SORT

-- user (passwd entry) management

SORT userid
FUN  < = : userid ** userid -> bool
            -- orderings

SORT user
FUN  < = : user ** user -> bool
           -- orderings (derived from userid orderings)
FUN  userName : user -> denotation             -- user name
     userId   : user -> userid                 -- user ID
     iGroupId : user -> groupid                -- initial group ID
     homeDir  : user -> denotation             -- initial working directory
     shell    : user -> denotation             -- initial user program

FUN getUser : userid     -> com[option[user]]
              -- lookup user (passwd entry) by ID, see POSIX getpwuid()
    getUser : denotation -> com[option[user]]
              -- lookup user (passwd entry) by user name, see POSIX getpwnam()

-- group management

SORT groupid
FUN  < = : groupid ** groupid -> bool
           -- orderings

SORT group
FUN  < = : group ** group -> bool
           -- orderings (derived from groupid orderings)
FUN  groupName    : group -> denotation        -- group name
     groupId      : group -> groupid           -- group ID
     groupMembers : group -> set[denotation,<] -- user names of members

FUN getGroup : groupid    -> com[option[group]]
               -- lookup group by ID, see POSIX getgrgid()
    getGroup : denotation -> com[option[group]]
               -- lookup group by name, see POSIX getgrnam()

FUN getGroups : com[set[groupid,<]]
                -- return supplementary groups, see POSIX getgroups()
                -- NOTE: may or may not contain the effective GID of
                --       the calling process! Consult the manual.