Queue

include order
include collections

module message_queue(net_msg,seq_num) = {

    relation contents(M:net_msg.t)

    action enqueue(msg:net_msg.t) returns (ok:bool)
    action empty returns (res:bool)
    action pick_one returns (res:net_msg.t)
    action delete_all(seq:seq_num.t)


    object spec = {
    init ~contents(M)

    before enqueue {
        assert contents(X) -> net_msg.num(X) ~= net_msg.num(msg)
    }

    after enqueue {
        if ok {
        contents(msg) := true
        }
    }

    after empty returns (res:bool) {
        assert contents(M) -> ~res;
        assert ~res -> exists M. contents(M)
    }

    before pick_one {
        assert exists M. contents(M)
    }

    after pick_one {
        assert contents(res)
    }

    before delete_all  {
        contents(M) := contents(M) & ~(net_msg.num(M) <= seq)
    }
    }

    object impl = {

    instance imap : ordered_map(seq_num,net_msg.t)

    implement enqueue {
        call imap.set(net_msg.num(msg),msg);
        ok := true
    }

    implement empty {
        res := seq_num.iter.is_end(imap.lub(seq_num.iter.create(0)))
    }

    implement delete_all(seq:seq_num.t) {
        call imap.erase(seq_num.iter.create(0),seq_num.iter.create(seq_num.next(seq)))
    }

    implement pick_one {
        res := imap.get(seq_num.iter.val(imap.lub(seq_num.iter.create(0))),res)
    }

    conjecture imap.maps(X,Y) -> X = net_msg.num(Y)
    conjecture contents(Y) <-> imap.maps(net_msg.num(Y),Y)

    }

}