counters.aug

Modules and composition · Source and specification

Files in this project

• main.aug
• counters.aug
• domain/app.aug
• domain/export.aug
• domain/models.aug
• domain/numbers.aug

Code

Indentation

// aug-spec: "counters.aug.md" explains this file. Read it before changes; refresh with aug spec.
/** Reading state has no mutation effect. */
interface State:
Explanation 1Explanation 2
    read() returns int
Explanation 1Explanation 2
_Initial() implements State:
Explanation 1Explanation 2
    read():
        return 0
Explanation 1Explanation 2
_Updated(int count) implements State:
Explanation 1Explanation 2
    read():
        return count
/** A mutable counter with an explicit transition contract. */
interface Counter:
Explanation 1Explanation 2
    increment() changes self
Explanation 1Explanation 2
    value() returns int
Explanation 1Explanation 2
_Counter(resolve mutable State initial to _state) implements Counter:
Explanation 1Explanation 2
    increment():
        _state to _Updated(count=_state.read() + 1)
Explanation 1Explanation 2
    value():
        return _state.read()
/** The complete counter composition; its mutable state belongs to each scope. */
composition Counters:
    implement State with _Initial
    implement Counter with _Counter scoped mutable

Braces

// aug-spec: "counters.aug.md" explains this file. Read it before changes; refresh with aug spec.
/** Reading state has no mutation effect. */
interface State {
Explanation 1Explanation 2
    read() returns int
}
Explanation 1Explanation 2
_Initial() implements State {
Explanation 1Explanation 2
    read() {
        return 0
    }
}
Explanation 1Explanation 2
_Updated(int count) implements State {
Explanation 1Explanation 2
    read() {
        return count
    }
}
/** A mutable counter with an explicit transition contract. */
interface Counter {
Explanation 1Explanation 2
    increment() changes self
Explanation 1Explanation 2
    value() returns int
}
Explanation 1Explanation 2
_Counter(resolve mutable State initial to _state) implements Counter {
Explanation 1Explanation 2
    increment() {
        _state to _Updated(count=_state.read() + 1)
    }
Explanation 1Explanation 2
    value() {
        return _state.read()
    }
}
/** The complete counter composition; its mutable state belongs to each scope. */
composition Counters {
    implement State with _Initial
    implement Counter with _Counter scoped mutable
}

Compiled specification

Interactions and sequences

State · interface · source

Reading state has no mutation effect.

State.read · source

It returns int.

Counter · interface · source

A mutable counter with an explicit transition contract.

Counter.increment · source

It may change self.

Counter.value · source

It returns int.

Counters · source

The complete counter composition; its mutable state belongs to each scope.

These providers are registered before startup. State is provided by _Initial. The same instance is shared. Counter is provided by _Counter. Each scope shares one instance. Shared mutation is allowed. It requires bindings for State.

_Initial · class · source

It implements State. It is private to this file.

_Initial.read · source

It returns 0. source

Checked interface

read() returns int

_Updated · class · source

It implements State. It is private to this file. It takes count as an integer, kept read-only.

_Updated.read · source

It returns count. source

Checked interface

read() returns int

_Counter · class · source

It implements Counter. It is private to this file. The _state dependency is injected as State and stored mutably and privately.

_Counter.increment · source

It may change self. It sets _state to a _Updated with count from _state.read plus 1. source

Checked interface

increment() returns void changes self

It may change self.

_Counter.value · source

It returns _state.read. source

Checked interface

value() returns int