counter.aug

Read access and mutable borrows · Source and specification

Files in this project

• main.aug
• counter.aug

Code

Indentation

// aug-spec: "counter.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
Counter(mutable int value) implements ICounter:
Explanation 1Explanation 2
    increment():
        borrow self:
            value = value + 1
Explanation 1Explanation 2
    read():
        return value
interface ICounter:
Explanation 1Explanation 2
    increment() changes self
Explanation 1Explanation 2
    read() returns int

Braces

// aug-spec: "counter.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
Counter(mutable int value) implements ICounter {
Explanation 1Explanation 2
    increment() {
        borrow self {
            value = value + 1
        }
    }
Explanation 1Explanation 2
    read() {
        return value
    }
}
interface ICounter {
Explanation 1Explanation 2
    increment() changes self
Explanation 1Explanation 2
    read() returns int
}

Compiled specification

Interactions and sequences

Counter · class · source

It implements ICounter. It takes value as an integer, kept mutable.

Counter.increment · source

It may change self. With temporary permission to change self, it increases value by 1. source

Checked interface

increment() returns void changes self

It may change self.

Counter.read · source

It returns value. source

Checked interface

read() returns int

ICounter · interface · source

ICounter.increment · source

It may change self.

ICounter.read · source

It returns int.