【问题标题】:Generic Data Structure Description Language通用数据结构描述语言
【发布时间】:2025-12-03 06:00:02
【问题描述】:

我想知道是否存在任何用于任意描述数据结构的格式和语义的声明性语言,可以将其编译为任何一组目标语言中该结构的特定实现。也就是说,类似于通用的data definition language,但旨在描述任意数据结构,例如向量、列表、树等,以及对这些结构的操作的语义。我问是因为我对这个概念的可行实施有了一个想法,我只是想知道它是否值得,因此,以前是否有人这样做过。

另一个稍微抽象一点的问题:数据结构的规范规范(它做什么)和它的实现(它是如何做的)之间有什么真正的区别吗?更具体地说,是否应该将相同需求的单独实现视为不同的结构

【问题讨论】:

    标签: data-structures programming-languages declarative


    【解决方案1】:

    如果您愿意,XML 与 XSLT 的组合可以描述一种数据结构,并根据您的选择提供基本上任何语言的匹配定义。我从未尝试过正式证明它,但我的第一个猜测是 S 表达式是 XML 的超集(模数语法差异)。

    至少在理论上,是的,对数据结构的作用和它如何做的描述之间存在(或至少可能存在)差异。举一个明显的例子,你可以描述一个从键到值的通用映射,它可以使用基于哈希表、跳过列表、二叉搜索树等的实现。这主要是一个在足够高的抽象级别上描述它的问题,以允许在实施中存在差异。如果您包含太多要求(复杂性、排序等),您可以很快排除许多实现。

    【讨论】:

    • XSLT 确实是一种有趣的方法。我会调查的。我并不是要问对于相同的需求是否可以有不同的实现。我的意思是问是否应该将相同需求的两个不同实现视为不同的数据结构。这对w.r.t有影响。这种元语言可以而且应该具有怎样的声明性。
    【解决方案2】:

    您可能对消息规范/数据序列化语言感兴趣,例如 Google 的协议缓冲区以及 ASN.1。这与您正在寻找的倾斜度略有不同,但本质相同。

    两者都是声明通用消息以进行通信的方式。协议缓冲区消息规范“编译”为不同的语言,但中心协议是一致的。 ASN.1 具有多种不同的编译实用程序以及不同的协议表示,在逻辑上与不同的文字实现保持一致。以 XER、PER 与 BER 为例。

    我喜欢一种规范语言,它只专注于针对逻辑内存结构的简单打包二进制布局。可能纯 C 结构是表达这一点的最简单常用方式。我曾希望 ASN.1 有一些方法可以做到这一点,但在看了一会儿之后,ASN.1 PER 很接近,但并不完全如此。

    编辑:Apache ThriftCapn' Proto 也可能很有趣。

    【讨论】:

      【解决方案3】:

      在动态逻辑中有一些处理这类事情的方法,它们试图捕捉程序的语义。但是,动态逻辑的含义是前置条件和后置条件,与列表的实际实现无关。

      这些数据结构本质上与实现相关,因为链表和数组之间的唯一区别在于它在内存中的布局方式。

      为此,有一种通用的数据定义语言——任何高级编程语言——C、C++、java——来指定这一点。它们中的任何一个都与另一个一样通用,因为在这种情况下,它们中的任何一个都可以编译为另一个。

      【讨论】:

      • 感谢您的帮助。我不同意你的观点,只是任何高级语言都构成真正通用的数据定义语言,因为即使逻辑细节相同,语言实现细节也必然不同。
      • 链表和数组公开了不同的操作/接口。具体来说,数组公开了一种随机访问的方式,但链表没有。
      【解决方案4】:

      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 Synthesis of Fast CollectionsGeneralized Data Structure Synthesis 中描述了它的实现。

      【讨论】: