Appendix A: Library Reference

A1. Global methods

The following global methods are defined. Some or all of these may be replaced by nonmember class methods in future versions of the library.

function debugPrint(s: string): bool

  ^= ?;		 Prints the string to standard output as an unspecified side-effect.

function debugHalt(s: string): bool

  ^= ?;		 Prints the string to standard output as an unspecified side-effect, then halts the program (possibly loading a debugger, if available).

function flatten(s: seq of seq of class X): seq of X

  ^= ( [s.empty]:
          seq of X{},
        []:
          ++over s
      );		 Converts a sequence of sequences to a single sequence by concatenating all the components. Equivalent to using ++ over except that the operand is allowed to be empty.

function flatten(s: set of set of class X): set of X

  require X has operator =(arg) end
  ^= ( [s.empty]:
          set of X{},
        []:
          ++ over s
      );		 Converts a set of sets to a single set by uniting all the components. Equivalent to using ++ over except that the operand is allowed to be empty.

function flatten(b: bag of bag of class X): bag of X

  require X has operator =(arg) end
  ^= ( [b.empty]:
          bag of X{},
        []:
          ++ over b
      );		 Converts a bag of bags to a single bag by uniting all the components. Equivalent to using ++ over except that the operand is allowed to be empty.

function interleave(s: seq of seq of class X, t: seq of X): seq of X

  ^= ( [s.empty]:
          seq of X{},
        []:
          s.head ++ flatten(for x::s.tail yield t ++ x)
      )
  assert #s ~= 0 & #t ~= 0 ==> #result ~= 0;		 Similar to flatten but inserts the element t between elements of s. Especially useful for converting a sequence of strings to a single string for printing, inserting a separator (e.g. comma or newline) between the elements.

function loadObject (env: Environment, strm: from InputStream, minVersion, maxVersion: nat): (from Storable) || SerialError

  ^= ?;		 Attempts to load an object from the stream. Returns the object retrieved if successful, otherwise the reason for the failure.

function max(a, b: class X): X

  ^= ([a ~~ b = rank below]: b, []: a);		 If the two parameters rank same, returns the first one.

function max(a, b: class X, repeated c: X): X

  ^= max(max(a, b), c.max);		  

function min(a, b: class X): X

  ^= ([a ~~ b = rank above]: b, []: a);		 If the two parameters rank same, returns the first one.

function min(a, b: class X, repeated c: X): X

  ^= min(min(a,b), c.min);		  

schema storeObject (obj: from Storable, env!: limited Environment, strm: from OutputStream, version: nat, err!: out SerialError || void)

  post ?;		 Stores the specified object to the stream. The err parameter is set to null if successful, otherwise it holds the reason for the failure.

schema swap(x!, y!: class X)

  post x!= y, y!= x;		 Swaps the values of the two parameters. May be more efficient for some data types on some platforms than using x! = y, y! = x directly.


 

A2. Classes

All of these classes inherit from class anything, except for classes anything and void.

Variables are only mentioned if they are public or are referred to in the specifications.

The ancestors given in the inherits parts are not necessarily the direct ancestors of the classes concerned, since additional classes may be inserted in the inheritance chain for implementation reasons, or for future extension.

For enumeration classes other than rank, additional values may be inserted or appended in future versions of the library. The toString method of each enumeration class is redefined in the usual way, but not shown here.

anything
deferred class anything This is ancestor of all classes defined in Perfect (whether by the user or by the system) unless declared public or external

Methods
function toString: string
  decrease ?
  ^= ?;		 Return a textual representation of the value of the object. The default returns the string "No output string specified for this type" or similar. It should be overridden in any class for which toString is likely to be called. Recursive definitions of toString are allowed.

 

bag of X
final class bag of X
A bag is an unordered collection of values. Duplicate values are permitted and significant.

Constructors
build{}
  post ?
  assert result.empty;		 Builds an empty bag
build{repeated x: X}
  post ?;		 Builds a bag containing the values in the parameter list

Methods
operator (a: X)#: nat
  require X has operator =(arg) end
  ^= #(those x::self :- x = a);		 Returns the number times the given value occurs in the bag
operator (a: X) in: bool
  require X has operator =(arg) end
  ^= a in ran;		 Returns true if the bag contains the parameter
operator #: nat
  ^= ?;		 Returns the number of elements in the bag
operator **(a: bag of X): bag of X
  require X has operator =(arg) end
  satisfy forall x:X :- x # result = min(x # self, x # a);		 Returns the intersection of the bag with the parameter
operator ##(a: bag of X): bool
  require X has operator =(arg) end
  ^= forall x::self :- x ~in a;		 Returns true if the bag is disjoint with the parameter
operator ++(a: bag of X): bag of X
  satisfy forall x:X :- x # result = x # self + x # a;		 Returns the union of the bag with the parameter
operator --(a: bag of X): bag of X
  require X has operator =(arg) end   satisfy forall x:X :- x # result = max(x # self - x # a, 0);		 Returns the difference between the bag and the parameter
operator <<=(a: bag of X): bool
  require X has operator =(arg) end
  ^= forall x::self :- x # self <= x # a;		 Returns true if the bag is a sub-bag of the parameter
operator <<(a: bag of X):bool
  require X has operator =(arg) end
  ^= self <<= a & #self < #a;		 Returns true if the bag is a strict sub-bag of the parameter
function append(a: X): bag of X
  satisfy result >> self,
    #result = >#self,
    forall x::result :- x # result = ([x = a]: >(x # self), [x ~= a]: x # self);		 Returns a new bag like the original but with one more instance of the parameter adjoined
function empty: bool
  ^= #self = 0;		 Returnstrue if the bag is empty
function max: X
  require X has total operator ~~(arg) end
  pre ~empty
  ^= that x::self :- forall y::self :- (x ~~ y) ~= rank below;		 Returns the highest element in the bag
function min: X
  require X has total operator ~~(arg) end
  pre ~empty
  ^= that x::self :- forall y::self :- (x ~~ y) ~= rank above;		 Returns the lowest element in the bag
opaque function omax: X
  pre ~empty
  ^= any x::self :- forall y::self :- (x ~~ y) ~= rank below;		 Returns a highest element in the bag. If the element type has a total ordering, you should use max instead.
opaque function omin: X
  pre ~empty
  ^= any x::self :- forall y::self :- (x ~~ y) ~= rank above;		 Returns a lowest element in the bag. If the element type has a total ordering, you should use min instead.
opaque function opermndec: seq of X
  satisfy result .ranb = self,
    result.isndec;		 Returns a sequence comprising the elements of the bag in a nondecreasing order. If the element type has a total ordering, you should use permndec instead.
opaque function opermninc: seq of X
  satisfy result .ranb = self,
    result.isninc;		 Returns a sequence comprising the elements of the bag in a nonincreasing order. If the element type has a total ordering, you should use permninc instead.
function permndec: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb = self,
    result.isndec;		 Returns the sequence comprising the elements of the bag in a nondecreasing order
function permninc: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb = self,
    result.isninc;		 Returns the sequence comprising the elements of the bag in a nonincreasing order
function ran: set of X
  require X has operator =(arg) end
  satisfy forall x:X :- x in result <==> x in self;		 Converts the bag to a set by removing duplicates
function remove(a: X): bag of X
  require X has operator =(arg) end
  satisfy ([a in self]: a # result = <(a # self) & result .append(a) = self, [a ~in self]: result = self);		 Returns a new bag like the original except that if there were one or more instances of the parameter in the bag, the result contains one fewer instance
function rep(a: nat): bag of X
  satisfy result .ran = self.ran,
    forall x::self :- x # result = a * (x # self)		 Returns a new bag in which each element of the original is replicated the number of times given by the parameter
redefine function toString: string
  ^= ?;		 Returns a textual representation of the bag
function unique: bool
  require X has operator =(arg) end
  ^= forall x::self :- x # self = 1;		 Returns true if the bag contains no repeated values

 

bool
final class bool The Boolean type has values true and false.

Methods
operator &(arg: bool) Equivalent (except for precedence) to: ([~self]: false, []: arg)
operator | (arg: bool) Equivalent (except for precedence) to: ([self]: true, []: arg)
operator ==> (arg: bool) Equivalent (except for precedence) to: ~self | arg
operator <== (arg: bool) Equivalent (except for precedence) to: self | ~arg
operator <==> (arg: bool) Equivalent (except for precedence) to: self = arg
redefine function toString
  ^= ([self]: "true", []: "false);		  

 

byte
final class byte Represents an 8-bit byte. Used primarily for reading and writing streams and files.

Constructors
build {bits: seq of bool}
  pre #bits = 8;
 		 Constructs a byte from 8 bits (the most significant bit istheBits[0])
build{arg: nat}
  pre arg < 256
  ^= byte
      { seq of bool
        { arg >= 128,
          (arg % 128) >= 64,
          (arg % 64) >= 32,
          (arg % 32) >= 16,
          (arg % 16) >= 8,
          (arg % 8) >= 4,
          (arg % 4) >= 2,
          (arg % 2) = 1
        }
      }
  assert +result = arg;		 Constructs the byte representing the given number.

Methods
operator +: nat
  ^= ?
  assert result < 256,
    byte{result} = self;		 Returns the interpretation of the byte as an unsigned integer.
total operator ~~(a) ^= +self ~~ +a;  
operator .. (b: byte): seq of byte
  ^= ([b >= self ]: (self .. <b).append(b), [b < self]:seq of byte {})
  assert result.isndec;		  
operator >: byte
  pre self ~= byte {255
  ^= byte{>+self};		  
operator <: byte
  pre self ~= byte{0
  ^= byte{<+self};		  
function and(arg: byte): byte
  ^= byte{for i::0..7 yield theBits[i] & arg.theBits[i]};		  
function or (arg: byte): byte
  ^= byte{for i::0.. 7 yield theBits[i] | arg.theBits[i]};		  
function compl: byte
  ^= byte {for i::0.. 7 yield ~theBits[i]};		  
function shl(arg: nat): byte
  pre arg < 8
  ^= byte{theBits.drop(8) ++ seq of bool{false }.rep(arg)};		  
function shr(arg: nat): byte
  pre arg < 8
  ^= byte{seq of bool{false}.rep(arg) ++ theBits.take(8-arg)};		  
redefine function toString: string
  ^= (+self).toString;		  

 

ByteData
final class ByteData A memory buffer that can be used for stream input/output

Data
var bytes: seq of byte The data held
var index: nat The index of the next byte to be read

Invariants
index <= #bytes  

Constructors
build{}
  post bytes! = seq of byte{};		 Builds an empty ByteData
build{!bytes: seq of byte}; Builds a ByteData from a byte array

Methods
function eof: bool
  ^= index = #bytes;		 Returns true if there are no more bytes to be read
schema !get(b!: out byte)
  pre ~eof
  post b! = bytes[tell],
    index! + 1;		 Retrieves the next byte and advances the pointer
schema !get(sb!: out seq of byte, len: nat)
  pre index + len <= #bytes
  post  sb! = bytes.slice(streamPos, len), streamPos! + len;		 Retrieves the specified number of bytes
schema !put(b: byte)
  post bytes! = bytes.append(b), streamPos! + 1;		  
schema !put(sb: seq of byte)
  post bytes! ++ sb;		  
function size: nat
  ^= #bytes;		  

 

ByteInputStream
class ByteInputStream ^= inherits InputStream An input stream that reads from data in memory

Constructors
build {!bytes: ref ByteData on StreamHeap}
  inherits InputStream{};		 Builds a ByteInputStream from a reference to a ByteData object

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream.
define ghost function gStreamData: seq of byte
  ^= bytes.value.bytes;		 The data held by the stream
define ghost function gStreamPtr: nat
  ^= bytes.value .tell;		 The index of the next element to be read
define ghost function gStreamAtEnd: bool
  ^= ?;		 Returns true if there are no more bytes to be read
define schema !read(b!: out byte, ret!: out FileError)
  post ?;		 Reads a byte from the stream
schema !read(s!: out seq of byte, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream
schema !read(n!: out int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream
schema !read(c!: out char, decoder!: limited from CharDecoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream
schema !read(r!: out real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream

 

ByteOutputStream
final class ByteOutputStream ^= inherits OutputStream An output stream that writes to an area of memory

Constructors
build {!bytes: ref ByteData on StreamHeap}inherits OutputStream{}; Builds a ByteOutputStream from a reference to a ByteData object

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream.
define schema !flush
  post pass;		  
define schema !write(b: byte, ret!: out FileError)
  post ?;		 Appends the byte to the memory buffer
define ghost function gStreamData: seq of byte
  ^= bytes.value.bytes;		 The data in the memory buffer
schema !write(s: seq of byte, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream
schema !write(i: int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class OutputStream
schema !write(c: char, encoder: from CharEncoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream
schema !write(r: real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream

 

char
final class char Represents a single character. When compiling to Java, the character set is Unicode; when compiling to C++ it may be a variant of ASCII, or (depending on code generation options chosen) Unicode.

Constructors
build{n: nat}
  post ?
  assert +self' = n;		 Constructs the character whose numeric value in the supported character set is equal to n.

Methods
total operator ~~(a)
  ^= +self ~~ +a;		 Defines a total ordering of between characters
operator .. (b: char) :seq of char
  ^= ([b >= self ]: (self ..<b).append(b), [b < self]:seq of char {})
    assert result.isndec;		  
operator >: char
  ^= char {>+self};		  
operator <: char
  ^= char {<+self};		  
operator +: nat
  ^= ?
  assert char{result } = self;		 Returns the numeric value of the character in the supported character set
function isLetter: bool
  ^= ?
  assert result ==> isPrintable, isDigit ==> ~result,
    self in " !\"$%^&*()-_=+[]{};:'@#~,<.>/?\\|`" ==> ~ result,
    self in "abcdefghijklmnopqrstuvwxyz" ++ "ABCDEFGHIJKLMNOPQRSTUVWXYZ" ==> result;		 Returns true if the character is a letter.
function isLowerCase: bool ^= ?
  assert result ==> isLetter,
    result ==> ~isUpperCase,
    isDigit ==> ~result,
    self in " !\"$%^&*()-_=+[]{};:'@#~,<.>/?\\|`" ==> ~ result,
    self in "ABCDEFGHIJKLMNOPQRSTUVWXYZ" ==> ~result,
    self in "abcdefghijklmnopqrstuvwxyz" ==> result;		 Returns true if the character is a lower case letter.
function isUpperCase: bool ^= ?
  assert result ==> isLetter,
    result ==> ~isLowerCase,
    isDigit ==> ~result,
    self in " !\"$%^&*()-_=+[]{};:'@#~,<.>/?\\|`" ==> ~ result,
    self in "ABCDEFGHIJKLMNOPQRSTUVWXYZ" ==> result,
    self in "abcdefghijklmnopqrstuvwxyz" ==> ~result;		 Returns true if the character is an upper case letter.
function isDigit: bool
  ^= self in "0123456789";		 Returns true if the character is a digit.
function isPrintable: bool
  ^= ?
  assert isLetter ==> result,
    isDigit ==> result,
    self in " !\"$%^&*()-_=+[]{};:'@#~,<.>/?\\|`" ==> result;		 Returns true if the character is printable or a normal space (i.e. not a control character)..
function digit: int
  pre isDigit
  ^= ?
  assert 0 <= result < 10,
    self = `0` <==> result = 0,
    self = `1` <==> result = 1,
    self = `2` <==> result = 2,
    self = `3` <==> result = 3,
    self = `4` <==> result = 4,
    self = `5` <==> result = 5,
    self = `6` <==> result = 6,
    self = `7` <==> result = 7,
    self = `8` <==> result = 8,
    self = `9` <==> result = 9;		 Converts the character to the number it represents.
function toLowerCase: char
  ^= ?
  assert self .isUpperCase ==> result.isLowerCase,
    ~self .isUpperCase ==> result = self;		 Returns the lower case version of the character, it it is an upper case character; otherwise returns the character unchanged.
redefine function toString: string
  ^= string{self };		  
function toUpperCase: char
  ^= ?
  assert self .isLowerCase ==> result.isUpperCase,
    ~self .isLowerCase ==> result = self;		 Returns the upper case version of the character, it it is a lower case character; otherwise returns the character unchanged.

 

CharDecoder
deferred class CharDecoder ^= inherits CharEncoderDecoder  

Constructors
build{}
  inherits CharEncoderDecoder{};		  

Methods
deferred function charReady: bool; Returns true if the decoder has a completed character.
final ghost function decode(input: seq of byte):string
  decrease #input
  ^= ( let temp ^= getFirstChar(input);
        [temp = null]:
          string{},
        []:
          decode((temp is pair of (char, seq of byte)).y).prepend((temp is pair of (char, seq of byte)).x)
      );		 Expresses the result of decoding a sequence of bytes.
deferred function getCompletedCharacter: char
  pre charReady;		 Retrieves the completed character.
final ghost function getFirstChar(input: seq of byte): pair of (char, seq of byte) || void
  decrease #input
  ^= ( [#input = 0]:
          null as pair of (char, seq of byte) || void,
        []:
          ( let temp ^= self after it!process(input.head);
            [temp.charReady]:
              pair of (char, seq of byte) {temp.getCompletedCharacter, input.tail},
            []:
              temp.getFirstChar(input.tail)
          )
      )
  assert result ~= null ==> #(result is pair of (char, seq of byte)).y < #input;		 Decodes the next character from a byte string. Returns null if the end of the string is reached first, else the character and the rest of the input byte string.
deferred schema !process(bb: byte); Consumes the byte, possibly giving rise to a completed character
final ghost schema !process(sb: seq of byte)
decrease #sb
post ( [~sb.empty]:
            !process(sb.head) then !process(sb.tail),
          []
        );		 Expresses the effect of consuming a sequence of bytes
deferred schema !reset; Resets the decoder, ready to decode the next encoded character. This saves having to build a new decoder every time another character is to be decoded.

 

CharEncoder
deferred class CharEncoder ^= inherits CharEncoderDecoder  

Constructors
build{}
  inherits CharEncoderDecoder{};		  

Methods
deferred function encode(c: char): seq of byte; Encodes a character into a byte sequence
final ghost function encode(input: string): seq of byte
decrease #input
  ^= ( [input.empty]:
          seq of byte{},
        []:
          encode(input.head) ++ encode(input.tail)
      );		 Expresses the byte sequence generated if an entire character string is encoded.
deferred function preamble: seq of byte; Returns the Byte Order Mark (if any) to generate at the start of a text file or stream.

 

CharEncoderDecoder
class CharEncoderDecoder  

Data
const encodingTable: map of (string -> pair of (from CharEncoder, from CharDecoder)) ^= ?; A table of character set names and the corresponding encoders and decoders.

Constructors
build{};  

Methods
nonmember function getDecoder(s: string): from CharDecoder || void
  ^= ( [isRecognisedEncoding(s)]:
          encodingTable[s].yas from CharDecoder || void,
        []:
          null
      )
  assert isRecognisedEncoding(s) ==> result ~= null;		 Returns the decoder for the specified character set, or null if the character set name is not recognized.
nonmember function getEncoder(s: string): from CharEncoder || void
  ^= ( [isRecognisedEncoding(s)]:
          encodingTable[s].xas from CharEncoder || void,
        []:
          null
      )
  assert isRecognisedEncoding(s) ==> result ~= null;		 Returns the encoder for the specified character set, or null if the character set name is not recognized.
nonmember function isRecognisedEncoding(s: string ):bool
  ^= s in encodingTable
  assert s in set of string{"ascii", "utf8", ""} ==> result;		 Indicates whether the character set name is recognized. ASCII (7-bit) and UFT8 character sets are always recognized. [Note: support for UTF8 may be incomplete on platforms that use an 8-bit character set.]

 

Comparator of X
deferred class Comparator of X Base class for constructing an object to compare two values of type X. Used as a parameter to some of the ordering and sorting methods for the built-in collection classes.

Constructors
build{};  

Methods
deferred function compare(a, b: X): rank; This must be defined in descendent classes to specify the ordering required. The definition must satisfy the symmetry and transitivity properties.
final function notLessThan(a, b: X): bool
  ^= compare(a, b) ~= rank below;		  

Properties
property (a, b: X)
  assert compare(a, b) = rank same <==> compare(b, a) = rank same,
    compare(a, b) = rank below <==> compare(b, a) = rank above;		 These symmetry properties must be obeyed by the definition of 'compare' in a descendent class
property(a, b, c: X)
  assert compare(a, b) = rank same ==> compare(a, c) = compare(b, c),
    compare(a, b) = rank below & compare(b, c) = rank below ==> compare(a, c) = rank below;		 These transitivity properties must be obeyed by the definition of 'compare' in a descendent class

 

DebugType
class DebugType ^= enum preConditions, postConditions, loopInvariants, loopVariants, specVariants, impVariants, embAsserts, postAsserts, lastChoices, classInvariants, constraints end Enumeration for control of runtime debug checks. Each of these will only be effective when running a debug build that had the relevant check enabled at build time.

 

Environment
final class Environment external Class to describe the interface with the operating system

Data
class File ^=
abstract
  var idata: seq of byte,
    iptr: nat;
  invariant iptr <= #idata;
interface
  ghost selector data: seq of byte ^= idata;
  ghost selector fileptr: nat ^= iptr;
  ghost function atEof: bool ^= fileptr = #data;
end;

var openFiles: map of (FileHandle -> File),
    stdInStream: StandardInputStream,
    stdOutStream, stdErrStream: StandardOutputStream;

const pathSeparator: char ^= ?;
const caseSensitiveFileNames: bool ^= ?;
function pathSeparator, caseSensitiveFileNames;		  

Methods
function clock: nat
  ^= ?;		 Returns the number of clock ticks since the program started. Depending on platform, this may be either CPU time consumed or elapsed time.
function clocksPerSecond: nat ^= ?
  assert result >= 1;		 Returns the number of clock ticks per second.
schema !close(f: FileRef, ret!: out FileError)
pre gIsOpen(f)
post change openFiles, ret
  satisfy (ret' = FileError success ==> openFiles' = openFiles.remove(f.handle)),
    (ret' ~= FileError success) ==> openFiles' = openFiles;		 Closed the file identified by the given file reference
schema !clrRuntimeOption(debOpt: DebugType)
  post !setRuntimeOptionState(debOpt, false);		 Disables debug checks of the specified type
schema !clrRuntimeOptions(debOpts: set of DebugType)
  post !setRuntimeOptionsState(debOpts, false);		 Disables debug checks of the specified types
schema !delete(pathname: string, ret!: out FileError)
  post ?;		 Deletes the file with the specified name
schema !execute(command: string, args: seq of string, stdin, stdout, stderr: FileRef || void, res!: out FileError)
  post ?;		 Executes the specified command with the specified command line arguments and the specified standard input, output and error streams. [This method is not yet available in Java. In a future revision, the standard input, output and error parameters will be streams instead of file references.]
schema !fastForward(f: FileRef, ret!: out FileError)
pre gIsOpen(f)
post change openFiles[f.handle].fileptr, ret
  satisfy ret' = FileError success ==> openFiles[f.handle].fileptr' = #openFiles[f.handle].data;		 Moves the file pointer to the end of the file
schema !fileSize(f: FileRef, size!: out nat, ret!: out FileError)
pre gIsOpen(f)
post change size, ret, openFiles[f.handle].fileptr
  satisfy ret' = FileError success ==> size' = #openFiles[f.handle].data,
    openFiles[f.handle].fileptr' = openFiles[f.handle].fileptr;		 Gets the size of an open file. This is a modifying schema because it may change the file pointer if it fails.
function fileStatus(pathname: string): FileStats || FileError
  ^= ?;		 Returns status information about a file, including the times it was created, last modified and last accessed; its size; and its attributes, i.e. read-only, archive, system, directory (size will be 0 if this attribute is returned). Returns the FileStats object containing the information described, or a FileError describing the problem. If a path ending with the path separator character is passed, this is taken as an assertion that the path refers to a directory, and so if the path actually refers to a file instead of a directory, the error 'directoryNotFound' is returned.
function fileValid(pathname: string): bool
  ^= ?;		 Returns true if the file specified is accessible on the local file system (i.e. whether an open in read mode or a file status operation would succeed).
schema !flush(f: FileRef, ret!: out FileError)
  pre gIsOpen(f)
  post ?;		 Flushes any data held in buffers to the disk, console or printer concerned
schema !forceFileTime(filename: string, modified, accessed: Time || void, res!: out FileError)
  post ?;		 Forces the time attributes on a file. The schema will fail if the file does not exist or is currently open.
schema !garbageCollect
  post pass;		 Invokes the garbage collector of the run-time system provided by the implementation language, or attempts to reduce memory fragmentation in other ways. In a typical C++ implementation, memory held in free-lists in thePerfect run-time system is returned to the C++ memory manager.
function getCurrentDateTime: Time
  ^= ?;		 Returns the system date and time.
function getCurrentDirectory: string || void
  ^= ?;		 Returns the current default directory.
function getEnvironmentVar(envVar: string): string || void
  ^= ?;		 Returns the value of the specified environment variable, ornull if no variable of that name is defined.
function getImagePath: string
  ^= ?
  assert #result = 0 | result.last = pathSeparator;		 Returns the directory from which the program was loaded, if available.
function getImageVersion: seq of int
  ^= getImageVersion("")
  assert #result > 0;		 Returns version information for the main module of the current program. On Windows platforms, a sequence of four integers is returned in this order: Major version, Minor version, Revision, Build number. If no version information is available, a single zero is returned.
function getImageVersion(moduleName: string): seq of int
  ^= ?
  assert #result > 0;		 Returns version information for the specified module of the current program, or the main module if moduleName is the empty string. On Windows platforms, a sequence of four integers is returned in this order: Major version, Minor version, Revision, Build number. If no version information is available, a single zero is returned.
function getMemoryUsed: nat
  ^= ?;		 Returns the total number of bytes of memory allocated to the program (up to a maximum of 2GB on a 32-bit platform).
function getOsInfo: OsInfo
  ^= ?; 		Returns operating system information. Note that windows2000 will be detected as 'windowsNT' with the major version as 5.
function getRuntimeLanguage: string
  ^= ?; 		Returns the name of the programming language for which the runtime was built. Currently this is one of "c++", "c#" or "java".
ghost function gFileAtEof(f: FileRef): bool
  pre gIsOpen(f)
  ^= openFiles[f.handle].atEof;		 Expresses whether the file pointer is at the end of the file.
ghost selector gFileData(f: FileRef): seq of byte
  pre gIsOpen(f)
  ^= openFiles[f.handle].data;		 Expresses the contents of the file.
ghost function gFilePtr(f: FileRef): nat
  pre gIsOpen(f)
  ^= openFiles[f.handle].fileptr;		 Expresses the value of the file pointer.
ghost function gIsOpen(f: FileRef): bool
  ^= f.handle in openFiles.dom;		 Expresses whether the specified file is open.
ghost schema !gSetFilePtr(f: FileRef, pos: nat)
  pre gIsOpen(f),
    pos <= gFilePtr(f)
  post openFiles[f.handle].fileptr! = pos;		 Expresses the concept of setting the file pointer.
schema !makeDirectory(pathname: string, err!: out FileError)
  post ?;		 Creates the directory specified by 'pathname', including all components that do not already exist.
schema !move(oldPath, newPath: string, overwrite: bool, res!: out FileError)
 post ?;		 Moves the file specified by oldPath to newPath, overwriting any existing file if overwrite is true. Directories cannot be moved by this method. If the call fails, the error return res is set to one of the following values:
  • FileNotFound if 'oldPath' does not specify an existing file
  • AttribError if 'newPath' specifies an existing file and the overwrite argument was false
  • DeleteError if we failed to delete the existing target when trying to overwrite it
  • FileSpecError if oldPath and newPath specify the same file or if either are invalid
  • OtherError for any other problem (for example, if oldPath specifies a directory).

Only the 'last-accessed' attributes on the moved file is changed; all others are preserved.
function normalizeFile(path: string, fileName:string): FilePath || void
  pre #path = 0 | path.last = pathSeparator
  ^= ?;		 Splits fileName into path and filename components, assuming that the default directory is path.
schema !open(filename: string, mode: set of FileModeType, f!: out FileRef || FileError)
  pre #(set of FileModeType{FileModeType read, FileModeType create, FileModeType append} ** mode) ~= 0,
  ~(set of FileModeType{FileModeType create, FileModeType append} <<= mode)
  post change openFiles, f
    satisfy (f' within FileRef) ==>
      ( let fileHandle ^= (f' is FileRef).handle;
        openFiles'.dom= openFiles.dom.append(fileHandle)
        & openFiles'[fileHandle].fileptr = 0
        & (forall x::openFiles.dom :- openFiles'[x]= openFiles[x])
        & (FileModeType create in mode ==> #openFiles[fileHandle].data = 0)
        & ((FileModeType create in mode | FileModeType append in mode) <==> (f' is FileRef).fileWritable)
      ),
      (f' within FileError) ==> openFiles'= openFiles;		 Opens the specified file in the specified mode. The mode must include at least one of append, read or create; but may not include both append and create.
schema !open(hostname: string, port: nat, mode: SocketMode, s!: out Socket || SocketError)
  post ?;		 Opens a socket at the specified port at the specified named host.
schema !open(ipAddress: seq of byte, port: nat, mode: SocketMode, s!: out Socket || SocketError)
  pre #ipAddress = 4
  post ?;		 Opens a socket on the specified port at the specified IP address.
schema !print(c: char)
  post change stdOutStream.charData satisfy ?
  assert self'.stdOutStream.isOpen = stdOutStream.isOpen,
    stdOutStream.isOpen ==> self'.stdOutStream.charData = stdOutStream.charData.append(c);		 Writes the character to standard output.
schema !print(s: string)
  post change stdOutStream.charData satisfy ?
  assert self'.stdOutStream.isOpen = stdOutStream.isOpen,
    stdOutStream.isOpen ==> self'.stdOutStream.charData = stdOutStream.charData ++ s;		 Writes the string to standard output.
schema !print(f: FileRef, c: char, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post !write(f, seq of byte{byte{+c}}, ret!);		 Writes the character to the specified file.
schema !print(f: FileRef, s: string, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post !write(f, for x::s yield byte{+x}, ret!);		 Writes the string to the specified file.
schema !printStdErr(s: string)
  post change stdErrStream.charData satisfy ?
  assert self'.stdErrStream.isOpen = stdErrStream.isOpen,
    stdErrStream.isOpen ==> self'.stdErrStream.charData = stdErrStream.charData ++ s;		 Writes the string to the standard error stream.
schema !profile(f: FileRef, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post ?		 Stops collecting profile data and writes profiling information to the specified file. The data will be empty unless startProfiling has been called previously.
schema !read(f: FileRef, b!: out byte, ret!:out FileError)
  pre gIsOpen(f)
  post change openFiles[f.handle].fileptr, b, ret
   satisfy ret' = FileError success ==>
    openFiles[f.handle].fileptr < #openFiles[f.handle].data
    & b' = openFiles[f.handle].data[openFiles[f.handle].fileptr]
    & openFiles[f.handle].fileptr' = >openFiles[f.handle].fileptr;		 Reads a byte from the file.
schema !read(f: FileRef, s!: out seq of byte, len: nat, ret!: out FileError)
pre gIsOpen(f)
post change openFiles[f.handle].fileptr, s, ret
  satisfy ( let ptr ^= openFiles[f.handle].fileptr;
    let remainingData ^= openFiles[f.handle].data.drop(ptr);
        ( ret' = FileError success ==>
          len <= #remainingData
          & s' = remainingData.take(len)
          & openFiles[f.handle].fileptr' = ptr + len
        )
    & ( ret' = FileError success ==>
          len > #remainingData
          & s' = remainingData
          & openFiles[f.handle].fileptr' = #openFiles[f.handle].data
        )
    );		 Reads up to len bytes from the file.
schema !read(f: FileRef, n!: out int, numBytes:nat, ret!: out FileError)
  pre gIsOpen(f), numBytes > 0
  post ?;		 Reads numBytes bytes from the file and interprets them as an integer in big-endian format.
schema !read(f: FileRef, r!: out real, ret!:out FileError)
  pre gIsOpen(f)
  post ?;		 Reads a number of bytes (typically 8) from file and interprets them as a floating-point number (typically assuming IEEE double precision format).
schema !readLine(line!:out string, ret!: out FileError)
  post change stdInStream.charData, line, ret satisfy ?
  assert `\n` ~in line',
    line' ++ "\n" ++ self'.stdInStream.charData = stdInStream.charData
    | (line' = stdInStream.charData & self'.stdInStream.charData.empty)
    | (line' = "" & ret' ~= FileError success);		 Reads a line of text from standard input. The final line-feed or carriage-return and line-feed are discarded and not returned.
schema !readLine(f: FileRef, line!: out string, ret!: out FileError)
  pre gIsOpen(f)
  post ?;		 Reads a line of text (i.e. a data block ending in either linefeed or end-of-file) from the specified file. The final line-feed or carriage-return and line-feed are discarded and not returned.
schema !rewind(f: FileRef, ret!: out FileError)
  pre gIsOpen(f)
  post !seek(f, 0, ret!);		 Moves the file-pointer to the start of the file.
schema !scan(f: FileRef, s!: out string, len:nat, ret!: out FileError)
  pre gIsOpen(f)
  post ?;		 Attempts to read up to len characters from the file.
schema !scan(f: FileRef, c!: out char, ret!:out FileError)
  pre gIsOpen(f)
  post ?;		 Attempts to read a single character from the file.
schema !seek(f: FileRef, pos: nat, ret!: out FileError)
  pre gIsOpen(f)
  post change openFiles[f.handle].fileptr, ret
    satisfy ret' = FileError success ==> openFiles[f.handle].fileptr' = pos;		 Sets the file pointer to the given file position as a byte offset from the start of the file.
schema !setCurrentDirectory(path: string, ret!: out FileError)
  post ?;		 Sets the current directory.
schema !setCurrentThreadPriority(priority: int)
  pre priority in 1..20
  post ?;		 Sets the priority of the current thread, where 1 is the lowest priority and 20 is the highest.
schema !setMaxCheckNestLevel(level: nat)
  post ?;		 Sets the nesting level to which debug checks are performed (i.e. when debug checks occur while evaluating debug checks).
schema !setMode(fname: string, atts: set of FileAttribute, res!:out FileError)
  pre atts <<= set of FileAttribute{FileAttribute read, FileAttribute write, FileAttribute execute}
  post ?;		 Sets the attributes of the file with the specified name.
schema !setRuntimeOption(debOpt: DebugType)
  post !setRuntimeOptionState(debOpt, true);		 Enables debug checks of the specified type.
schema !setRuntimeOptions(debOpts: set of DebugType)
  post !setRuntimeOptionsState(debOpts, true);		 Enables debug checks of the specified types.
schema !setRuntimeOptionState(debOpt: DebugType, state: bool)
 post !setRuntimeOptionsState(set of DebugType{debOpt}, state);		 Enables (if state is true) or disables (if state is false) debug checks of the specified type.
schema !setRuntimeOptionsState(debOpt: set of DebugType, state: bool)
  post ?;		 Enables (if state is true) or disables (if state is false) debug checks of the specified types.
schema !startProfiling
  post ?		 Starts collecting profiling data, if the program has been built with profiling enabled; otherwise ignored.
function stdErr: StandardOutputStream
  ^= stdErrStream;		 Returns a stream corresponding to standard error output.
function stdIn: StandardInputStream
  ^= stdInStream;		 Returns a stream corresponding to standard input.
function stdOut: StandardOutputStream
  ^= stdOutStream;		 Returns a stream corresponding to standard output.
function tell(f: FileRef): nat || FileError
  pre gIsOpen(f)
  satisfy (result within nat) ==> result = openFiles[f.handle].fileptr;		 Returns the current file position as a byte offset from the start of the file.
schema !write(f: FileRef, b: byte, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post !write(f, seq of byte{b}, ret!);		 Writes a single byte to the file.
schema !write(f: FileRef, s: seq of byte, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post change openFiles[f.handle].data, openFiles[f.handle].fileptr, ret
    satisfy ret' = FileError success ==>
        ( let ptr ^= openFiles[f.handle].fileptr;
          let oldData ^= openFiles[f.handle].data;
          openFiles[f.handle].data' = oldData.take(ptr) ++ s ++ ([ptr + #s < #oldData]: oldData.drop(ptr + #s), []: seq of byte{})
        & openFiles[f.handle].fileptr' = ptr + #s
        ),
        ret' ~= FileError success ==> openFiles[f.handle].data'.begins(openFiles[f.handle].data);		 Writes a sequence of bytes to the file.
schema !write(f: FileRef, i, numBytes: int, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable, numBytes > 0
  post ?;		 Writes an integer of the specified size (number of bytes) to the file.
schema !write(f: FileRef, r: real, ret!: out FileError)
  pre gIsOpen(f), f.fileWritable
  post ?;		 Write a real number in binary format to a file (typically 8 bytes in IEEE double-precision format).

 

FileAttribute
class FileAttribute ^= enum read, write, execute, archive, system, hidden, directory end; Enumeration class to describe the various attributes of a file.

 

FileError
class FileError ^=
enum
  success,
  endOfFile,
  fileNotFound,
  directoryNotFound,
  fileNotOpen,
  diskFull,
  readError,
  writeError,
  flushError,
  seekError,
  deleteError,
  attribError,
  fileSpecError,
  permError,
  createError,
  closeError,
  otherError
end		 Error codes returned by the various file system methods.

The value 'success' indicates no error.

The directoryNotFound value is generated by the filestatus schema of class Environment if a path that ends with a path separator is passed and the path refers to a file instead of a directory; and by setCurrentDirectory if the path specified does not exist.

 

FileHandle
class FileHandle ^= tag Class used internally to refer to open files in an Environment

 

FileInputStream
final class FileInputStream ^= inherits InputStream  

Constructors
build {!fref: FileRef, !env: Environment}
  inherits InputStream{};		  

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream and its associated file.
define ghost function gStreamAtEnd: bool
  ^= ?;		  
define ghost function gStreamData: seq of byte
  ^= env.gFileData(fref);		  
define ghost function gStreamPtr: nat
  ^= env.gFilePtr(fref);		  
define schema !read(b!: out byte, ret!: out FileError)
  post ?;		  
schema !read(s!: out seq of byte, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream.
schema !read(n!: out int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream.
schema !read(c!: out char, decoder!: limited from CharDecoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream.
schema !read(r!: out real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream.

 

FileMode
class FileMode This is a namespace class that provides some constant definitions

Data
const read ^= set of FileModeType{FileModeType read};
const create ^= set of FileModeType{FileModeType create};
const append ^= set of FileModeType{FileModeType append};
const readText ^= set of FileModeType{FileModeType read, FileModeType text};
const createText ^= set of FileModeType{FileModeType create, FileModeType text};
const appendText ^= set of FileModeType{FileModeType append, FileModeType text};
function read, create, append, readText, createText, appendText;		 These constants represents commonly-used modes.

 

FileModeType
class FileModeType ^= enum read, create, append, text end Enumeration describing the modes in which a file may be opened.

 

FileOutputStream
final class FileOutputStream ^= inherits OutputStream  

Constructors
build {!fref: FileRef, !env: Environment}
  inherits OutputStream{};		  

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream and its associated file, flushing any buffered data to the file.
define schema !flush
  post ?;		 Flushes any buffered data to the file.
define ghost function gStreamData: seq of byte
  ^= ?;		  
define schema !write(b: byte, ret!: out FileError)
  post ?;		 Writes a byte to the file.
schema !write(s: seq of byte, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.
schema !write(i: int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class OutputStream.
schema !write(c: char, encoder: from CharEncoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.
schema !write(r: real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.

 

FilePath
final class FilePath Type returned by Environment function normalizeFile to hold the split components, path and file.

Data
var pathName, fileName: string;
function pathName, fileName;		  

Invariants
#pathName > 0,
pathName.last = Environment pathSeparator,
Environment pathSeparator ~in fileName;		  

Constructors
build {!pathName, !fileName: string}
  pre #pathName > 0,
    pathName.last = Environment pathSeparator,
    Environment pathSeparator ~in fileName;		  

Methods
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

FileRef
final class FileRef Encapsulates a FileHandle object. Returned by members of class Environment that create or open files.

Methods
function fileWritable: bool
  ^= ?;		  
ghost function handle: FileHandle
  ^= ?;		  

 

FileStats
final class FileStats Hold status information for a file as returned from the environment function fileStatus.

Data
var created, lastModified, lastAccessed: Time,
  attribs: set of FileAttribute,
  size: nat ;
function created, lastModified, lastAccessed, attribs, size;		  

Constructors
build {!created, !lastModified, !lastAccessed: Time, !attribs:set of FileAttribute, !size: nat};  

Methods
redefine function toString: string
  ^= ?;		  

 

GuardedObject of X
final class GuardedObject of X  

Data
var guard: bool,
  when [guard]:
    object: X
  end;
function guard, object;		  

Constructors
build{}
  post guard! = false;		  
build {!object: X}
  post guard! = true;		  

 

InputStream
deferred class InputStream  

Constructors
build{}
  inherits Stream{};		  

Methods
operator =(other);  
deferred schema !close(ret!: out FileError)
  pre isOpen
  assert ~self'.isOpen;		 Closes the stream, making it unavailable for subsequent input and releasing any associated resources.
deferred ghost function gStreamAtEnd: bool;  
deferred ghost function gStreamPtr: nat
  assert result <= #gStreamData;		  
deferred schema !read(b!: out byte, ret!: out FileError)
  pre isOpen
  assert self'.isOpen,
    self'.gStreamData = gStreamData,
    self'.gStreamPtr = ([ret'= FileError success]: gStreamPtr + 1, []: gStreamPtr),
    ret' = FileError success ==> gStreamPtr < #gStreamData & b' = gStreamData[gStreamPtr];		 Basic schema for reading a byte from a stream.
schema !read(s!: out seq of byte, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?   assert self'.isOpen,
    self'.gStreamData = gStreamData,
    ( [ret' = FileError success]:
        1 <= #s' <= numBytes
        & self'.gStreamPtr = gStreamPtr + #s'
        & s' = gStreamData.drop(gStreamPtr).take(#s'),
      []:
        s' = seq of byte{}
    );		  
schema !read(n!: out int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?
  assert self'.isOpen, self'.gStreamData = gStreamData;		  
schema !read(c!: out char, decoder!: limited from CharDecoder, ret!: out FileError)
  pre isOpen
  post ?
  assert self'.isOpen, self'.gStreamData = gStreamData;		  
schema !read(r!: out real, ret!: out FileError)
  pre isOpen
  post ?
  assert self'.isOpen, self'.gStreamData = gStreamData;		  

 

int
final class int ^= storable A class representing zero and the positive and negative integers

Constructors
build {s: string}
  pre #s > 0,
    forall x::s :- x.isDigit
  ^= ( [#s > 1]:
        10 * s.head.digit + nat {s.tail},
      []:
        s.head.digit
    )
  assert result >= 0;		 Builds a non-negative integer from its string representation in decimal.

Methods
total operator ~~(a)
  ^= ?;		 The usual ordering between integers (the successor of n ranks above n)
operator +(a: int): int
  ^= ?;		 Addition.
operator +(a: real ): real
  ^= real{self} + a;		 Addition.
operator -: int
  ^= ?;		 Negation.
operator -(a: int):int
  ^= ?;		 Subtraction.
operator -(a: real):real
  ^= real{self} - a;		 Subtraction.
operator *(a: int): int
  ^= ?;		 Multiplication.
operator *(a: real ): real
  ^= real{self} * a;		 Multiplication.
operator /(a: int): int
  pre a > 0
  ^= ?;		 Division, rounding towards minus infinity.
operator /(a: real): real
  pre a ~= 0.0
  ^= real{self} / a;		 Division.
operator %(a: int): int
  pre a > 0
  ^= ?
  assert result in 0..<a;		 Modulo (remainder).
operator ^(a: nat): int
  ^= ?;		 Exponentiation.
operator ^(a: real ): real
  pre a > 0.0
  ^= real{self} ^ a;		 Exponentiation.
operator >: int
  ^= self + 1;		 Successor.
operator <:int
  ^= self - 1;		 Predecessor.
operator .. (b: int): seq of int
  decrease b
  ^= ([b < self]: seq of int{}, [b >= self]: (self .. <b).append(b))
  assert result.isndec;		 Returns the sequence of all integers in the given range (inclusive) in ascending order.
function abs: nat
  ^= ([self >= 0]: self, [self <= 0]: -self);		 Returns the absolute value.
function intln: nat
  pre self >= 0
  ^= ([self = 0]: 0, [self > 0]: that i::0..self :- 2 ^ i <= self & 2 ^ (i + 1) > self);		 Returns the logarithm to base 2, rounded down.
redefine function toString: string
  ^= ?
  assert result ~= "";		 Returns the integer as a string in minimum-width format, i.e. "0" or "###" or "-###" where ### is a nonempty digit string with no leading zeros.

 

map of (X -> Y)
final class map of (X->Y)
  require X has operator =(arg) end		 This class represents a mapping from elements of type X to elements of type Y.

Constructors
build{}
  post ?
  assert self'.pairs.empty;		  
build{repeated a:X -> b:Y}
  pre forall i::0..(#a-2) :- forall j::>i..<#a :- a[i] = a[j] ==> b[i] = b[j]
  post ?
  assert self'.pairs = (for i::0..<#a yield pair of (X , Y){a[i] , b[i]}).ran,
    forall i::0..<#a :- self'[a[i]] = b[i];		  
build{p: set of pair of (X,Y)}
  require Y has operator =(arg) end
  pre forall x, y::p :- x = y | x.x ~= y.x
  post ?
  assert self '.pairs = p;		  
build {a: seq of pair of (X,Y)}
  require Y has operator =(arg) end
  pre forall x, y::a :- x = y | x.x ~= y.x
  post ?
  assert self '.pairs = a.ran;		  

Methods
operator #: nat
  ^= #pairs;		  
operator ++(a: map of (X->Y)): map of (X->Y)
  require Y has operator =(arg) end
  pre forall x::dom**a.dom :- self[x] = a[x]
  ^= map of (X->Y){pairs ++ a.pairs}
  assert result.dom = dom ++ a.dom,
    forall x::dom :- result [x] = self[x],
    forall x::a.dom :- result[x] = a[x];		  
operator --(a: set of X): map of (X->Y)
  ^= map of (X->Y){those x::pairs :- x.x ~in a};		  
operator **(a: set of X): map of (X->Y)
  ^= map of (X->Y){those x::pairs :- x.x in a};		  
operator ##(a: map of (X->Y)): bool
  ^= dom ## a.dom;		  
operator ##(a: set of X): bool
  ^= dom ## a;		  
selector [](a: X): Y
  pre a in dom
  ^= ?
  assert result = (that x::pairs :- x.x = a).y;		  
operator (a: X) in: bool
  ^= exists x::pairs :- x.x = a;		  
function append(a: pair of (X,Y)): map of (X->Y)
  require Y has operator =(arg) end
  pre a.x in self ==> a.y = self[a.x]
  ^= map of (X->Y){pairs.append(a)};		  
function append(a: X -> b: Y): map of (X->Y)
  require Y has operator =(arg) end
  pre a in self ==> b = self[a]
  ^= map of (X->Y){pairs.append(pair of (X,Y){a , b})};		  
function dom: set of X
  ^= for p::pairs yield p.x;		  
function empty: bool
  ^= #self = 0;		  
function pairs: set of pair of (X,Y)
  ^= ?
  assert forall a, b::result :- a.x = b.x ==> a = b;		 This returns the contents of the mapping viewed as a set of (domain element, range element) pairs.
function ran: set of Y
  require Y has operator =(arg) end
  ^= for x::pairs yield x.y;		  
function ranb: bag of Y
  ^= for p::pairs.rep(1) yield p.y;		  
function remove(a: X): map of (X->Y)
  ^= map of (X->Y){those x::pairs :- x.x ~= a};		  
function testIndex(a: X): GuardedObject of Y
  ^= ( [a in self ]:
        GuardedObject of Y{self [a]},
      []:
        GuardedObject of Y{}
    );		  
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

nat
class nat ^= int >= 0; The naturals comprise the non-negative integers.

 

OsInfo
class OsInfo ^= storable This is the type returned by Environment function getOsInfo to hold the operating system type and version information.

Data
var type: OsType,
  osMajorVersion: nat,
  osMinorVersion: nat,
  spMajorVersion: nat,
  spMinorVersion: nat;
function type, osMajorVersion, osMinorVersion, spMajorVersion, spMinorVersion;		 The operating system type, its major and minor version numbers and its service pack major and minor version numbers.

Constructors
build {!type: OsType, !osMajorVersion, !osMinorVersion, !spMajorVersion, !spMinorVersion: nat}; Constructor to set operating system type, operating system major & minor versions and service pack major & minor versions (for Microsoft operating systems).

build{!type: OsType, !osMajorVersion, !osMinorVersion: nat}
  post spMajorVersion! = 0, spMinorVersion! = 0;		 Constructor to set operating system type and operating system major & minor versions only.

Methods
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

OsType
class OsType ^= enum unknown, windows95, windows98, windowsNT, linux end Note that Windows 2000 reports itself as Windows NT version 5.

 

OutputStream
deferred class OutputStream  

Constructors
build{}
  inherits Stream{};		  

Methods
operator =(other);  
deferred schema !close(ret!: out FileError)
  pre isOpen
  assert ~self'.isOpen;		 Closes the stream, making it unavailable for subsequent output and releasing any associated resources.
deferred schema !flush(ret!: out FileError)
  pre isOpen
  assert self'.isOpen, self'.gStreamData = gStreamData;		 Flushes any buffered data to the device concerned.
deferred schema !write(b: byte, ret!: out FileError)
  pre isOpen
  assert self'.isOpen,
    ret' = FileError success ==> self'.gStreamData = gStreamData.append(b);		  
schema !write(s: seq of byte, ret!: out FileError)
  pre isOpen
  post ?
  assert self'.isOpen,
    ret' = FileError success ==> self'.gStreamData = gStreamData ++ s;		  
schema !write(i: int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?
  assert self'.isOpen;		  
schema !write(c: char, encoder: from CharEncoder, ret!: out FileError)
  pre isOpen
  post ?
  assert self'.isOpen;		  
schema !write(r: real, ret!: out FileError)
  pre isOpen
  post ?
  assert self'.isOpen;		  

 

pair of (X, Y)
final class pair of (X, Y) ^= storable  

Data
var x: X, y: Y;
selector x, y;		  

Constructors
build {!x: X , !y: Y};  

Methods
operator ~~(a)
  ^= ( let t1 ^= x ~~ a.x;
        [t1 = rank same ]:
          y ~~ a.y,
        []:
          t1
      );
 		  
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

rank
class rank ^= enum below, same, above end The class used to express the result of a comparison between two values.

 

real
final class real ^= storable A class representing real numbers stored to some limited precision (typically IEEE double-precision format).

Constructors
build{a: int}
  ^= ?;		 Constructs a real from the given integer.

Methods
total operator ~~(a)
  ^= ?; 		Higher numbers rank above lower numbers.
operator +(a: real): real
  ^= ?;		 Addition.
operator +(a: int): real
  ^= self + real {a};		 Addition.
operator -: real
  ^= ?;		 Negation.
operator -(a: real): real
  ^= ?;		 Subtraction.
operator -(a: int): real
  ^= self - real {a};		 Subtraction.
operator *(a: real): real
  ^= ?;		 Multiplication.
operator *(a: int ): real
^= self * real{a};		 Multiplication.
operator /(a: real): real
  pre a ~= 0.0
  ^= ?;		 Division.
operator /(a: int): real
  pre a ~= 0
  ^= self / real{a};		 Division.
operator ^(a: real): real
  pre a > 0.0
  ^= ?;		 Exponentiation.
operator ^(a: int): real
  pre self ~= 0.0 | a ~= 0
  ^= self ^ real{a};		 Exponentiation.
function abs: real
  ^= ([self >= 0.0]: self, [self <= 0.0]: -self)
  assert result >= 0.0;		 Absolute value.
function isInfinite: bool
  ^= ?;		 Returns true if the given value represents of positive or negative infinity.
function isNaN: bool
  ^= ?;		 Returns true if the given value represents a not-a-number.
function rounddn: int
  satisfy real{result} <= self & real{>result} > self;		 Return integral part, rounding towards minus infinity.
function roundin: int
  ^= ([self >= 0.0]: rounddn, [self <= 0.0]: roundup);		 Return integral part, rounding towards zero.
function roundout: int
  ^= ([self >= 0.0]: roundup, [self <= 0.0]: rounddn);		 Return integral part, rounding away from zero.
function roundup: int
  satisfy real{result} >= self & real{<result} < self;		 Return integral part, rounding towards plus infinity.
redefine function toString: string
  ^= ?
  assert result ~= "";		 Returns a string representation of the real number.

 

ReverseComparator of X
final class ReverseComparator of X ^= inherits Comparator of X This comparator compares objects according to the reverse of their normal rank ordering.

Constructors
build{}
  inherits Comparator of X{};		  

Methods
define function compare(a, b: X): rank
  ^= b ~~ a;		  
final function notLessThan(a, b: X): bool
  ^= compare(a, b) ~= rank below;		 Inherited from class Comparator of X.

 

seq of X
final class seq of X An ordered list of elements.

Constructors
build {}
  post ?
  assert #self';=0;		 Builds an empty sequence.
build{repeated x: X}
  post ?;		 Builds a sequence containing the elements in the parameter list.

Methods
total operator ~~(b)
 ^= ( let len ^= #self;
    let lenb ^= #b;
    [len = 0 = lenb]:
      rank same,
    [len = 0 ~= lenb]:
      rank below,
    [len ~= 0 = lenb]:
      rank above,
    [len ~= 0 ~= lenb]:
      ( let temp ^= self.head ~~ b.head;
        [temp = rank same]:
          self.tail ~~ b.tail,
        []:
          temp
      )
    );		 Ordering operator. Compares the lengths first; only compares the elements if the lengths are the same.
operator #: nat
  ^= ?;		 Returns the number of elements in self.
operator (elem: X) #: nat
  require X has operator =(arg) end
  ^= #(those i::dom :- elem = self[i]);		 Returns the number of times elem occurs in self.
operator ++(other: seq of X): seq of X
  satisfy #result = #self + #other,
    forall x::dom :-result[x] = self[x],
    forall x::other.dom :- result[x + #self] = other[x];		 Returns a new sequence comprising self followed by other.
operator (elem: X) in: bool
  require X has operator =(arg) end
  ^= exists i::dom :- self [i] = elem;		 Returns true if and only if self has the element elem.
operator (other: seq of X)<<=: bool
  require X has operator =(arg) end
  ^= exists i::0..(#self -#other) :- slice(i, #other) = other;		 Returnstrue if and only if other is a subsequence of self. See also the begins and ends methods.
operator (other: seq of X)<<: bool
  require X has operator =(arg) end
  ^= a <<= self & self ~= other;		 Returns true if and only if other is a strict subsequence of self.
selector [](index: nat): X
  pre index < #self
  ^= ?;		 Accesses the element at position index. The first element has index zero.
function append(elem: X): seq of X
  satisfy #result = >#self,
    result.front = self,
    result.last = elem;		 Returns a new sequence comprising self with elem appended.
function begins(other: seq of X): bool
  require X has operator =(arg) end
  ^= #other <= #self & self.take(#other) = other;		 Returns true if and only if other is a leading subsequence of self.
function dom: set of nat
  ^= (for i::0.. <#self yield i is nat).ran;		 Returns the set of all the valid indices of self.
function drop(howMany: nat): seq of X
  pre howMany <= #self
  satisfy #result = #self - howMany,
    forall i::result.dom :- result[i] =self[i + howMany];		 Returns a copy of self with howMany leading elements removed.
function empty: bool
  ^= #self = 0;		 Returnstrue if and only if self contains no elements.
function ends(other: seq of X): bool
  require X has operator =(arg) end
  ^= #other <= #self & self.drop(#self - #other) = other;		 Returns true if and only if other is a trailing subsequence of self.
function findFirst(token: X): int
  ^= ( [token in self]:
        (those i::self.dom :- self[i] = token).min,
      []:
        -1
    );		 Returns the index of the first occurrence of token inself, or -1 if it does not occur.
function findFirst(arg: seq of X): int
  ^= ( [arg <<= self]:
        (those i::0..#self :- self.drop(i).begins(arg)).min,
      []:
        -1
    );		 Returns the index of the first occurrence of arg inself, or -1 if it does not occur.
function findLast(token: X): int
  ^= ( [token in self]:
        (those i::self.dom :- self[i] = token).max,
      []:
        -1
    );		 Returns the index of the last occurrence of token in self, or -1 if it does not occur.
function findLast(arg: seq of X): int
  ^= ( [arg <<= self]:
        (those i::0..#self :- self.drop(i).begins(arg)).max,
      []:
        -1
    );		 Returns the index of the last occurrence of arg in self, or -1 if it does not occur.
function front: seq of X
  pre #self ~= 0
  satisfy #result = <#self,
    forall x::result .dom :- result[x] =self[x];		 Returns a copy of self with the last element removed.
selector head: X
  pre ~empty
  ^= self[0];		 Returns the first element of self.
function insert(index: nat, a: X): seq of X
  pre index <= #self
  ^= take(index).append(a)++drop(index);		 Returns a new sequence comprising the original with the given element inserted before the element at index.
function insert(index: nat, a: seq of X):seq of X
  pre index <= #self
  ^= take(index)++ a ++drop(index);		 Returns a new sequence comprising the original with the given sequence inserted before the element at index.
function insertndec(x: X): seq of X
  pre isndec
  ^= orderedInsert(x, SimpleComparator of X{})
  assert result.isndec;		 Returns a new sequence comprising the original nondecreasing sequence with the given element inserted at the latest possible position that preserves the ordering.
function insertninc(x: X): seq of X
  pre isninc
  ^= orderedInsert(x, ReverseComparator of X{})
  assert result.isninc;		 Returns a new sequence comprising the original nonincreasing sequence with the given element inserted at the latest possible position that preserves the ordering.
function isndec: bool
  ^= #self <= 1 | (forall i::1..<#self :- (self[i] ~~ self[<i]) ~= rank below);		 Returns true if self is nondecreasing according to the standard ordering relation on its elements.
function isninc: bool
  ^= #self <= 1 | (forall i::1..<#self :- (self[i] ~~ self[<i]) ~= rank above);		 Returns true if self is nonincreasing according to the standard ordering relation on its elements.
function isOrdered(cp: from Comparator of X): bool
   ^= forall i::1..<#self :- cp.notLessThan(self[i],self[<i]);		 Returns true if self is nondecreasing according to the ordering defined by cp .
selector last: X
  pre ~empty
  ^= self[<#self ];		 Returns the last element of self.
function max: X
  pre ~empty
  ^= self[that x::0..<#self :- (forall y::0..<#self :- self [y] ~~ self[x] ~= rank above) & (forall y::0..<x :- self[y] ~~ self[x] ~= rank same)];		 Returns the highest value from self. If the element type does not have a total ordering and there are several different elements in self that rank same with each other but above all other elements, returns the earliest one.
function mergendec(other: seq of X): seq of X
  pre isndec, other.isndec
  ^= orderedMerge(other, SimpleComparator of X{})
  assert result.isndec;		 Merges other into self. Elements of other appear in the result after elements of self with which they rank same.
function mergeninc(other: seq of X): seq of X
  pre isninc, other.isninc
  ^= orderedMerge(other, ReverseComparator of X{})
  assert result.isninc;		 Merges other into self. Elements of other appear in the result after elements of self with which they rank same.
function min: X
  pre ~empty
  ^= self[that x::0..<#self :- (forall y::0..<#self :- self [y] ~~ self[x] ~= rank below) & (forall y::0..<x :- self[y] ~~ self [x] ~= rank same)];		 Returns the lowest value from self. If the element type does not have a total ordering and there are several different elements in self that rank same with each other but below all other elements, returns the earliest one.
opaque function opermndec: seq of X
  satisfy result .ranb = ranb,
    result.isndec;		 Returns a copy of the sequence sorted into a nondecreasing order. If the element type has a total ordering, you should use permndec instead.
opaque function opermninc: seq of X
  satisfy result .ranb = ranb,
    result.isninc;		 Returns a copy of the sequence sorted into a nonincreasing order. If the element type has a total ordering, you should use permninc instead.
function orderedInsert(elem: X, cp: from Comparator of X): seq of X
  pre isOrdered(cp)
  satisfy result.isOrdered(cp) & result .ranb =self.ranb.append(x);		 Returns a new sequence comprising the original ordered sequence with elem inserted at the latest possible position that preserves the ordering.
function orderedMerge(other: seq of X, cp: from Comparator of X): seq of X
  pre isOrdered(cp), other.isOrdered(cp)
  satisfy result .isOrdered(cp) &result.ranb = self.ranb ++ other.ranb;		 Merges other into self. Elements of other appear in the result after elements of self with which they rank same.
opaque schema !osort(cp: from Comparator of X)
  post change self satisfy self'.isOrdered(cp),
    self'.ranb = ranb;		 Sorts the sequence into a nondecreasing order according to the ordering defined by cp. If cp provides a total ordering on the element type, you should use sort instead.
function permndec: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb = ranb,
    result.isndec;		 Returns a copy of self sorted into nondecreasing order.
function permninc: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb = ranb,
    result.isninc;		 Returns a copy of self sorted into nonincreasing order.
function prepend(a: X): seq of X
  satisfy #result = >#self,
    result.head = a,
    result.tail = self;		 Returns a new sequence comprising the original with the parameter prepended.
function ran: set of X
  require X has operator =(arg) end
  satisfy forall x:X :- (x in result) = (x in self);		 Creates a set from the elements by removing duplicates and ordering.
function ranb: bag of X
  require X has operator =(arg) end
  satisfy #result = #self,
    forall x::result :- x # result = x #self;		 Creates a bag from the elements by removing the ordering.
function remove(index: nat): seq of X
  pre index < #self
  ^= take(index) ++ drop(>index);		 Creates a copy of self with the element at the given position removed.
function remove(index: nat, length: nat):seq of X
  pre length+index <= #self
  satisfy result = take(index) ++ drop(index + length);		 Creates a copy of self with length elements starting at position index removed.
function rep(n: nat): seq of X
  satisfy #result = #self * n,
    forall j::0.. <n, i::dom :- result[i + (j * #self)] = self[i];		 Produces a new sequence by concatenating self n times.
function rev: seq of X
  satisfy #result = #self,
    forall x::dom :- result[#self-x-1] =self[x];		 Produces the sequence with the elements in reverse order.
function slice(index, length: nat): seq of X
  pre index+length <= #self
  ^= drop(index).take(length);		 Returns length elements starting at offset index.
schema !sort(cp: from Comparator of X)
  pre forall x,y: X :- cp.compare(x, y) = rank same ==> x = y
  post change self satisfy self'.isOrdered(cp),
    self'.ranb = ranb;		 Sorts the elements into nondecreasing order according to the ordering defined by cp.
function split(token: X): seq of seq of X
  require X has operator =(arg) end
  ^= ( let bounded ^= append(token).prepend(token);
      let token_indices ^= those i::0..<#bounded :- bounded[i] = token;
      for i::0..(#token_indices-2) yield bounded.take(token_indices[i+1]).drop(token_indices[i]+1)
    )
  assert #result > 0;		 Splits the sequence into a sequence of sequences, using the specified token element to determine the split points.
function tail: seq of X
  pre #self ~= 0
  satisfy #result = <#self,
    forall x::result .dom :- result[x] =self[>x];		 Returns a new sequence comprising self with the first element removed.
function take(n: nat): seq of X
  pre n <= #self
  satisfy #result = n,
    forall i::0..<n :- result[i] = self[i];		 Returns a new sequence comprising the first n elements of self.
redefine function toString: string
  ^= ?
  assert result ~= "";		 Returns a textual representation of self.
function unique: bool
  require X has operator =(arg) end
  ^= forall x::dom :- ~(exists y::>x..<#self :- self[y] = self [x])
  assert result <==> #self = #(self.ran);		 Returns true if no value occurs more than once in self.

 

SerialError
final class SerialError  

Data
var id: SerialErrorType,
  msg: string;
function id, msg;		  

Constructors
build {!id: SerialErrorType, !msg: string};  

 

SerialErrorType
class SerialErrorType ^=
enum
  // General system errors ...
  writeError, internalError, readError,
  // Storage-stream system errors ...
  systemVersionError, userVersionError, streamError, missingInstantiation,
  missingHeap, missingType, unexpectedType, corruptStream,
  // Catchall system error
  unspecifiedError
end;		  

 

set of X
final class set of X
  require X has operator =(arg) end		 An unordered collection of elements in which duplicates are not permitted

Constructors
build {}
  post ?
  assert self'.empty;		 Builds an empty set
build{repeated x: X}
 post ?;		 Builds a set containing the parameters (any duplicates are removed)

Methods
operator #: nat
  ^= ?;		 Cardinality of self.
operator ##(a: set of X): bool
  ^= forall x::self :- x ~in a;		 Disjointness operator.
operator ++(a: set of X): set of X
  satisfy forall x:X :- x in result <==> x in self | x in a;		 Union.
operator --(a: set of X): set of X
  satisfy forall x:X :- x in result <==> x in self & x ~in a;		 Difference.
operator **(a: set of X): set of X
  ^= those x::self :- x in a;		 Intersection.
operator <<=(a: set of X): bool
  ^= forall x::self :- x in a;		 Subset.
operator <<(a: set of X): bool
  ^= self <<= a & #self < #a;		 Strict subset.
operator (a: X) in: bool
   ^= ?;		 Membership.
function append(a: X): set of X
  satisfy self <<= result,
    a in result,
    forall x::result :- x = a | x in self;		 Adds an element to self, returning a new set.
function empty: bool
  ^= #self = 0;		  
function max: X
  require X has total operator ~~(arg) end
  pre ~empty
  ^= that x::self :- forall y::self :- (x ~~ y) ~= rank below;		 Return the maximum element from self.
function min: X
  require X has total operator ~~(arg) end
  pre ~empty
  ^= that x::self :- forall y::self :- (x ~~ y) ~= rank above;		 Return the minimum element from self.
opaque function omax: X
  pre ~empty
  ^= any x::self :- forall y::self :- (x ~~ y) ~= rank below;		 Return a maximum element from self. If the element type has a total ordering, you should use max instead.
opaque function omin: X
  pre ~empty
  ^= any x::self :- forall y::self :- (x ~~ y) ~= rank above;		 Return a minimum element from self. If the element type has a total ordering, you should use min instead.
opaque function opermndec: seq of X
  satisfy result .ranb = self.rep(1),
    result.isndec;		 Returns a sequence comprising the elements of self in nondecreasing order. If the element type has a total ordering, you should use permndec instead.
opaque function opermninc: seq of X
  satisfy result .ranb = self.rep(1),
    result.isninc;		 Returns a sequence comprising the elements of self in nonincreasing order. If the element type has a total ordering, you should use permninc instead.
function permndec: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb =self.rep(1),
    result.isndec;		 Returns the sequence comprising the elements of self in nondecreasing order
function permninc: seq of X
  require X has total operator ~~(arg) end
  satisfy result.ranb =self.rep(1),
    result.isninc;		 Returns the sequence comprising the elements of self in nonincreasing order
function remove(a: X): set of X
  satisfy result <<= self,
    a ~in result,
    self = result | self = result.append(a);		 Removes an element to self, returning a new set
function rep(a: nat): bag of X
  satisfy result .ran = self,
    forall x::self :- x # result = a;		 Returns a bag comprising each element of self repeated a times
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

SimpleComparator of X
final class SimpleComparator of X ^= inherits Comparator of X This comparator compares objects using their normal rank ordering.

Constructors
build{}
  inherits Comparator of X{};		  

Methods
define function compare(a, b: X): rank
  ^= a ~~ b;		  
final function notLessThan(a, b: X): bool
  ^= compare(a, b) ~= rank below;		 Inherited from class Comparator of X

 

Socket
final class Socket Represents a socket for communicating over a network. [A future version of the library is likely to support sockets as streams instead.]

Methods
schema !awaitConnection(res!: out bool)
  post ?;		 Wait for a connection, blocking until one arrives (for server mode sockets only).
schema !closeSocket(res!: out bool)
  post ?;		  
function getLastError: SocketError
  ^= ?;		 Returns the last network error recorded.
function getRemoteAddress: seq of nat
  pre gIsServerSocket
  ^= ?
  assert #result = 4;		  
function getRemotePort: nat
  pre gIsServerSocket
  ^= ?;		  
ghost function gIsServerSocket: bool
  ^= ?;		  
schema !read(res!: out byte || SocketError)
  post ?;		 Reads a single byte from the socket.
schema !read(numBytes: nat, res!: out (seq of byte) || SocketError)
  pre numBytes > 0
  post ?;		 Reads the specified number of 8-bit bytes from the socket specified. Blocks until all bytes read or an error is encountered. Returns the sequence of bytes read, in the order read, or an appropriate socket error.
schema !read(rdata!: out seq of byte, res!: out bool)
 post ?
  assert #rdata' > 0;		 Read currently available data from the socket as a sequence of bytes.
schema !read_noblock(rdata!: out seq of byte, res!: out bool)
  post ?;		 Read data if any is available but don't block if not, just return an empty sequence.
schema !write(data: byte, res!: out SocketError)
  post ?;		  
schema !write(data: seq of byte, res!: out SocketError)
  pre #data > 0
  post ?;		  

 

SocketError
class SocketError ^= enum success, unknownHost, ioError, generalError, invalidAddress, initError, invalidSocket, wrongType, connectionNotOpen end  

 

SocketMode
class SocketMode ^= enum client, server end  

 

StandardInputStream
final class StandardInputStream ^= inherits InputStream Class returned by method stdIn of class Environment.

Data
var charData: seq of char;
ghost function charData;		  

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream.
define ghost function gStreamAtEnd: bool
  ^= ?;		  
define ghost function gStreamData: seq of byte
  ^= env.gFileData(fref);		  
define ghost function gStreamPtr: nat
  ^= env.gFilePtr(fref);		  
define schema !read(b!: out byte, ret!: out FileError)
  post ?;		 Reads a byte from the stream.
schema !read(s!: out seq of byte, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream.
schema !read(n!: out int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class InputStream.
schema !read(c!: out char, decoder!: limited from CharDecoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream.
schema !read(r!: out real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class InputStream.

 

StandardOutputStream
final class StandardOutputStream ^= inherits OutputStream Class returned by methods stdOut and stdErr of class Environment.

Data
var charData: seq of char;
ghost function charData;		  

Methods
define schema !close(ret!: out FileError)
  post ?;		 Closes the stream and its associated file, flushing any buffered data to the device or file.
define schema !flush
  post ?;		 Flushes any buffered data to the device or file.
define ghost function gStreamData: seq of byte
  ^= ?;		  
define schema !write(b: byte, ret!: out FileError)
  post ?;		 Writes a byte to the file or device.
schema !write(s: seq of byte, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.
schema !write(i: int, numBytes: nat, ret!: out FileError)
  pre isOpen,
    numBytes ~= 0
  post ?;		 Inherited from class OutputStream.
schema !write(c: char, encoder: from CharEncoder, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.
schema !write(r: real, ret!: out FileError)
  pre isOpen
  post ?;		 Inherited from class OutputStream.

 

Storable
deferred class Storable This is the implicit ancestor of any class declared storable.

Methods
final schema store(env!: limited Environment, fref: from OutputStream, version: nat)
  post ?;		 Stores the object to the stream.

 

string
class string ^= seq of char  

 

Time
final class Time ^= storable Represents a date and time.

Data
var seconds: nat in 0..59,
  minutes: nat in 0..59,
  hours: nat in 0..23,
  day: nat in 0..6,
  date: nat in 1..31,
  month: nat in 1..12,
  year: nat;
function seconds, minutes, hours, day, date, month, year;		 Day 0 is Sunday, month 1 is January, and the year is AD.

Constructors
build {!seconds, !minutes, !hours, !day, !date, !month, !year: nat}
  pre seconds in 0..59,
    minutes in 0..59,
    hours in 0..23,
    day in 0..6,
    date in 1..31,
    month in 1..12;		  

Methods
total operator ~~(rhs)
  ^= ( let yearRank ^= year ~~ rhs.year;
        [yearRank = rank same]:
          ( let monthRank ^= month ~~ rhs.month;
            [monthRank = rank same]:
              ( let dateRank ^= date ~~ rhs.date;
                [dateRank = rank same]:
                  ( let dayRank ^= day ~~ rhs.day;
                    [dayRank = rank same]:
                      ( let hourRank ^= hours ~~ rhs.hours;
                        [hourRank = rank same]:
                          ( let minuteRank ^= minutes ~~ rhs.minutes;
                            [minuteRank = rank same]:
                              seconds ~~ rhs.seconds,
                            []:
                              minuteRank
                          ),
                        []:
                          hourRank
                      ),
                    []:
                      dayRank
                  ),
                []:
                  dateRank
              ),
            []:
              monthRank
          ),
        []:
          yearRank
      );		 Later dates/times rank above earlier ones.
redefine function toString: string
  ^= ?
assert result ~= "";		 This is a simple definition of toString for diagnostic purposes. In an application, you will need to define a text representation that takes account of the local conventions for printing days, dates and times.

 

triple of (X, Y, Z)
final class triple of (X, Y, Z) ^= storable  

Data
var x: X, y: Y, z: Z;
selector x, y, z;		  

Constructors
build {!x: X, !y: Y, !z: Z};  

Methods
operator ~~(a)
  ^= ( let t1 ^= x ~~ a.x;
        [t1 = rank same ]:
          ( let t2 ^= y ~~ a.y;
            [t2 = rank same]:
              z ~~ a.z,
            []:
              t2
          ),
        []:
          t1
      );		  
redefine function toString: string
  ^= ?
  assert result ~= "";		  

 

void
final class void ^= storable The void type has a single value denoted by the literal null. It has no constructors.

Methods
redefine function toString: string
  ^= "null";		  

 

Perfect Language Reference Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.