terminology - 声明性规范和基于模型的规范之间的区别

Question

我已经在 wiki 上阅读了这两个概念的定义，但区别仍然不清楚。有人可以举一些例子和一些简单的解释吗？

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 后，如果您刚刚插入该元素（e 等于 x）或者如果它之前存在（x 是 s 的成员），则元素 x 将成为集合的成员。相反，在像 Z 或 Alloy 这样的语言中，你会写出类似的东西

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

具有将集合（s'）的新值与旧值（s）相关联的约束。

有关声明性、基于模型的规范的许多示例，请参阅http://alloy.mit.edu上有关 Alloy 的材料，或我的《软件抽象》一书。您还可以通过本书附录中的示例查看基于模型的声明性语言之间的比较，该附录可在本书的网站http://softwareabstractions.org上找到。