class BUFFER_ACCESS [T]
    feature
        put(b : BOUNDED_BUFFER [T], x : T) is
            require
                not b.full
            do
                b.put(x)
            ensure
                not b.empty
            end

        get(b : BOUNDED_BUFFER [T]) : T is
            require
                not b.empty
            do
                Result := b.get
            ensure
                not b.full
            end
end -- class BUFFER_ACCESS