docs: @Requires("pathName != null")
    @Ensures("result != null")
    public static String getRelativeName(String pathName) {
      int lastSep = pathName.lastIndexOf('.');
      if (lastSep == -1) {
        return pathName;
      } else {
        return pathName.substring(lastSep + 1);
      }
    }