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分层存储的重实现——展示了实用价值。