我想知道是否存在任何用于任意描述数据结构的格式和语义的声明性语言,可以将其编译为任何一组目标语言中该结构的特定实现。也就是说,类似于通用数据定义语言,但旨在描述任意数据结构,例如向量、列表、树等,以及对这些结构的操作的语义。我问是因为我对这个概念的可行实施有了一个想法,我只是想知道它是否值得,因此,以前是否有人做过。
另一个稍微抽象一点的问题:数据结构的规范规范(它做什么)和它的实现(它是如何做的)之间有什么真正的区别吗?更具体地说,是否应该将相同要求的单独实现视为不同的结构?
我想知道是否存在任何用于任意描述数据结构的格式和语义的声明性语言,可以将其编译为任何一组目标语言中该结构的特定实现。也就是说,类似于通用数据定义语言,但旨在描述任意数据结构,例如向量、列表、树等,以及对这些结构的操作的语义。我问是因为我对这个概念的可行实施有了一个想法,我只是想知道它是否值得,因此,以前是否有人做过。
另一个稍微抽象一点的问题:数据结构的规范规范(它做什么)和它的实现(它是如何做的)之间有什么真正的区别吗?更具体地说,是否应该将相同要求的单独实现视为不同的结构?
如果您愿意,XML 与 XSLT 的组合可以描述一种数据结构,并根据您的选择提供基本上任何语言的匹配定义。我从未尝试过正式证明它,但我的第一个猜测是 S 表达式是 XML 的超集(模数语法差异)。
至少在理论上,是的,对数据结构的作用和它如何做的描述之间存在(或至少可能存在)差异。举一个明显的例子,你可以描述一个从键到值的通用映射,它可以使用基于哈希表、跳过列表、二叉搜索树等的实现。这主要是一个在足够高的抽象级别上描述它的问题,以允许在实施中存在差异。如果您包含太多要求(复杂性、排序等),您可以很快排除许多实现。
您可能对消息规范/数据序列化语言感兴趣,例如 Google 的协议缓冲区以及 ASN.1。这与您正在寻找的倾斜略有不同,但在同一条线上。
两者都是为通信声明通用消息的方式。协议缓冲区消息规范“编译”为不同的语言,但中央协议是一致的。ASN.1 有多个不同的编译实用程序以及不同的协议表示,在逻辑上与不同的文字实现保持一致。以 XER、PER 与 BER 为例。
我喜欢一种规范语言,它只关注针对逻辑内存结构的简单打包二进制布局。可能纯 C 结构是表达这一点的最简单常用方式。我曾希望 ASN.1 有办法做到这一点,但看了一会儿之后,ASN.1 PER 很接近,但并不完全如此。
编辑:Apache Thrift和Capn' Proto也可能很有趣。
在动态逻辑中有一些处理这类事情的方法,它们试图捕捉程序的语义。然而,动态逻辑的含义是前置条件和后置条件,并且与列表的实际实现无关。
这些数据结构本质上与实现相关,因为链表和数组之间的唯一区别在于它在内存中的布局方式。
为此,有一种通用数据定义语言——任何高级编程语言——C、C++、java——来指定这一点。它们中的任何一个都与另一个一样通用,因为在这种情况下,它们中的任何一个都可以编译为另一个。
Cozy是“一种从非常高级的规范中综合数据结构实现的工具”,当我问这个问题时,它似乎本质上是我实际寻找(或考虑编写)的语言。
它可以从使用其专有语言编写的数据结构规范中自动生成实现(在撰写本文时使用 Java 或 C++)。规范描述了数据结构的抽象状态、更新操作和查询操作,以及必须维护的不变量和求解器可以用来优化实现的假设。例如,这里是图数据结构的部分规范:
Graph:
handletype Node = { id : Int }
handletype Edge = { src : Int, dst : Int }
state nodes : Bag<Node>
state edges : Bag<Edge>
// Invariant: disallow self-edges.
invariant (sum [ 1 | e <- edges, e.val.src == e.val.dst ]) == 0;
op addNode(n : Node)
nodes.add(n);
op addEdge(e : Edge)
assume e.val.src != e.val.dst;
edges.add(e);
query out_degree(nodeId : Int)
sum [ 1 | e <- edges, e.val.src == nodeId ]
// …
Calvin Loncaric、Emina Torlak 和 Michael D. Ernst在 Fast Collections 的Fast Synthesis of Fast Collections和Generalized Data Structure Synthesis中描述了它的实现。