Keys

The abstract data type for keys is quite simple:

include order

object key = {

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

    object impl = {
        interpret t -> bv[16]
    }
    isolate iso = iter with impl
}

That is, keys are totally ordered with a least element called 0. They could be, for example, ASCII strings ordered lexicographically, in which case the zero element would be the empty string. Just for a test, though, we will use 16-bit numbers.

Keys are also equipped with an iterator type. An iterator type gives us an end value that is greater than all other values. This is often needed in loops and also gives us a way to describe a range of keys as a semi-open interval [l,u) where l and u are iterator values.

For reference, here is the specification of order iterators, from the standard library:

module order_iterator(range) = {
    type t = struct {
        is_end : bool,
        val : range.t
    }

    instantiate totally_ordered(range.t)

    definition (X < Y) = ~is_end(X) & is_end(Y) 
                      | ~is_end(X) & ~is_end(Y) & val(X) < val(Y)

    function done(X,Y) = is_end(Y) | X < val(Y)
    function between(X,V,Y) = ~done(V,X) & done(V,Y)

    action create(x:range.t) returns (y:t)
    action end returns (y:t)

    object spec = {
        after create {
            assert ~is_end(y);
            assert val(y) = x
        }
        after end {
            assert is_end(y);
            assert val(y) = 0
        }
    }
    ...
}

Iterators provides several useful executable predicates. There is an order relation < such that end is greater than all values. There is a predicate done(X,Y) that tells us when value X is less than iterator Y. Finally, there is a predicate between(X,V,Y) that tells us when value V is in the interval [X,Y). These predicates are useful in writing invariants of loops.

Notice that iterators require that the range type be totally ordered. We have to prove this, which is why the key object contains this line:

    isolate iso = iter with impl

This says to use the interpration of type key.t to prove the properties required by key.iter.