11. Library overview

Library classes and methods are documented alphabetically in Appendix A. This section provides an overview of commonly-used operations by category.

11.1 Order and sorting

The built-in class seq of X has a number of members that relate to the ordering of elements. Many of these methods take a parameter of type from Comparator of X. The user may define the ordering required by declaring a class that inherits from Comparator of T (where T is the type of elements concerned) and defines the method compare. Predefined classes inheriting from Comparator of X are SimpleComparator of X (which compares according to the ~~ operator) and ReverseComparator of X (which defines the inverse ordering).

The sequence member isOrdered tests whether a sequence is ordered with respect to a comparator. Functions isndec and isninc are specializations of isOrdered using SimpleComparator and ReverseComparator respectively (so isndec means "is non-decreasing" according to normal element comparison using the "~~" or "<" operator).

Schema sort sorts the sequence so that it is ordered with respect to the given comparator. Functions permndec and permninc return new sequences which are sorted into nondecreasing and nonincreasing order respectively. These functions are also provided as members of classes set of X and bag of X.

11.2 Input/output

The Environment class is the interface through which Perfect programs may interact with the outside world. It is expected that in a future release of Perfect Developer, the environment class will be supplied as a separate library.

All methods referred to in this section are members of class Environment unless otherwise stated.

11.2.1 Console input / output

The print schemas of class Environment output characters to the standard output stream (usually the screen). The printStdErr schema outputs the given string to the standard error stream.

The readLine schema reads a line of text from the standard input stream (usually the keyboard); the value of ret will be either success@FileError, attribError@FileError or otherError@FileError. Note that the final line feed or carriage return + line feed are not returned.

The stdIn, stdOut and stdErr functions return the FileRef objects representing the standard input, output and error streams. In a future version of the library, these methods may return streams instead.

11.2.2 File operations

The open schema attempts to open a file named filename in the mode specified by the mode parameter as follows:

create@FileModeType means a new file is created, and any existing file is deleted
append@FileModeType means the file is opened and data written will be appended to the existing data
read@FileModeType means the file may be read
text@FileModeType means the file is opened as a text file in the underlying operating system, otherwise it is opened as a binary file

The modes create@FileModeType and append@FileModeType are mutually exclusive. At least one of create@FileModeType, append@FileModeType and read@FileModeType must be present.

If the open succeeds a FileRef is returned in the out parameter, otherwise a FileError is returned as follows:

fileNotFound@FileError means the file was not present, and neither append@FileModeType nor create@FileModeType were specified
attribError@FileError means the file was not accessible in the requested mode.

The close schema will attempt to close the given file. ret' will be set to either success@FileError is the close was successful, or writeError@FileError if it failed in some way.

The print schemas output character data to a given file. If the write fails ret' will be equal to writeError@FileError, otherwise it will be success@FileError.

The write schemas output binary data to a given file. The schema taking two int parameters will output the integer n as a sequence of numBytes bytes, most significant byte first. If the integer to be written is too large to fit into the specified number of bytes, the higher bytes will be lost. If the write fails, ret' will be equal to writeError@FileError, otherwise it will be success@FileError.

The scan schemas read character data from a file. If the read succeeds ret' will be equal to success@FileError, otherwise it will be either readError@FileError or endOfFileError@FileError.

The readLine schema attempts to read a line of text from the given file. If successful line' contains the line of text (including the linefeed and/or carriage return if present) and ret' = success@FileError. If the read failed line' is the empty string and ret' = readError@FileError.

The read schemas read binary data from a file. If the read succeeds ret' will be equal to success@FileError, otherwise it will be either readError@FileError or endOfFileError@FileError.

The seek, fastForward and rewind schemas attempt to position the file pointer at a specified position in the file. ret' will be set to either success@FileError is this was successful, or seekError@FileError if it failed in some way.

The fileSize schema returns the size of the data contained in a given file. The schema may change the file pointer of the queried file only if the call fails, in which case res' will be seekError@FileError. If the call succeeds, res' will be success@FileError, and the file pointer will be unchanged.

The tell function returns the position of the file pointer if it succeeds. If the call fails seekError@FileError is returned.

The flush schema attempts to flush any buffer associated with the given file. ret' will be set to success@FileError is the flush was successful, or to flushError@FileError if it failed in some way.

The ghost functions gIsOpen, gFileData, gFilePtr, gFileAtEof and ghost schema gSetFilePtr can be used to reason about the file system.

11.2.3 Disk operations

The makeDirectory schema attempts to create the given directory; all directories below the specified one will also be created if they are not already present. The returned FileError has the following meanings:

success@FileError: the directory was successfully created
permError@FileError: the process did not have permission to create the directory
createError@FileError: a file with the same name as the given directory already existed
diskFull@FileError: insufficient disk space
otherError@FileError: the directory could not be created for some other reason.

The move schema attempts to move and rename the file given by oldPath to that given by newPath. If parameter overwrite is true then if the file newPath already exists it will be replaced by the moved file. The res' parameter will be set to one of the following values:

success@FileError: the move succeeded
fileSpecError@FileError: one or both file names were illegal, or both pointed to the same file
attribError@FileError: the target file already exists, and overwrite is false
deleteError@FileError: the target file already exists and could not be deleted
fileNotFound@FileError: the source file did not exist
otherError@FileError: the move failed in some other way.

The delete schema will attempt to delete the given file. ret' will be set to one of the following values:

success@FileError: the delete succeeded
fileNotFound@FileError: the specified file did not exist
deleteError@FileError: the file could not be deleted.

The fileValid function returns true if the given file and pathname is legal and refers to an existing file or directory.

The fileStatus function returns information on the given file or directory. If the pathname passed ends in the pathSepChar then the call will only succeed if the path represents a directory. If the returned value is of type FileStats, the call succeeded and this is the information. Otherwise the result will be:

fileNotFound@FileError: the file did not exist
directoryNotFound@FileError: the path existed as a file, but the pathname ended in pathSepChar
otherError@FileError: no information could be found for some other reason.

The forceFileTime schema sets the last modified and accessed times on the given file. If either modified or accessed is null, that attribute is not affected. res' will be one of the following values:

success@FileError: the dates were changed successfully
fileNotFound@FileError: the file did not exist
otherError@FileError: failed to change the dates for some other reason

The setMode schema (not implemented in the Java version of the runtime library) attempts to change the file mode flags on the named file. res' will be one of the following values:

success@FileError: the mode was changed successfully
fileNotFound@FileError: the file did not exist
permError@FileError: permission was denied to change mode
otherError@FileError: failed to change mode for some other reason

The getImagePath function returns the full path and file name of the current executable.

The normalizeFile function takes a path and file, and will return a FilePath object corresponding to this file. If the file is not valid, the result is null.

The function getCurrentDirectory returns the current directory in the underlying file system. If the call fails, the result is null. The schema setCurrentDirectory attempts to set the current directory to the specified string; ret will be set to one of the following values:

success@FileError: the directory was successfully changed
directoryNotFound@FileError: the directory did not exist
permError@FileError: the process did not have permission the access the directory
otherError@FileError: the call failed in some other way

The constant caseSensitiveFileNames indicates whether the file system distinguishes between upper and lower case letters. The constant pathSeparator is the character used to separate components of a file name (e.g. `\` in Windows, `/` in Unix).

11.2.4 Opening sockets

The two socket open schemas attempt to open a socket connected to the specified port of the host given either as a string or as an IP address. Returns either the socket if successful, or a socket error if not. Sockets facilitate communication with other machines over a network or the internet.

11.2.5 Other environment methods

schema !(priority: int) pre priority in 1..20

Schema setCurrentThreadPriority sets the priority of the current thread, where 1 is the lowest priority and 20 the highest.

Schema execute (not currently implemented in the Java runtime library) attempts to run the command command on the underlying operating system, passing arguments args, and optionally redirecting standard in, out and error to files. The schema returns when the command has completed, and res will be set as follows:

success@FileError: the command was successfully executed
fileNotFound@FileError: the command did not exist
attribError@FileError: a file of the stated name was found, but was not executable
otherError@FileError: execution failed in some other way

The clock function returns the number of clock ticks since the current executable was started; clocksPerSecond returns the number of clock ticks in a second. Thus, for example, the time in seconds since the current executable started is clock / clocksPerSecond.

Function getCurrentDateTime returns the current date and time as a Time object.

Function getEnvironmentVar returns the value of a given environment variable in the underlying operating system, or null if the variable is not set.

The getImageVersion functions return the version information for the current executable, or named module.

Function getMemoryUsed returns the amount of memory being used by the current executable.

Schema garbageCollect causes the process to return unused memory to the operating system.

Function getOsInfo returns the type and version of the underlying operating system.

11.2.6 Runtime checks and profiling

The setRuntimeOptionState, setRuntimeOption and clrRuntimeOption schemas can be used to change the amount of checking performed at runtime (if runtime checks are being performed at all). Schema setMaxCheckNestLevel determines how deeply checks will be performed. For example, if the setting is 2, runtime check points reached while running the program will be evaluated, also any check points reached whilst evaluating these check points will be evaluated; but runtime check points reached during this second-level evaluation will be skipped.

To perform run-time profiling (only available in certain versions of the C++ runtime library), call schema to begin collecting timing information. Calling schema stopProfiling will suspend the collection of timing information. To write the timing information to file, call schema profile (which implicitly calls stopProfiling) having already created the file. In order to use this mechanism, the macro _dProfile must have been defined as 1 when compiling the generated C++ code.

11.3 Debugging functions

The global function debugPrint is provided to aid debugging, allowing diagnostic information to be output to the console even where no Environment object is available. The return value serves no purpose. Typically, this function will be invoked within a let-statement like this:

let dummy ^= debugPrint("Value of foo is " ++ foo.toString ++ "\n");

The function debugHalt also outputs the given string, but then causes execution to stop with a runtime error.

11.4 Streams

Stream-based input/output is provided by the classes InputStream, OutputStream and their descendents (ByteInputStream, FileInputStream, StandardInputStream and the corresponding output streams).

11.5 Serialization

Declaring a class storable implicitly means it inherits from Storable. This is the only way a class should inherit from Storable, and directly declaring inherits Storable is not allowed.

Storable objects may be stored and re-loaded using the global storeObject and loadObject methods. Note that there is no check that a loaded object satisfies any type constraints or class invariants defined for its class.

The serialization formats used by the C++, C# and Java versions of the runtime system are not compatible with each other.

11.6 Character encoding and decoding

An interface is provided to encode the Perfect char class into a sequence of bytes using a chosen scheme, and to perform to corresponding decoding. It is expected that these will be integrated into the environment print and scan methods in a future release of Perfect Developer.

The base class CharEncoderDecoder serves as an interface for generating encoders and decoders for particular schemes. These encoders and decoders are returned as descendents of CharEncoder and CharDecoder respectively.

An encoder simply contains a function which returns the encoding for any given character, plus a function to return a preamble for the encoding scheme used.

A decoder contains a process schema which is passed bytes until a complete character has been built, at which point the method charReady will return true. The character may then be extracted using getCompletedCharacter, the decoder may then be reset and further characters decoded.