august/1.0.0/io/contracts.aug

Labeled calls and injection · Dependency source and specification

This is the exact dependency version used by this example.

Code

Indentation

// Generated by aug spec. This is a copy of the installed dependency source.
// aug-spec: "contracts.aug.md" explains this file. Read it before changes; refresh with aug spec.
/** Permission to write to a console, provided by an explicitly selected adapter. */
capability Console:
    /** Write one line of text. @param value Text to display. */
Explanation 1Explanation 2
    write<T>(T value) uses Console.write
/** The native standard-output adapter. Construction performs no output. */
Explanation 1Explanation 2
SystemConsole() implements Console:
Explanation 1Explanation 2
    write<T>(T value):
        print(value=value)
/** Read UTF-8 text through an explicitly selected filesystem adapter. */
capability FileReader:
    /** Read text. @param path File path. @throws FileError The file could not be read. */
Explanation 1Explanation 2
    read(string path) returns string uses FileReader.read unless FileError
/** Write UTF-8 text through an explicitly selected filesystem adapter. */
capability FileWriter:
    /** Write text. @param path File path. @param content Text. @throws FileError Writing failed. */
Explanation 1Explanation 2
    write(string path, string content) uses FileWriter.write unless FileError
/** Native filesystem adapter. Construction opens no files. */
Explanation 1Explanation 2
LocalFiles() implements FileReader, FileWriter:
Explanation 1Explanation 2
    read(string path):
        return read_file(path=path)
Explanation 1Explanation 2
    write(string path, string content):
        write_file(path=path, content=content)
/** Read command-line input through an explicit dependency. */
capability Arguments:
Explanation 1Explanation 2
    read() returns List<string> uses Arguments.read
/** Native command-line arguments. */
Explanation 1Explanation 2
ProcessArguments() implements Arguments:
Explanation 1Explanation 2
    read():
        return arguments()

Braces

// Generated by aug spec. This is a copy of the installed dependency source.
// aug-spec: "contracts.aug.md" explains this file. Read it before changes; refresh with aug spec.
/** Permission to write to a console, provided by an explicitly selected adapter. */
capability Console {
    /** Write one line of text. @param value Text to display. */
Explanation 1Explanation 2
    write<T>(T value) uses Console.write
}
/** The native standard-output adapter. Construction performs no output. */
Explanation 1Explanation 2
SystemConsole() implements Console {
Explanation 1Explanation 2
    write<T>(T value) {
        print(value=value)
    }
}
/** Read UTF-8 text through an explicitly selected filesystem adapter. */
capability FileReader {
    /** Read text. @param path File path. @throws FileError The file could not be read. */
Explanation 1Explanation 2
    read(string path) returns string uses FileReader.read unless FileError
}
/** Write UTF-8 text through an explicitly selected filesystem adapter. */
capability FileWriter {
    /** Write text. @param path File path. @param content Text. @throws FileError Writing failed. */
Explanation 1Explanation 2
    write(string path, string content) uses FileWriter.write unless FileError
}
/** Native filesystem adapter. Construction opens no files. */
Explanation 1Explanation 2
LocalFiles() implements FileReader, FileWriter {
Explanation 1Explanation 2
    read(string path) {
        return read_file(path=path)
    }
Explanation 1Explanation 2
    write(string path, string content) {
        write_file(path=path, content=content)
    }
}
/** Read command-line input through an explicit dependency. */
capability Arguments {
Explanation 1Explanation 2
    read() returns List<string> uses Arguments.read
}
/** Native command-line arguments. */
Explanation 1Explanation 2
ProcessArguments() implements Arguments {
Explanation 1Explanation 2
    read() {
        return arguments()
    }
}

Compiled specification

Interactions and sequences

Console · capability interface · source

Permission to write to a console, provided by an explicitly selected adapter.

Console.write · source

Write one line of text. The type parameters are T. It takes value as T (Text to display). It can call Console.write.

SystemConsole · class · source

The native standard-output adapter. Construction performs no output. It implements Console.

SystemConsole.write · source

Write one line of text. It takes value as T. It can call Console.write. It prints value. source

Checked interface

write<T>(T value) returns void uses Console.write

The type parameters are T. It takes value as T (Text to display). It can call Console.write.

FileReader · capability interface · source

Read UTF-8 text through an explicitly selected filesystem adapter.

FileReader.read · source

Read text. It takes path as a string (File path).

It returns string. It can call FileReader.read. Failures can raise FileError (The file could not be read).

FileWriter · capability interface · source

Write UTF-8 text through an explicitly selected filesystem adapter.

FileWriter.write · source

Write text. It takes path as a string (File path) and content as a string (Text). It can call FileWriter.write. Failures can raise FileError (Writing failed).

LocalFiles · class · source

Native filesystem adapter. Construction opens no files. It implements FileReader and FileWriter.

LocalFiles.read · source

Read text. It takes path as a string. It can call FileReader.read. Failures can raise FileError (The file could not be read).

It returns read_file with path. source

Checked interface

read(string path) returns string unless FileError uses FileReader.read

It takes path as a string (File path). It can call FileReader.read. Failures can raise FileError (The file could not be read).

LocalFiles.write · source

Write text. It takes path and content as strings. It can call FileWriter.write. Failures can raise FileError (Writing failed).

It calls write_file with path and content. source

Checked interface

write(string path, string content) returns void unless FileError uses FileWriter.write

It takes path as a string (File path) and content as a string (Text). It can call FileWriter.write. Failures can raise FileError (Writing failed).

Arguments · capability interface · source

Read command-line input through an explicit dependency.

Arguments.read · source

It returns List<string>. It can call Arguments.read.

ProcessArguments · class · source

Native command-line arguments. It implements Arguments.

ProcessArguments.read · source

It can call Arguments.read. It returns arguments. source

Checked interface

read() returns List<string> uses Arguments.read

It can call Arguments.read.

Built-in operations follow the language reference.