We present a composition-based approach to building correctby-construction database backing stores. In previous work, we specified the behaviour of several store variants and proved their correctness and equivalence. Here, we derive a Java implementation: the simplicity of the specification makes manual construction straightforward. We leverage spec-guaranteed store equivalence to compose performance features, then demonstrate practical value with CobbleDB, a reimplementation of RocksDB's levelled storage.

翻译：我们提出了一种基于组合的方法来构建正确性由构造保证的数据库后端存储。在先前的工作中，我们指定了几种存储变体的行为，并证明了其正确性和等价性。在此，我们推导出一个Java实现：规范的简洁性使得手动构建变得直接。我们利用规范保证的存储等价性来组合性能特征，然后通过CobbleDB（RocksDB分层存储的一个重实现）展示其实用价值。