Разница между декларативной и основанной на модели спецификацией

Question

Я прочитал определение этих двух понятий в вики, но разница все еще не ясна. Может ли кто-нибудь привести примеры и несколько простых объяснений?

Answer 1

Декларативная спецификация описывает операцию или функцию с ограничением, которое связывает вывод с вводом. Вместо того, чтобы давать вам рецепт для вычисления выходных данных, он дает вам правило для проверки правильности выходных данных. Например, рассмотрим функцию, которая принимает массив a и значение e и возвращает индекс элемента массива, соответствующего e. Декларативная спецификация скажет точно, что:

    function index (a, e)
      returns i such that a[i] = e

Напротив, операционная спецификация будет выглядеть как код, например, с циклом по индексам, чтобы найти i. Обратите внимание, что декларативные спецификации часто являются недетерминированными; в этом случае, если e соответствует более чем одному элементу e, существует несколько допустимых значений i (и в спецификации не сказано, что возвращать). Это мощная функция. Кроме того, декларативные спецификации часто не являются полными: здесь, например, спецификация предполагает, что такой i существует (и в некоторых языках вы бы добавили предварительное условие, чтобы сделать это явным).

Чтобы поддерживать декларативную спецификацию, язык обычно должен содержать логические операторы (особенно конъюнкцию) и квантификаторы.

Основанный на модели язык - это язык, который использует стандартные математические структуры (такие как множества и отношения) для описания состояния. Сплав и Z оба основаны на модели. Напротив, алгебраические языки (такие как OBJ и Larch) используют уравнения для неявного описания состояния. Например, чтобы указать операцию, которая вставляет элемент в набор, на алгебраическом языке вы могли бы написать что-то вроде

    member(insert(s,e),x) = (e = x) or member(s,x)

в котором говорится, что после того, как вы вставите e в s, элемент x будет членом набора, если вы только что вставили этот элемент (e равно x) или если он был там раньше (x является членом s). Напротив, на языке, таком как Z или Alloy, вы бы написали что-то вроде

    insert (s, e)
      s' = s U {e}

с ограничением, связывающим новое значение набора (ов) со старым значением (ями).

Многие примеры декларативной спецификации на основе моделей см. В материалах по Alloy по адресу http://alloy.mit.edu/ или в моей книге "Абстракции программного обеспечения". Вы также можете увидеть сравнения между декларативными языками на основе моделей на примере в приложении к книге, доступном на веб-сайте книги http://softwareabstractions.org/.