resource.aug

Move ownership · Source and specification

Files in this project

• main.aug
• resource.aug

Code

Indentation

// aug-spec: "resource.aug.md" explains this file. Read it before changes; refresh with aug spec.
import Console from august.io
Explanation 1Explanation 2
Resource() implements IResource:
Explanation 1Explanation 2
    drop():
        pass
interface IResource:
    pass
Explanation 1Explanation 2
make() returns own Resource:
    own Resource value = Resource()
    return value
Explanation 1Explanation 2
consume(resolve Console console, own Resource value):
Explanation 1Explanation 2
    console.write(value="consumed")

Braces

// aug-spec: "resource.aug.md" explains this file. Read it before changes; refresh with aug spec.
import Console from august.io
Explanation 1Explanation 2
Resource() implements IResource {
Explanation 1Explanation 2
    drop() {
        pass
    }
}
interface IResource {
    pass
}
Explanation 1Explanation 2
make() returns own Resource {
    own Resource value = Resource()
    return value
}
Explanation 1Explanation 2
consume(resolve Console console, own Resource value) {
Explanation 1Explanation 2
    console.write(value="consumed")
}

Compiled specification

Interactions and sequences

Resource · class · source

It implements IResource.

Resource.drop · source

It continues without an operation. source

Checked interface

drop() returns void

IResource · interface · source

make · source

It returns ownership of Resource. It creates Resource and stores the result in owned value (Resource). It returns value. source

Checked interface

make() returns own Resource

It returns ownership of Resource.

consume · source

It takes value as Resource with ownership transferred. It gets console (Console) from dependency injection. It can call Console.write. It passes "consumed" to console.write. source

Checked interface

consume(resolve Console console, own Resource value) returns void uses Console.write

It takes value as Resource with ownership transferred. It gets console (Console) from dependency injection. It can call Console.write.

Dependencies

It uses Console (write) from august.io.