Key

include order

object key = {

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

returns the maximum key

    action max returns (x:t)

returns the least key greater than x

    action next(x:t) returns (y:t)

returns the greatest key less than x

    action prev(x:t) returns (y:t)

    object spec = {
    after max {
        assert X <= x
    }
    before next {
        assert exists Z. ~(Z <= x)
    }
    after next {
        assert x <= y & x ~= y & (X <= y & X ~= y -> X <= x)
    }
    before prev {
        assert exists Z. Z < x
    }
    after prev {
        assert y < x & (Y < x -> Y <= y)
    }
    }

    object impl = {
    interpret t -> bv[1]

    implement iter.prev {
        iter.iter_val(x) := max if iter.iter_end(y) else iter.iter_val(y) - 1;
        iter.iter_end(x) := false
    }

    implement max {
        x := 1
    }

    implement next {
        y := x + 1
    }

    implement prev {
        y := x - 1
    }
    }

    isolate iso_props = props with impl
}