dam*_*uar 1 specifications terminology z-notation alloy
我已经在维基上阅读了这两个概念的定义,但差异仍然不明确.有人能举例和一些简单的解释吗？
声明性规范描述了具有约束的操作或函数,该约束将输出与输入相关联.它不是为您提供计算输出的方法,而是为您提供检查输出是否正确的规则.例如,考虑一个采用数组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')的新值与旧值相关联的约束.
有关声明式,基于模型的规范的许多示例,请参阅合金上的材料http://alloy.mit.edu或我的书籍Software Abstractions.您还可以通过本书附录中的示例看到基于模型的声明性语言之间的比较,可以在本书的网站http://softwareabstractions.org上找到.