Interprets <time> as a time, using the same representation as given in the description of `time()', and converts it into a 28-character, human-readable string in the following format:
Mon Aug 13 19:13:20 1990 PDT
If the current day of the month is less than 10, then an extra blank appears between the month and the day:
Mon Apr 1 14:10:43 1991 PST
If <time> is not provided, then the current time is used.
Note that `ctime()' interprets <time> for the local time zone of the computer on which the MOO server is running.