Program Examples in Mungo

This page is a repository of program examples written in the Mungo language and typechecked using the mungob tool. All examples type check, and where a main class is available, the output of executing the programs is also available.

File Example

File protocol
Protocol for File class

The classic example for typestate programming. A file follows a simple protocol. A file can only be read after it has been opened, and only while the file contains more data than what has already been read. The figure above illustrates this protocol, which can also be seen, expressed as a usage, in the code below.

The implementation of the File class itself is only a skeleton implementation, but the usage is specified according to an actual file implementation. So the interesting class is the main class which actually reads a file. Omitting the line f.open() would cause a type error, as would removing the line f.close().

class File [{open; rec X.{isEmpty; <{close; end}, {read; X}>}}] {

    string next
    void open() {
        unit
    }
    
    bool isEmpty() {
        next = input();
        next == ""
    }

    string read() {
        next
    }

    void close() {
        unit
    }
}



class main[{main; end}] {
    File f
    string lastLine    
    void main() {
        f = new File;
        f.open();
        (loop: 
            if (f.isEmpty()) {
                f.close()
            } else {
                lastLine = f.read();
                print(lastLine);
                continue loop
            }
        )
    }
}

Output

 
$ mungob exampleprograms/file.mg < datafile.txt

file
with
multiple
lines

House Controller Example

House controller protocol
Protocol for HouseController class

Here we present a more complex example of a class composed of multiple unlrelated fields. Parallel usages allows for the specfication of a protocol with unrelated parts. In this example, each field results in a parallel constituent for a local protocol for using that specific field. The parallel usages avoid enumerating the exponential number of states arising when allowing arbritrary interleaving of methods on unrelated fields without parallel usages. The figure above illustrates the parallel usage, where each local protocol is followed simultaneously.

class LightController[
        { on; rec Y.{changeIntensity; Y off; end} }
    ] {
    void on() {
        print("LightController turned on")
    }
    void off() {
        print("LightController turned off")
    }
    void changeIntensity() {
        print("LightController set to high intensity")
    }
}

class TempController [
        rec A.{
            setTemperature; A
            off; end
        }
    ] {
    void off() {
        print("TempController turned off")
    }
    void setTemperature(int temp) {
        print("TempController set to high intensity");
        print(temp)
    }
}

class DoorController [
        rec B.{
            lock; B
            unlock; B
            off; end
        }
    ] {
    void off() {
        print("DoorController turned off")
    }
    
    void lock() {
        print("DoorController locked doors")
    }

    void unlock() {
        print("DoorController unlocked doors")
    }
}

class HouseController [
    (
    { initLightController; 
        {lightOn; rec C.{ 
            adjustLight; C 
            lightOff; end}}}
    |
    { initTempController; 
        rec D. {
            setTemperature; D
            turnTempOff; end}}
    |
    { initDoorController; 
        rec E. {
            lockDoors; E
            unlockDoors; E
            turnDoorOff; end }} 
    ).end 
    ] {
    LightController lc
    TempController tc
    DoorController dc

    void initLightController() { lc = new LightController }

    void initTempController() { tc = new TempController }

    void initDoorController() { dc = new DoorController }

    void lightOn() { lc.on() }

    void adjustLight() { lc.changeIntensity() }

    void lightOff() { lc.off() }

    void setTemperature(int x) { tc.setTemperature(x) }

    void turnTempOff() { tc.off() }

    void lockDoors() { dc.lock() }

    void unlockDoors() { dc.unlock() }

    void turnDoorOff() { dc.off() }
}

Bank Account Example

Account protocol
Protocol for Account class

In this example we present the sequential usage, and show how a usage U;U’=(U|end).U’ can be used to simplify method parameter types, and allow a form of method overloading. The figure above shows the protocol for a bank account. The balance of the account cannot be accessed after calling addSalary but before applyInterest, hence we never access an intermediate account balance. By using behavioural separation with the sequential usage, the output method can be used when account has type Account[{getBalance; end};{addSalary; {applyInterest; end}};{getBalance; end}] and Account[{getBalance; end}].

class Account [
        {getBalance; end};{addSalary; {applyInterest; end}};{getBalance; end}
    ] {

    int balance

    int getBalance() { balance }
    void addSalary() { balance = (balance + 16000) }
    void applyInterest() { balance = (balance + 30) }
}

class Printer [rec X.{output; X finish; end}] {
    int balance
    void output(Account[{getBalance; end}] -> Account[end] x) {
        balance = x.getBalance();
        print(balance)
    }
    void finish() { unit }
}

class main [{main; end}] {
    Account acc
    Printer p

    void main() {
        acc = new Account;
        p = new Printer;
        p.output(acc);
        acc.addSalary();
        acc.applyInterest();
        p.output(acc);
        p.finish()
    }
}

Output

 
$ mungob exampleprograms/account.mg


0
16030

Travel Agency Example

Agency protocol
Protocol for Agency class

We present another classic example, this time from session type theory. A customer must contact a travel agency and book a trip, after bargaining for a price that is acceptable. The protocol for the travel agent is shown above, and shows a quote can be continuosly requested until the price is reasonable, in which case the trip is accepted, and the travel service is contacted and given the buyers information, and a date for the trip is returned.

class PriceValidator[{isFairPrice; <end, end>}] {
    bool isFairPrice(int x) {
        (x <= 100)
    }
}

class Customer[{bargain; {finalize; end}}] {
    int price
    PriceValidator pv
    Service s
    int date

    void bargain(Agency[{getQuote; rec X.{getQuote; X accept; end}}] -> Agency[end] agent) {
        pv = new PriceValidator;
        price = agent.getQuote();
        if (pv.isFairPrice(price)) {
            print("Initial price accepted");
            print(price);
            s = agent.accept()
        } else {
            pv = new PriceValidator;
            loop: (
                price = agent.getQuote();
                print("New price received from agency");
                print(price);
                if (pv.isFairPrice(price)) {
                    print("Accepted price");
                    print(price);
                    s = agent.accept()
                } else {
                    pv = new PriceValidator;
                    continue loop
                }
            )
        }
        
    }

    void finalize() {
        s.setAddress("Selma Lagerlöfs Vej 300");
        date = s.getDate()
    }
}

class Agency[{init; {getQuote; rec X.{getQuote; X accept; end}}}] {
    int curQuote

    void init() {
        curQuote = (210)
    }

    int getQuote() {
        curQuote = (curQuote - 10);
        curQuote
    }

    Service[{setAddress; {getDate; end}}] accept() {
        new Service
    }

}

class Service[{setAddress; {getDate; end}}] {
    string address
    void setAddress(string x) {
        address = x
    }

    int getDate() {27}
}

class main[{main; end}] {
    Customer c
    Agency a
    
    void main() {
        c = new Customer;
        a = new Agency;
        a.init();
        c.bargain(a);
        c.finalize()
    }
}

Output

 
$ mungob exampleprograms/travel.mg


New price received from agency
190
New price received from agency
180
New price received from agency
170
New price received from agency
160
New price received from agency
150
New price received from agency
140
New price received from agency
130
New price received from agency
120
New price received from agency
110
New price received from agency
100
Accepted price
100

Aliasing Example

Pair protocol
Protocol for Pair class

We present an example of aliasing. The Pair class must be initialised with a left and right value before calling the sum method. The PairUser class initialises both a left side and right side of a pair, given as arguments. Calling the method with the same Pair object as both parameters, causes the full object to be initialised.

class Pair[({setLeft; end} | {setRight; end}).{sum; end}] {
    int left
    int right

    void setLeft(int x) { left = x }
    
    void setRight(int x) { right = x }

    int sum() { left + right }
}

class PairUser[{initialise; end}] {
    void initialise(Pair[{setLeft; end}] -> Pair[end] l, 
                    Pair[{setRight; end}] -> Pair[end] r) {
        l.setLeft(2);
        r.setRight(5)
    }
}

class main[{main; end}] {
    Pair p
    PairUser pu
    int res

    void main() {
        p = new Pair;
        pu = new PairUser;
        pu.initialise(p, p);
        res = p.sum();
        print(res)
    }
}

Output

 
$ mungob exampleprograms/pair.mg


7