论文标题
将规范SQL转换为Coq中的命令代码
Translating Canonical SQL to Imperative Code in Coq
论文作者
论文摘要
SQL是迄今为止最广泛使用和实施的查询语言。但是，在某些关键功能上，例如相关查询和无效语义，许多实现差异或包含错误。我们利用SQL和查询编译器形式化的最新进展来开发DBCERT，这是第一个经过机械验证的编译器，该编译器是从规范形式编写的SQL查询到当务代码的。 Building DBCert需要在本文中描述的几项新贡献。首先，我们指定并机械化从SQL到嵌套关系代数的完整翻译，可用于查询优化。其次，我们定义了IMP，这是一种足以表达SQL的小型命令式语言，可以针对包括JavaScript在内的几种执行语言。最后，我们使用嵌套的关系演算作为中间步骤开发了从嵌套的关系代数到IMP的机械化翻译。
SQL is by far the most widely used and implemented query language. Yet, on some key features, such as correlated queries and NULL value semantics, many implementations diverge or contain bugs. We leverage recent advances in the formalization of SQL and query compilers to develop DBCert, the first mechanically verified compiler from SQL queries written in a canonical form to imperative code. Building DBCert required several new contributions which are described in this paper. First, we specify and mechanize a complete translation from SQL to the Nested Relational Algebra which can be used for query optimization. Second, we define Imp, a small imperative language sufficient to express SQL and which can target several execution languages including JavaScript. Finally, we develop a mechanized translation from the nested relational algebra to Imp, using the nested relational calculus as an intermediate step.
