通用数据结构描述语言

Question

我想知道是否存在任意描述数据结构的格式和语义的声明性语言,可以在任何一组目标语言中编译成该结构的特定实现.也就是说,类似于通用数据定义语言,但旨在描述任意数据结构,如向量,列表,树等,以及对这些结构的操作语义.我问,因为我有一个关于这个概念的可行实现的想法,我只是想知道它是否值得,因此,它是否已经完成.

另一个稍微抽象的问题是:数据结构的规范性规范(它的作用)与其实现(它是如何实现的)之间是否存在真正的差异？更具体地说,是否应将相同要求的单独实施视为不同的结构？

Answer 1

Cozy是 \xe2\x80\x9ca 工具，它从非常高级的规范 \xe2\x80\x9d 合成数据结构实现，并且似乎本质上是我在问这个问题时实际寻找（或考虑编写）的语言。

\n\n

它可以根据用其专有语言编写的数据结构规范自动生成实现（在撰写本文时使用 Java 或 C++）。规范描述了数据结构的抽象状态、更新操作和查询操作，以及必须维护的不变量和求解器可以用来优化实现的假设。例如，以下是图数据结构的部分规范：

\n\n

Graph:\n    handletype Node = { id : Int }\n    handletype Edge = { src : Int, dst : Int }\n\n    state nodes : Bag<Node>\n    state edges : Bag<Edge>\n\n    // Invariant: disallow self-edges.\n    invariant (sum [ 1 | e <- edges, e.val.src == e.val.dst ]) == 0;\n\n    op addNode(n : Node)\n        nodes.add(n);\n\n    op addEdge(e : Edge)\n        assume e.val.src != e.val.dst;\n        edges.add(e);\n\n    query out_degree(nodeId : Int)\n        sum [ 1 | e <- edges, e.val.src == nodeId ]\n\n    // \xe2\x80\xa6\n

\n\n

它的实现在Calvin Loncaric、Emina Torlak 和 Michael D. Ernst 的《快速集合的快速综合和通用数据结构综合》中进行了描述。

\n