Общая структура данных Язык описания

Question

Мне интересно, существует ли какой-либо декларативный язык для произвольного описания формата и семантики структуры данных, который можно скомпилировать для конкретной реализации этой структуры в любом из набора целевых языков. То есть что-то вроде общего языка определения данных , но ориентированного на описание произвольных структур данных, таких как векторы, списки, деревья и т. Д., И семантики операций с этими структурами. Я спрашиваю, потому что у меня была идея о возможной реализации этой концепции, и мне просто интересно, стоит ли она того, и, следовательно, было ли это сделано раньше.

Другой, немного более абстрактный вопрос: существует ли реальная разница между нормативной спецификацией структуры данных (что она делает) и ее реализацией (как она это делает)? В частности, следует ли считать реализации одинаковыми требованиями различными структурами ?

Answer 1

Если вам так хочется, комбинация XML и XSLT может описать структуру данных и обеспечить определение соответствия практически на любом языке, если вы выберете. Я никогда не пытался это доказать формально, но мое первое предположение состояло бы в том, что S-выражения являются надмножеством XML (по модулю синтаксических различий).

По крайней мере, теоретически, да (или, по крайней мере, могут быть) различия между описанием того, что делает структура данных, и как она это делает. В качестве очевидного примера вы могли бы описать общее сопоставление ключей и значений, которое могло бы использовать реализацию, основанную на хеш-таблицах, списках пропусков, деревьях двоичного поиска и т. Д. В основном это вопрос описания этого на достаточно высоком уровне абстракции допускают различия в реализации. Если вы включите слишком много требований (сложность, порядок и т. Д.), Вы можете довольно быстро исключить множество реализаций.

Answer 2

Вас могут заинтересовать языки спецификации сообщений / сериализации данных, такие как Google Protocol Buffers, а также ASN.1. Это немного другой наклон, чем вы ищете, но в том же духе.

Оба являются способами объявления общих сообщений для связи. Протокол буфера спецификаций сообщений «компилируется» на разных языках, но центральный протокол согласован. ASN.1 имеет несколько различных утилит компиляции, а также различные представления протоколов, оставаясь логически совместимыми с различными реализациями литералов. Посмотрите на XER, PER против BER, например.

Мне бы понравился язык спецификаций, который бы просто фокусировался на простом упакованном бинарном макете и логической структуре памяти. Вполне возможно, что простые структуры C - это самый простой общий способ выразить это. Я надеялся, что у ASN.1 есть какой-то способ добраться до этого, но, посмотрев немного, ASN.1 PER близок, но не совсем.

Редактировать: Apache Thrift и Capn 'Proto также могут быть интересны.

Answer 3

Существуют подходы к такого рода вещам в динамической логике, которые пытаются уловить семантику программ. Однако значение в терминах динамической логики заключается в терминах предусловий и постусловий и не зависит от фактической реализации списка.

Эти структуры данных по своей природе связаны с реализацией, поскольку единственное различие между связанным списком и массивом заключается именно в том, как он размещен в памяти.

Для этого существует универсальный язык определения данных - любой язык программирования высокого уровня - C, C ++, java - который определяет это. Любой из них так же универсален, как и другой, поскольку в этом контексте любой из них может быть скомпилирован с другим.

Answer 4

Уютно - это «инструмент, который синтезирует реализации структуры данных из спецификаций очень высокого уровня» и, по-видимому, по сути является языком, который я действительно искал (или рассматривал написание), когда задавал этот вопрос.

Он может автоматически генерировать реализацию (в 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 ]

    // …

Его реализация описана в Быстрый синтез быстрых коллекций и Обобщенный синтез структуры данных Кальвином Лонкаричем, Эминой Торлак и Майклом Д. Эрнстом.