This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models. The first one is a map-based, classical versioned key-value store; the second one, journal-based, appends individual transaction effects to a journal. We formalise a significant part of the specification in the Coq proof assistant. This work will form the basis for a formalisation of a full-fledged backend store with features such as caching or write-ahead logging, as variations on maps and journals.

翻译：本文描述了开发数据库后端形式化规范进行中的工作。我们提出了一个基本事务系统的预期行为的形式化，该系统调用简单的存储API，并在两个语义模型中实例化。第一个是基于映射的经典版本化键值存储；第二个是基于日志的，将各事务效果追加到日志中。我们在Coq证明助手中形式化了规范的重要组成部分。这项工作将为完整后端存储的形式化奠定基础，该后端存储具备缓存或预写日志等功能，作为映射和日志的变体。