Queue

include order
include collections

module message_queue(net_msg,seq_num) = {

    relation contents(M:net_msg.t)

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


    object spec = {
    init ~contents(M)

    before enqueue {
        assert ~contents(msg);
        contents(msg) := true
    }

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

    before pick_one {
        assert exists M. contents(M);
        call impl.spec.lemma
    }

    after pick_one {
        assert contents(res)
    }

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

    object impl = {

    type range

instantiate totally_ordered_with_zero(t) instance iter : order_iterator(range)

    individual full(X:range) : bool
    individual items(X:range) : net_msg.t

    init ~full(X)

    instance rev : map(net_msg.t,range,0)

    implement enqueue {
        assume exists X. ~full(X);
        if some pos:range. ~full(pos) {
        full(pos) := true;
        items(pos) := msg;
        call rev.set_(msg,pos)
        }
    }

    implement empty {
        if exists X. full(X) {
        res := false
        }
        else {
        res := true
        }
    }

    implement delete_all(seq:seq_num) {
        full(X) := full(X) & ~(net_msg.num(items(X)) <= seq)
    }

    implement pick_one {
        if some pos:range. full(pos) minimizing net_msg.num(items(pos)) {
        res := items(pos)
        }
    }

    object spec = {
        action lemma = {
        if some (msg:net_msg.t) contents(msg) {
            call rev.lemma(msg)
        }
        }
    }

    conjecture rev.map(M,X) -> (contents(M) <-> (full(X) & items(X) = M))
    conjecture full(X) & items(X) = M -> rev.map(M,X)

    }

}