Seqnum

include order

module sequence_numbers = {

    type t
    instance props : totally_ordered_with_zero(t)
    instance iter : order_iterator(this)

    action next(seq:t) returns (res:t)

    object spec = {

    after next {
        assume exists X. seq < X;
        assert seq < res & (X < res -> X <= seq)
    }
    }

    object impl = {
    interpret t->bv[16]
    implement next {
        res := seq + 1
    }
    }

    isolate iso_props = iter,props,spec,impl
}